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 metadatas

Cited literature [42 references]  Display  Hide  Download

https://hal.inria.fr/hal-00915189
Contributor : Tamara Rezk <>
Submitted on : Saturday, December 7, 2013 - 5:10:23 AM
Last modification on : Friday, November 16, 2018 - 1:39:11 AM
Long-term archiving on : Friday, March 7, 2014 - 10:55:17 PM

File

barthe_pichardie_rezk_2010_v2....
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

1812

Files downloads

290