Security Witnesses for Compiler Transformations
Compiler optimizations can be correct and yet be insecure. Program changes made during optimization may weaken security guarantees; for instance, by introducing new ways to leak secret data. This work presents a methodology for ensuring that security properties are preserved, at compile time. Properties are expressed as automata operating over a bundle of related program traces. A notion of automaton-based program refinement guarantees that the associated security property is preserved. In practice, such refinement relations can be generated by a compiler as it optimizes a source program, and validated with an independent refinement checker. This process formally establishes the security of every source-to-target transformation without, however, requiring a proof of correctness of the compiler implementation itself.
Presentation (PriSC-2019-Kedar-Namjoshi.pdf) | 565KiB |
Sun 13 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
14:00 - 15:30 | |||
14:00 30mTalk | Translation Validation for Security Properties PriSC Matteo BusiUniversità di Pisa - Dipartimento di Informatica, Pierpaolo DeganoUniversità di Pisa - Dipartimento di Informatica, Letterio GallettaIMT School for Advanced Studies Pre-print File Attached | ||
14:30 30mTalk | Security Witnesses for Compiler Transformations PriSC File Attached | ||
15:00 30mTalk | A Data Layout Description Language for Cogent PriSC Zilin ChenData61, CSIRO and UNSW, Matthew Di MeglioUNSW, Liam O'ConnorUNSW, Partha SusarlaData61, CSIRO, Christine RizkallahUNSW, Gabriele KellerUtrecht University |