Formalizing non-interference for a simple bytecode language in Coq
Article
Kammueller, F. 2008. Formalizing non-interference for a simple bytecode language in Coq. Formal Aspects of Computing. 20 (3), pp. 259-275.
Type | Article |
---|---|
Title | Formalizing non-interference for a simple bytecode language in Coq |
Authors | Kammueller, F. |
Abstract | In this paper, we describe the application of the interactive theorem prover Coq to the security analysis of bytecode as used in Java. We provide a generic specification and proof of non-interference for bytecode languages using the Coq module system. We illustrate the use of this formalization by applying it to a small subset of Java bytecode. The emphasis of the paper is on modularity of a language formalization and its analysis in a machine proof. |
Research Group | Foundations of Computing group |
Artificial Intelligence group | |
Publisher | Springer Verlag |
Journal | Formal Aspects of Computing |
ISSN | 0934-5043 |
Publication dates | |
2008 | |
Publication process dates | |
Deposited | 06 Jan 2011 |
Output status | Published |
Accepted author manuscript | |
Copyright Statement | Post refereed version as permitted by publisher. |
Language | English |
Permalink -
https://repository.mdx.ac.uk/item/83117
Download files
39
total views27
total downloads0
views this month0
downloads this month