We introduce Adversarial Logic, a new under-approximate logic constructed from incorrectness logic by introducing an explicit adversary. Adversarial logic emphasizes the ability to separate facts known to the adversary from facts solely known to the program under analysis. This flavor of program incorrectness can be used to analyze software in which error behavior happens at deeper levels of interactions between the program and its environment. Adversarial logic can be understood as a restriction of symbolic execution where symbolic variables can only be introduced by the adversary. To illustrate usage of adversarial logic, we introduce the oscillating bit protocol, an example algorithm where a side-channel vulnerability is discoverable in adversarial logic while remaining elusive to other frameworks. Additionally, we introduce the concept of equivalence testing, a weaker version of program equivalence only proved on specific program paths. We provide a denotational semantics to adversarial logic and prove its soundness, therefore guaranteeing that extracted attack paths are true positives.
Tue 6 DecDisplayed time zone: Auckland, Wellington change
10:30 - 12:00 | |||
10:30 30mTalk | SecWasm: Information Flow Control for WebAssemblyVirtual SAS Iulia Bastys Chalmers University of Technology, Maximilian Algehed Chalmers University of Technology, Sweden, Alexander Sjösten TU Wien, Andrei Sabelfeld Chalmers University of Technology | ||
11:00 30mTalk | Adversarial Logic SAS Julien Vanegue Bloomberg | ||
11:30 30mTalk | Property-driven code obfuscations - Reinterpreting Jones-optimality in Abstract Interpretation SAS |