KIT | KIT-Bibliothek | Impressum | Datenschutz

A Correctness Proof for the Volpano/Smith Security Typing System

Snelting, Gregor; Wasserrab, Daniel

The Volpano/Smith/Irvine security type systems requires that variables are annotated as high (secret) or low (public), and provides typing rules which guarantee that secret values cannot leak to public output ports. This property of a program is called confidentiality. For a simple while-language without threads, our proof shows that typeability in the Volpano/Smith system guarantees noninterference. Noninterference means that if two initial states for program execution are low-equivalent, then the final states are low-equivalent as well. This indeed implies that secret values cannot leak to public ports. The proof defines an abstract syntax and operational semantics for programs, formalizes noninterference, and then proceeds by rule induction on the operational semantics. The mathematically most intricate part is the treatment of implicit flows. Note that the Volpano/Smith system is not flow-sensitive and thus quite unprecise, resulting in false alarms. However, due to the correctness property, all potential breaks of confidentiality are discovered.

Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Publikationstyp Zeitschriftenaufsatz
Jahr 2008
Sprache Englisch
Identifikator ISSN: 2150-914X
KITopen ID: 1000017670
Erschienen in The Archive of Formal Proofs
Heft 9
Seiten 27 S.
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft KITopen Landing Page