Back to Search
Start Over
A certified lightweight non-interference Java bytecode verifier
- Source :
- Mathematical Structures in Computer Science, Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2013, 23 (5), pp.1032-1081. ⟨10.1017/S0960129512000850⟩, Mathematical Structures in Computer Science, 2013, 23 (5), pp.1032-1081. ⟨10.1017/S0960129512000850⟩
- Publication Year :
- 2013
- Publisher :
- Cambridge University Press (CUP), 2013.
-
Abstract
- International audience; 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.
- Subjects :
- Computer science
Programming language
Proof assistant
020207 software engineering
Java bytecode
02 engineering and technology
Non interference
Certification
Type (model theory)
computer.software_genre
Computer Science Applications
[INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Bytecode
Mathematics (miscellaneous)
Fragment (logic)
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
0202 electrical engineering, electronic engineering, information engineering
020201 artificial intelligence & image processing
Information flow (information theory)
computer
computer.programming_language
Subjects
Details
- ISSN :
- 14698072 and 09601295
- Volume :
- 23
- Database :
- OpenAIRE
- Journal :
- Mathematical Structures in Computer Science
- Accession number :
- edsair.doi.dedup.....afc87f42463f4582fb53f83f4588b8cd