A Sound Type System for Secure Flow Analysis
Irvine, Cynthia E.
MetadataShow full item record
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.
RightsThis publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.
Showing items related by title, author, creator and subject.
Volpano, Dennis; Smith, Geoffrey (1995-07);We prove the soundness of a polymorphic type system for a language with variables assignments and rst class functions As a corollary this proves the soundness of the Edinburgh LCF ML rules for typing variables and assignments ...
Özgen, Mustafa (Monterey, California. Naval Postgraduate School, 1996-09);In an attempt to bring the ML-style type inference to the C programming language, Smith and Volpano developed a type system for a dialect of C, called PolyC SmV96a SmV95b. PolyC extends C with ML-style polymorphism and a ...
Tubach, Paul B. (George Washington University, 1966-04);Procurement of equipment and weapons systems In the Defense establishment is big business—for two reasons. First, the resources required to design, develop, end procure these items are staggering. Secondly, the soundness ...