Colección SciELO Chile

Departamento Gestión de Conocimiento, Monitoreo y Prospección
Consultas o comentarios: productividad@anid.cl
Búsqueda Publicación
Búsqueda por Tema Título, Abstract y Keywords



An Extended Account of Trace-relating Compiler Correctness and Secure Compilation
Indexado
WoS WOS:000753685700002
Scopus SCOPUS_ID:85119491281
DOI 10.1145/3460860
Año 2021
Tipo artículo de investigación

Citas Totales

Autores Afiliación Chile

Instituciones Chile

% Participación
Internacional

Autores
Afiliación Extranjera

Instituciones
Extranjeras


Abstract



Compiler correctness, in its simplest form, is defined as the inclusion of the set of traces of the compiled program in the set of traces of the original program. This is equivalent to the preservation of all trace properties. Here, traces collect, for instance, the externally observable events of each execution. However, this definition requires the set of traces of the source and target languages to be the same, which is not the case when the languages are far apart or when observations are fine-grained. To overcome this issue, we study a generalized compiler correctness definition, which uses source and target traces drawn from potentially different sets and connected by an arbitrary relation. We set out to understand what guarantees this generalized compiler correctness definition gives us when instantiated with a non-trivial relation on traces. When this trace relation is not equality, it is no longer possible to preserve the trace properties of the source program unchanged. Instead, we provide a generic characterization of the target trace property ensured by correctly compiling a program that satisfies a given source property, and dually, of the source trace property one is required to show to obtain a certain target property for the compiled code. We show that this view on compiler correctness can naturally account for undefined behavior, resource exhaustion, different source and target values, side channels, and various abstraction mismatches. Finally, we show that the same generalization also applies to many definitions of secure compilation, which characterize the protection of a compiled program linked against adversarial code.

Métricas Externas



PlumX Altmetric Dimensions

Muestra métricas de impacto externas asociadas a la publicación. Para mayor detalle:

Disciplinas de Investigación



WOS
Computer Science, Software Engineering
Scopus
Software
SciELO
Sin Disciplinas

Muestra la distribución de disciplinas para esta publicación.

Publicaciones WoS (Ediciones: ISSHP, ISTP, AHCI, SSCI, SCI), Scopus, SciELO Chile.

Colaboración Institucional



Muestra la distribución de colaboración, tanto nacional como extranjera, generada en esta publicación.


Autores - Afiliación



Ord. Autor Género Institución - País
1 Abate, Carmine Hombre MPI-SP - Alemania
MPI SP - Alemania
2 Blanco, Roberto Hombre MPI-SP - Alemania
MPI SP - Alemania
3 Ciobâca, Stefan Hombre Universitatea Alexandru Ioan Cuza - Rumania
Alexandru Ioan Cuza Univ - Rumania
4 Durier, Adrien Hombre MPI-SP - Alemania
MPI SP - Alemania
5 Garg, Deepak Hombre Max Planck Institute for Software Systems - Alemania
Max Planck Inst Software Syst - Alemania
6 Hrițcu, Cătălin Hombre MPI-SP - Alemania
MPI SP - Alemania
7 Patrignani, Marco Hombre CISPA - Helmholtz Center for Information Security - Alemania
CISPA Helmholz Ctr Informat Secur - Alemania
8 TANTER, ERIC PIERRE Hombre Universidad de Chile - Chile
9 Thibault, Jeremy Hombre MPI-SP - Alemania
MPI SP - Alemania

Muestra la afiliación y género (detectado) para los co-autores de la publicación.

Financiamiento



Fuente
European Research Council
Office of Naval Research
German Federal Ministry of Education and Research (BMBF)
Bundesministerium für Bildung und Forschung
Horizon 2020 Framework Programme
Defense Advanced Research Projects Agency
CISPA-Stanford
UAIC
DARPA grant SSITH/HOPE
European Research Council under ERC Starting Grant SECOMP
CISPA-Stanford Center for Cybersecurity

Muestra la fuente de financiamiento declarada en la publicación.

Agradecimientos



Agradecimiento
C. Abate, R. Blanco, A. Durier, C. Hrit,cu, É. Tanter, and J. Thibault part of this work was conducted while these authors were employed at or visiting Inria Paris. This article revises and extends the work of Abate et al. [2] presented at ESOP’20 with the following additions: It contains a more complete account of the classes of properties that can be preserved by correct compilers by discussing safety and hyperproperty preservation. It discusses recent work on the preservation of noninterference through compilation [7, 52, 74] and interprets this work within the presented framework. It unifies the language presentation for the compilers that are proven correct using different relations. It provides a self-contained and in-depth analysis of the classes of properties that can be preserved by secure compilers by discussing subset-closed hyperproperties, hypersafety, 2-relational properties, 2-relational safety, and 2-relational hyperproperties. Generally, this article provides more intuition and explanation for some of the presented notions as well as for the discussed instances of our theory. Please note that Coq symbols as well as Compiler Criteria are links: the former to Coq files in the external repository https://github.com/secure-compilation/different_traces, the latter to definitions inside this document. This work was in part supported by the European Research Council under ERC Starting Grant SECOMP (715753), by the German Federal Ministry of Education and Research (BMBF) through funding for the CISPA-Stanford Center for Cyberse-curity (FKZ: 13N1S0762), by DARPA grant SSITH/HOPE (FA8650-15-C-7558), by the Office of Naval Research for support through grant N00014-18-1-2620, Accountable Protocol Customization, and by UAIC internal grant 07/2018. Authors’ addresses: C. Abate, R. Blanco, A. Durier, C. Hrit,cu, and J. Thibault, MPI-SP, Universitätsstraβe 140, Bochum, Germany; emails: {carmine.abate, roberto.blanco, adrien.durier}@mpi-sp.org, catalin.hritcu@gmail.com, jeremy.thibault@mpi-sp.org; S,. Ciobâcă, Department of Computer Science, Alexandru Ioan Cuza University Ias,i, Bulevardul Carol I, Nr. 11, 700506, Ias,i, Romania; email: stefan.ciobaca@info.uaic.ro; D. Garg, Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany; email: dg@mpi-sws.org; M. Patrignani, Stanford, 343 Serra Mall USA and CISPA Helmholz Center for Information Security, Saarland Informatics Campus, Saarbrücken, Germany; email: mp@cs.stanford.edu; È. Tanter, Computer Science Department (DCC), University of Chile, Chile; email: etanter@dcc.uchile.cl.
This work was in part supported by the European Research Council under ERC Starting Grant SECOMP (715753), by the German Federal Ministry of Education and Research (BMBF) through funding for the CISPA-Stanford Center for Cybersecurity (FKZ: 13N1S0762), by DARPA grant SSITH/HOPE (FA8650-15-C-7558), by the Office of Naval Research for support through grant N00014-18-1-2620, Accountable Protocol Customization, and by UAIC internal grant 07/2018.

Muestra la fuente de financiamiento declarada en la publicación.