SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Tue 6 Dec 2022 11:00 - 11:30 at AMRF Auditorium - Security Chair(s): Emanuele D’Osualdo

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 Dec

Displayed time zone: Auckland, Wellington change

10:30 - 12:00
SecuritySAS at AMRF Auditorium
Chair(s): Emanuele D’Osualdo MPI-SWS
10:30
30m
Talk
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
30m
Talk
Adversarial Logic
SAS
Julien Vanegue Bloomberg
11:30
30m
Talk
Property-driven code obfuscations - Reinterpreting Jones-optimality in Abstract Interpretation
SAS
Roberto Giacobazzi University of Verona, Isabella Mastroeni University of Verona, Italy