Abstract |
This paper presents a type-based information flow analysis for
MicroJava, a substantial subset of sequential Java. The analysis is
given in the form of a type-and-effect system, which is required for
handling side-effecting expressions and dynamic method lookup. The
type system and a proof of noninterference are formalized in the
Isabelle proof assistant, extending a comprehensive existing model
of MicroJava.
Online Copy |
Available as PDF
Also look at the conference version.
Isabelle Sources |
See here
BibTeX Entry |
@TechReport{strecker03:_infoflow_type_tr, author = {Martin Strecker}, title = {Formal Analysis of an Information Flow Type System for {M}icro{J}ava (Extended Version)}, institution = {Technische Universit{\"a}t M{\"u}nchen}, year = 2003, month = jul }
Last modified: Sat Nov 11 20:34:30 CET 2006 |