Secure Multi-Execution through Static Program Transformation

Abstract : Secure multi-execution (SME) is a dynamic technique to ensure secure information flow. In a nutshell, SME enforces security by running one execution of the program per security level, and by reinterpreting input/output operations w.r.t. their associated security level. SME is sound, in the sense that the execution of a program under SME is non-interfering, and precise, in the sense that for programs that are non-interfering in the usual sense, the semantics of a program under SME coincides with its standard semantics. A further virtue of SME is that its core idea is language-independent; it can be applied to a broad range of languages. A downside of SME is the fact that existing implementation techniques require modifications to the runtime environment, e.g. the browser for Web applications. In this article, we develop an alternative approach where the effect of SME is achieved through program transformation, without modifications to the runtime, thus supporting server-side deployment on the web. We show on an exemplary language with input/output and dynamic code evaluation (modeled after JavaScript’s eval) that our transformation is sound and precise. The crux of the proof is a simulation between the execution of the transformed program and the SME execution of the original program. This proof has been machine-checked using the Agda proof assistant. We also report on prototype implementations for a small fragment of Python and a substantial subset of JavaScript.
Type de document :
Communication dans un congrès
Holger Giese; Grigore Rosu. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7273, pp.186-202, 2012, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-30793-5_12〉
Liste complète des métadonnées

Littérature citée [29 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01528736
Contributeur : Hal Ifip <>
Soumis le : lundi 29 mai 2017 - 15:54:00
Dernière modification le : lundi 29 mai 2017 - 15:55:35
Document(s) archivé(s) le : mercredi 6 septembre 2017 - 11:25:06

Fichier

978-3-642-30793-5_12_Chapter.p...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Gilles Barthe, Juan Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas. Secure Multi-Execution through Static Program Transformation. Holger Giese; Grigore Rosu. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7273, pp.186-202, 2012, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-30793-5_12〉. 〈hal-01528736〉

Partager

Métriques

Consultations de la notice

45

Téléchargements de fichiers

27