Adversarial Logic

Adversarial logic is a new program logic inspired from incorrectness logic, founded on under-approximation of possible executions, rather than on their over-approximation (as generally done for verification). This new type of logic provides a foundations for bug finding rather than the verification of their absence and admits no false positives, while admitting false negatives. In adversarial logic, the target program and the attack program are composed in parallel and the code contract is attack-driven, where the adversary must prove the presence of external conditions to bring the target into an incorrect state. This type of program analysis is useful to determine the criticality of software bugs and distinguish benign bugs from security vulnerabilities that can lead to compromise. Published at the International Static Analysis Symposium (Auckland, NZ, Dec 2022), https://link.springer.com/chapter/10.1007/978-3-031-22308-2_19

Julien Vanegue leads the software security strategy at Bloomberg in New York as a member of the CTO office. Julien’s role includes research and development of program analysis solutions tailored to Bloomberg’s software stack. Bloomberg is the world leader in financial information distribution.