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 metadatas

Cited literature [53 references]  Display  Hide  Download

https://hal.inria.fr/inria-00106182
Contributor : David Pichardie <>
Submitted on : Thursday, January 31, 2008 - 4:02:02 PM
Last modification on : Friday, November 16, 2018 - 1:24:16 AM
Long-term archiving on : Tuesday, September 21, 2010 - 3:48:40 PM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00106182, version 2

Citation

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

Share

Metrics

Record views

392

Files downloads

320