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