Mixing Deductive and Inductive Analyses for Security Applications
Abstract:
Program analysis techniques often aim to recover relations between variables to check certain program properties. To recover such relations, we rely on two broad approaches: deductively deriving relations with rules and inductively inferring relations from examples. While being powerful, these approaches run into three fundamental challenges: the heavy workload of manually writing rules, computational intractability and low fidelity due to overfitting.
In this thesis, we propose new techniques to address the above challenges. We demonstrate the effectiveness of these techniques with three real-world security applications: type analysis for function arguments, exploit generation via dynamic symbolic execution and fault localization. For type analysis, we design a new technique to automatically learn rules to recover the type of function arguments from binaries. The learned rules exhibit comparable accuracy compared to manually written rules. For dynamic symbolic execution, we propose a new technique to recover the relations which dynamic symbolic execution fails to derive. Our experiments show that our technique can explore more paths and generate an exploit for around twice as many bugs as the vanilla dynamic symbolic execution. For fault localization, we divide it into two sub-problems: identifying the program points for patching and pinpointing the program variables at the identified program points for patching. For each sub-problem, we employ a specialized inductive approach using the examples constructed specially to avoid overfitting. Both techniques achieve much higher accuracy compared to the approaches using ad-hoc examples on their task.