Skip to Main content Skip to Navigation
Other publications

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.
Document type :
Other publications
Complete list of metadata

Cited literature [53 references]  Display  Hide  Download
Contributor : David Pichardie Connect in order to contact the contributor
Submitted on : Thursday, January 31, 2008 - 4:02:02 PM
Last modification on : Friday, February 4, 2022 - 3:25:09 AM
Long-term archiving on: : Tuesday, September 21, 2010 - 3:48:40 PM


Files produced by the author(s)


  • HAL Id : inria-00106182, version 2


Gilles Barthe, David Pichardie, Tamara Rezk. A Certified Lightweight Non-Interference Java Bytecode Verifier. 2007. ⟨inria-00106182v2⟩



Record views


Files downloads