Secure Optimization Through Opaque Observations
Secure applications implement software protections against side-channel and physical attacks. Such protections are meaningful at machine code or micro-architectural level, but they typically do not carry observable semantics at source level. To prevent optimizing compilers from altering the protection, security engineers embed input/output side-effects into the protection. These side-effects are error-prone and compiler-dependent, and the current practice involves analyzing the generated machine code to make sure security or privacy properties are still enforced. Vu et al. recently demonstrated how to automate the insertion of volatile side-effects in a compiler, but these may be too expensive in fined-grained protections such as control-flow integrity. We introduce observations of the program state that are intrinsic to the correct execution of security protections, along with means to specify and preserve observations across the compilation flow. Such observations complement the traditional input/output-preservation contract of compilers. We show how to guarantee their preservation without modifying compilation passes and with as little performance impact as possible. We validate our approach on a range of benchmarks, expressing the secure compilation of these applications in terms of observations to be made at specific program points.
preprint (prisc_opaque_observations.pdf) | 818KiB |
Sun 17 Jan Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
19:00 - 20:30: Formal analysis & proof techniquesPriSC at PriSC Chair(s): Marco PatrignaniStanford University, USA / CISPA, Germany, Jonathan ProtzenkoMicrosoft Research, Redmond | |||
19:00 - 19:18 Talk | Nanopass Back-Translation of Multiple Traces for Secure Compilation Proofs PriSC Pre-print Media Attached | ||
19:18 - 19:36 Talk | Explicit Leakage: Handling Side-Channel Behavior in Program Rewriting and Analysis PriSC Marc GourjonHamburg University of Technology and NXP Semiconductors Germany GmbH Media Attached | ||
19:36 - 19:54 Talk | Secure Optimization Through Opaque Observations PriSC Son Tuan VuSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Albert CohenGoogle, Karine HeydemannSorbonne Université, CNRS, Laboratoire d'Informatique de Paris 6, LIP6, Arnaud de GrandmaisonARM, Christophe GuillonSTMicroelectronics Pre-print Media Attached File Attached | ||
19:54 - 20:12 Talk | The Fox and the Hound: Comparing Fully Abstract and Robust Compilation PriSC Carmine AbateMax Planck Institute for Security and Privacy, Bochum, Germany, Matteo BusiUniversità di Pisa - Dipartimento di Informatica Pre-print Media Attached File Attached | ||
20:12 - 20:30 Talk | Toward Complete Stack Safety for Capability Machines PriSC Aina Linn GeorgesAarhus University, Armaël GuéneauAarhus University, Alix TrieuAarhus University, Lars BirkedalAarhus University Media Attached File Attached |