Skip to Main content Skip to Navigation
New interface
Journal articles

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

Cited literature [42 references]  Display  Hide  Download
Contributor : Tamara Rezk Connect in order to contact the contributor
Submitted on : Saturday, December 7, 2013 - 5:10:23 AM
Last modification on : Monday, June 27, 2022 - 3:04:57 AM
Long-term archiving on: : Friday, March 7, 2014 - 10:55:17 PM


Files produced by the author(s)



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



Record views


Files downloads