Formalizing non-interference for a simple bytecode language in Coq |
| |
Authors: | Florian Kammüller |
| |
Affiliation: | 1.Technische Universit?t Berlin, Institut für Softwaretechnik und Theoretische Informatik,TU Berlin,Berlin,Germany |
| |
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. C. B. Jones |
| |
Keywords: | Formal methods for security Programming language analysis Modular specification Interactive theorem proving |
本文献已被 SpringerLink 等数据库收录! |