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 [6,7]. Until now, however, the soundness of