Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sun 13 Jan 2019 14:30 - 15:00 at Sala VI - Session 3 Chair(s): Chung-Kil Hur

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

Displayed time zone: Belfast change

14:00 - 15:30
Session 3PriSC at Sala VI
Chair(s): Chung-Kil Hur Seoul National University
Translation Validation for Security Properties
Matteo Busi Università di Pisa - Dipartimento di Informatica, Pierpaolo Degano Università di Pisa - Dipartimento di Informatica, Letterio Galletta IMT School for Advanced Studies
Pre-print File Attached
Security Witnesses for Compiler Transformations
Kedar Namjoshi Bell Labs, Nokia, Lucas M. Tabajara Rice University
File Attached
A Data Layout Description Language for Cogent
Zilin Chen Data61, CSIRO and UNSW, Matthew Di Meglio UNSW, Liam O'Connor UNSW, Partha Susarla Data61, CSIRO, Christine Rizkallah UNSW, Gabriele Keller Utrecht University