Modern programming languages provide helpful high-level abstractions and mechanisms (e.g. types, module, automatic memory management) that enforce good programming practices and are crucial when writing correct and secure code. However, the security guarantees provided by such abstractions are not preserved when a compiler translates a source program into object code. Formally secure compilation is an emerging research field concerned with the design and the implementation of compilers that preserve source-level security properties at the object level. This paper presents a short guided tour of the relevant literature on secure compilation. Our goal is to help newcomers to grasp the basic concepts of this field and, for this reason, we rephrase and present the most relevant results in the literature in a common setting.

A brief tour of formally secure compilation

Busi M.
;
2019-01-01

Abstract

Modern programming languages provide helpful high-level abstractions and mechanisms (e.g. types, module, automatic memory management) that enforce good programming practices and are crucial when writing correct and secure code. However, the security guarantees provided by such abstractions are not preserved when a compiler translates a source program into object code. Formally secure compilation is an emerging research field concerned with the design and the implementation of compilers that preserve source-level security properties at the object level. This paper presents a short guided tour of the relevant literature on secure compilation. Our goal is to help newcomers to grasp the basic concepts of this field and, for this reason, we rephrase and present the most relevant results in the literature in a common setting.
2019
CEUR Workshop Proceedings
File in questo prodotto:
File Dimensione Formato  
itasec19-main.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Accesso libero (no vincoli)
Dimensione 373.4 kB
Formato Adobe PDF
373.4 kB Adobe PDF Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/5034717
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? ND
social impact