Towards Temporal Adversarial Logic
We report on preliminary results embedding temporal reasoning in a new under-approximate program logic designed to detect software vulnerabilities stemming from program timing conditions. Examples of time-dependent security issues are constant-time programming vulnerabilities, which can be found in cryptographic software implementations and lead to information disclosure and secret leakage. Other under-approximate program logics such as Concurrent Incorrectness Separation Logic (CISL), Concurrent Adversarial Separation Logic (CASL), Adversarial Logic (AL) and Outcome Logic (OL), are similarly inspired by Incorrectness Logic (IL), however none of these logics currently incorporate temporal reasoning.
Head of Infrastructure & Security Research at Bloomberg in New York, USA.
Tue 16 JanDisplayed time zone: London change
14:00 - 15:30 | Concurrency, Security, & Hyper-propertiesIncorrectness at Mountbatten Exhibition Chair(s): Azalea Raad Imperial College London | ||
14:00 22mTalk | Quantitative Weakest Hyper Pre Incorrectness Linpeng Zhang University College London, Benjamin Lucien Kaminski Saarland University; University College London File Attached | ||
14:22 23mTalk | A Reachability Logic for a Weak Memory Model with Promises Incorrectness Lara Bargmann University of Oldenburg, Brijesh Dongol University of Surrey, Heike Wehrheim University of Oldenburg File Attached | ||
14:45 22mTalk | Towards Temporal Adversarial Logic Incorrectness Julien Vanegue Bloomberg, USA | ||
15:07 22mTalk | Finding counterexamples to ∀∃ hyperproperties Incorrectness DOI Pre-print | ||
