Toward Behavioral Software Security: Bridging the Gap between the Theoretical Strengths of Formal Methods and the Practical Needs of Real-World Binary Analysis

Software security critically depends on the ability to analyze program behavior. Detecting behaviors of interest is a cen- tral objective of many cybersecurity tasks. This is especially true at the binary level, where access to source code is often unavailable. As a consequence, although there are numerous automated tools for binary analysis, it remains extremely dif- ficult to identify vulnerabilities and malicious code in prac- tice. This means that identifying a vulnerable code segment (e.g., buffer overflow) or detecting a malicious behavior (e.g., for privilege escalation) requires significant manual interven- tion and domain-specific expertise. These shortcomings high- light the need for more principled, behavior-oriented meth- ods for software security analysis. To ground this exploration, this thesis first examines process algebras and their role in modeling system behavior within cybersecurity contexts. Build- ing on the principles of this formalism, I developed a lan- guage and rule system designed to describe and capture pat- terns of interest in binary code. I thus propose GOLDRUSH and SMELTERY, rule-based frameworks for detecting vulner- abilities and malware, respectively. The rule-based method combined with symbolic execution allows GOLDRUSH and SMELTERY to identify potentially vulnerable and malicious instructions in executables, respectively. To evaluate the ef- fectiveness of GOLDRUSH, we tested ten C libraries and dis- covered a 0-day buffer overflow in one of them. To evaluate SMELTERY, we analyzed a well-known dataset to classify ex- ecutables as benign or malicious. This work aims to bridge the gap between the theoretical strengths of formal methods and the practical needs of real-world binary analysis.