The paper “Inferring Secrets by Guided Experiments” (preprint) from Quoc Huy Do, Richard Bubel and Reiner Hähnle won the Best Paper Award at ICTAC 2017.
A program has secure information flow if it does not leak any secret information to publicly observable output. A large number of static and dynamic analyses have been devised to check programs for secure information flow. The authors present an algorithm that can carry out a systematic and efficient attack to automatically extract secrets from an insecure program. The algorithm combines static analysis and dynamic execution. The attacker strategy learns from past experiments and chooses as its next attack one that promises maximal knowledge gain about the secret. The idea is to provide the software developer with concrete information about the severity of an information leakage. The static analysis is based on KeY’s symbolic execution engine.