Visible to the public Secure Compilation and Hyperproperty Preservation

TitleSecure Compilation and Hyperproperty Preservation
Publication TypeConference Paper
Year of Publication2017
AuthorsPatrignani, M., Garg, D.
Conference Name2017 IEEE 30th Computer Security Foundations Symposium (CSF)
ISBN Number978-1-5386-3217-8
Keywordscoding theory, compiled program, compiler security, composability, Concrete, correctness criterion, fully abstract compiler, hyperproperty preservation, low-level attack capabilities, program compilers, Program processors, program verification, pubcrawl, Resiliency, Safety, safety hyperproperties, secure compilation, secure compilers, security, security of data, security properties, Semantics, Standards, Syntactics, TPC, trace-preserving compilation, Type theory, typed source language, untyped target language

The area of secure compilation aims to design compilers which produce hardened code that can withstand attacks from low-level co-linked components. So far, there is no formal correctness criterion for secure compilers that comes with a clear understanding of what security properties the criterion actually provides. Ideally, we would like a criterion that, if fulfilled by a compiler, guarantees that large classes of security properties of source language programs continue to hold in the compiled program, even as the compiled program is run against adversaries with low-level attack capabilities. This paper provides such a novel correctness criterion for secure compilers, called trace-preserving compilation (TPC). We show that TPC preserves a large class of security properties, namely all safety hyperproperties. Further, we show that TPC preserves more properties than full abstraction, the de-facto criterion used for secure compilation. Then, we show that several fully abstract compilers described in literature satisfy an additional, common property, which implies that they also satisfy TPC. As an illustration, we prove that a fully abstract compiler from a typed source language to an untyped target language satisfies TPC.

Citation Keypatrignani_secure_2017