A Sound Type System for Secure Flow Analysis
96paper_jcs.pdf (216.1Kb)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.
Rights
This 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.Related items
Showing items related by title, author, creator and subject.
-
A Type Soundness Proof for Variables in LCF ML
(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 ... -
A type inference algorithm and transition semantics for polymorphic C
(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 ... -
Improving the system for providing spare parts support for new Marine Corps equipment
(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 ...
