Presented at
Summercon 2023,
July 14, 2023, 3 p.m.
(60 minutes)
Typical static analysis for program verification comes with an over-approximate flavor, which considers a superset of program behaviors to guarantee the absence of bugs. This is a problem as spurious behaviors can lead to false positives, the enemy of software developers and security auditors alike. In the last few years, a new kind of formal logic “incorrectness logic” (O’Hearn, POPL’20) introduced under-approximate program analysis, where every bug is guaranteed to be a true positive, at the expense of false negatives, therefore coming as a foundation for the theory of formal bug finding. Such methodology is applied at scale by large software vendors (e.g. Meta) and is more immediately usable in industrial CI/CD pipelines. This talk will introduce under-approximate reasoning to the Summercon crowd, and discuss a recent extension “adversarial logic” (Vanegue, SAS’22) extending incorrectness logic with explicit adversary to formalize the detection of exploit conditions in buggy programs.
Presenters:
-
Julien Vanegue
Julien Vanegue is a security researcher living in New York City who enjoys applying his logic knowledge to offense and defense.
Similar Presentations: