A sound type system for secure flow analysis

Article type: Research Article

Authors: Volpano, Dennis^a | Irvine, Cynthia^a | Smith, Geoffrey^b

Affiliations: [a] Computer Science Department, Naval Postgraduate School, Monterey, California 93943, USA | [b] School of Computer Science, Florida International University, Miami, Florida 33199, USA

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 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.

Keywords: Type systems, program security, soundness proofs

DOI: 10.3233/JCS-1996-42-304

Journal: Journal of Computer Security, vol. 4, no. 2-3, pp. 167-187, 1996