POPL 2019 (series) / PriSC 2019 (series) / Principles of Secure Compilation /
Translation Validation for Security Properties
Secure compilation aims to build compilation chains that preserve security properties when translating programs from a source to a target language. Recent research led to the definition of secure compilation principles that, if met, guarantee that the compilation chain in hand never violates specific families of security properties. Still, to the best of our knowledge, no effective procedure is available to check if a compilation chain meets such requirements. Here, we outline our ongoing research inspired by translation validation, to effectively check one of those principles.
Presentation (stv_prisc19.pdf) | 80KiB |
Sun 13 JanDisplayed time zone: Belfast change
Sun 13 Jan
Displayed time zone: Belfast change
14:00 - 15:30 | |||
14:00 30mTalk | Translation Validation for Security Properties PriSC 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 | ||
14:30 30mTalk | Security Witnesses for Compiler Transformations PriSC File Attached | ||
15:00 30mTalk | A Data Layout Description Language for Cogent PriSC 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 |