A certified lightweight non-interference Java bytecode verifier

Gilles Barthe 1 David Pichardie 2 Tamara Rezk 3
2 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
3 INDES - Secure Diffuse Programming
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : Non-interference guarantees the absence of illicit information flow throughout program execution. It can be enforced by appropriate information flow type systems. Much of the previous work on type systems for non-interference has focused on calculi or high-level programming languages, and existing type systems for low-level languages typically omit objects, exceptions and method calls. We define an information flow type system for a sequential JVM-like language that includes all these programming features, and we prove, in the Coq proof assistant, that it guarantees non-interference. An additional benefit of the formalisation is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to the best of our knowledge, the first sound and certified information flow type system for such an expressive fragment of the JVM.
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (5), pp.1032-1081. 〈10.1017/S0960129512000850〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00915189
Contributeur : Tamara Rezk <>
Soumis le : samedi 7 décembre 2013 - 05:10:23
Dernière modification le : mardi 16 janvier 2018 - 15:54:15
Document(s) archivé(s) le : vendredi 7 mars 2014 - 22:55:17

Fichier

barthe_pichardie_rezk_2010_v2....
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Gilles Barthe, David Pichardie, Tamara Rezk. A certified lightweight non-interference Java bytecode verifier. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (5), pp.1032-1081. 〈10.1017/S0960129512000850〉. 〈hal-00915189〉

Partager

Métriques

Consultations de la notice

922

Téléchargements de fichiers

166