Relational bytecode correlations

13 years 2 months ago
Relational bytecode correlations
We present a calculus for tracking equality relationships between values through pairs of bytecode programs. The calculus may serve as a certification mechanism for noninterference, a well-known program property in the field of language-based security, and code transformations. Contrary to previous type systems for non-interference, no restrictions are imposed on the control flow structure of programs. Objects, static and virtual methods are included, and heap-local reasoning is supported by frame rules. In combination with polyvariance, the latter enable the modular verification of programs over heap-allocated data structures, which we illustrate by verifying and comparing different implementations of list copying. The material is based on a complete formalisation in Isabelle/HOL. Key words: Non-interference, Relational proof systems, Program transformations, Proof-carrying code, Formalised program analyses
Lennart Beringer
Added 19 May 2011
Updated 19 May 2011
Type Journal
Year 2010
Where JLP
Authors Lennart Beringer
Comments (0)