A Certified Lightweight Non-Interference Java Bytecode Verifier

Gilles Barthe 1 David Pichardie 2 Tamara Rezk 1
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
Abstract : Non-interference is a semantical condition on programs that guarantees the absence of illicit information flow throughout their execution, and that can be enforced by appropriate information flow type systems. Much of 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, and/or do not prove formally the soundness of the type system. We define an information flow type system for a sequential JVM-like language that includes classes, objects, arrays, exceptions and method calls, and prove that it guarantees non-interference. For increased confidence, we have formalized the proof in the proof assistant Coq; an additional benefit of the formalization is that we have extracted from our proof a certified lightweight bytecode verifier for information flow. Our work provides, to our best knowledge, the first sound and implemented information flow type system for such an expressive fragment of the JVM.
Type de document :
Autre publication
submitted to TOPLAS in September 2007. 2007
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00106182
Contributeur : David Pichardie <>
Soumis le : jeudi 31 janvier 2008 - 16:02:02
Dernière modification le : vendredi 16 novembre 2018 - 01:24:16
Document(s) archivé(s) le : mardi 21 septembre 2010 - 15:48:40

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00106182, version 2

Collections

Citation

Gilles Barthe, David Pichardie, Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. submitted to TOPLAS in September 2007. 2007. 〈inria-00106182v2〉

Partager

Métriques

Consultations de la notice

372

Téléchargements de fichiers

240