Paper Info
Title
Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work
Abstract
Secure compilation is a discipline aimed at developing compilers that preserve the security properties of the source programs they take as input in the target programs they produce as output. This discipline is broad in scope, targeting languages with a variety of features (including objects, higher-order functions, dynamic memory allocation, call/cc, concurrency) and employing a range of different techniques to ensure that source-level security is preserved at the target level. This article provides a survey of the existing literature on formal approaches to secure compilation with a focus on those that prove fully abstract compilation, which has been the criterion adopted by much of the literature thus far. This article then describes the formal techniques employed to prove secure compilation in existing work, introducing relevant terminology, and discussing the merits and limitations of each work. Finally, this article discusses open challenges and possible directions for future work in secure compilation.
Year
DOI
Venue
2019
10.1145/3280984
ACM Computing Surveys (CSUR)
Keywords
DocType
Volume
Secure compilation, contextual equivalence, fully abstract compilation, program equivalence, type preserving compilation
Journal
51
Issue
ISSN
Citations 
6
0360-0300
4
PageRank 
References 
Authors
0.39
66
3
Name
Order
Citations
PageRank
Marco Patrignani111611.58
Amal Ahmed239127.05
Dave Clarke341626.19