A Sound Type System for Secure Flow Analysis

Get BibTex-formatted data

Author

Dennis Volpano, Geoffrey Smith, Cynthia Irvine

Entry type

article

Abstract

Ensuring secure iniformation 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 analysishas not been established satisfactorily. We formulate Denning\'s approach as a type system and ppresent a notion of soundness for the system that can be vieewed as a form of noninterferencee. Soundness is established by proving, with respect to a standard programming language semantics, that all well-typed programs have this noninterference property.

Date

1996 – July – 29

Journal

Journal of Computer Security

Key alpha

Volpano, Smith, Irvine

Pages

1-20

Publisher

IOS Press

Publication Date

0000-00-00

Keywords

type systems, program security, soundness proofs

Language

English

Location

A hard-copy of this is in the Papers Cabinet

Subject

secure information flow

BibTex-formatted data

To refer to this entry, you may select and copy the text below and paste it into your BibTex document. Note that the text may not contain all macros that BibTex supports.

@Article{ Volpano, Smith, Irvine,
	title = "A Sound Type System for Secure Flow Analysis",
	author = "Dennis Volpano, Geoffrey Smith, Cynthia Irvine",
	year = "1996",
	month = "July",
	journal = "Journal of Computer Security",
	pages = "1-20",
	publisher = "IOS Press",
	day = "29",
	abstract = "Ensuring secure iniformation 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 analysishas not been established satisfactorily.  We formulate Denning\'s approach as a type system and ppresent a notion of soundness for the system that can be vieewed as a form of noninterferencee.  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",
	language = "English",
	subject = "secure information flow",
}