A Sound Type System for Secure Flow Analysis

Abstract

Ensuring secure information flow within programs in the context of multiple sensitivity levels has been widely studied Especially noteworthy is Denning' s work in secure flow analysis and the lattice model. Until now however the soundness of Denning s analysis has not been established satisfactorily We formulate Denning's approach as a type system and present a notion of soundness for the system that can be viewed as a form of noninterference Soundness is established by proving with respect to a standard programming language semantics that all well typed programs have this noninterference property.