Certification of Programs for Secure Information Flow This paper presents a certification mechanism for verifying the secure flow of information through a program. Because it exploits the properties of a lattice structure among security classes, the procedure is sufficiently simple that it can easily be included in the analysis phase of most existing compilers. Appropriate semantics are presented and proved correct. An important application is the confinement problem: The mechanism can prove that a program cannot cause supposedly nonconfidential results to depend on confidential input data. CACM July, 1977 Denning, D. E. Denning, P. J. protection, security, information flow, program certification, lattice, confinement, security classes 4.3 4.35 5.24 CA770707 JB December 28, 1977 8:48 AM 1807 4 2945 2034 4 2945 2290 4 2945 2579 4 2945 2923 4 2945 2945 4 2945 2945 4 2945 2945 4 2945 3128 4 2945 3150 4 2945 1947 5 2945 2704 5 2945 2870 5 2945 2945 5 2945 2945 5 2945 2945 5 2945