Operating R.S. Gaines Systems Editor Certification of Programs for Secure Information Flow

This paper presents a certification mechanism for verifying the secure flow of information through a pro-gram. Because it exploits the properties of a lattice structure among security classes, the procedure is suf-ficiently simple that it can easily be included in the analysis phase of most existing compilers. Appropriate semantics are presented and proved correct. An impor-tant application is the confinement problem: The mechanism can prove that a program cannot cause supposedly nonconfidential results to depend on confi-dential input data