uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Formal Approaches to Secure Compilation: A Survey of Fully Abstract Compilation and Related Work
Stanford Univ, Comp Sci Dept, 353 Serra Mall, Stanford, CA 94301 USA;CISPA, Saarbrucken, Germany.
Northeastern Univ, Coll Comp & Informat Sci, 328 West Village H,360 Huntington Ave, Boston, MA 02115 USA.
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science.
2019 (English)In: ACM Computing Surveys, ISSN 0360-0300, E-ISSN 1557-7341, Vol. 51, no 6, article id 125Article in journal (Refereed) Published
Abstract [en]

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.

Place, publisher, year, edition, pages
2019. Vol. 51, no 6, article id 125
Keywords [en]
Secure compilation, fully abstract compilation, type preserving compilation, contextual equivalence, program equivalence
National Category
Computer Sciences
Identifiers
URN: urn:nbn:se:uu:diva-379940DOI: 10.1145/3280984ISI: 000460376100016OAI: oai:DiVA.org:uu-379940DiVA, id: diva2:1299353
Funder
EU, European Research Council, 715753Available from: 2019-03-26 Created: 2019-03-26 Last updated: 2019-03-26Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full text

Authority records BETA

Clarke, Dave

Search in DiVA

By author/editor
Clarke, Dave
By organisation
Computing Science
In the same journal
ACM Computing Surveys
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 39 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf