Reasoning about software security via synthesized behavioral substitutes

Since software is an integral part of our daily life, it is of great importance to ensure its safety and security. Still, we frequently observe attackers exploiting security vulnerabilities to steal secret customer information, manipulate essential data and take control over critical infrastructure. On the other hand, security researchers make efforts to find and eliminate security flaws, which is often a non-trivial task. Even more, it is proven to be undecidable. As a consequence, security analysis is often goal-oriented, effectively limiting the analysis scope by focusing only on certain types of bugs or proving the presence of specific program characteristics. Therefore, analysis techniques are based on assumptions that may only hold in artificial scenarios. In practice, such methods are either too broad and suffer from false positives or too narrow and miss many cases. Still, they often are very effective for their designed use case and alleviate tedious and time-consuming work of a human analyst. Some techniques are based on abstraction in which we transform parts of a program into an abstract domain that is explicitly constructed to facilitate reasoning about specific characteristics. In this domain, a so-called behavioral substitute represents only the desired characteristics of a given program. Often, the transformation process relies on labor-intensive manually implemented rules, resulting in behavioral substitutes that are too generic or incomplete in some cases. In this thesis, we propose problem-specific analysis techniques based on synthesized behavioral substitutes to advance research on topics related to code deobfuscation, fuzzing and root cause analysis. In each case, we design a domain-specific representation that allows generic reasoning in its associated area. We apply stochastic program synthesis techniques to automatically learn behavioral substitutes. For this, we use the target program as a black-box, basically using the program’s behavior as feedback. This combination of crafting target-specific representations in a problem-specific domain allows us to reason about more generic instances of the problem while staying close to the target. As a consequence, our methods are generic regarding the problem and geared to the target, allowing us to operate on a wide range of problem instances without implementing a target-specific analysis. In our empirical evaluation, we show for various real-world targets that we either outperform state-of-the-art approaches or that our techniques are orthogonal to existing approaches and perform in scenarios where others do not.