@article{certification-sec-info-flow,
 author = {Dorothy E. Denning and Peter J. Denning},
 title = {Certification of programs for secure information flow},
 journal = {Commun. ACM},
 volume = {20},
 number = {7},
 year = {1977},
 issn = {0001-0782},
 pages = {504--513},
 doi = {http://doi.acm.org/10.1145/359636.359712},
 publisher = {ACM Press},
 address = {New York, NY, USA},
 abstract = {
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. 
 },
 notes = {
"Information flow control" is a procedure for regulating the dissemination of data amongst program objects. Program objects are assigned to security classes (e.g. top-secret, secret, public) and a policy is represented by a relation between these classes. A "flow" is only allowed to exist between x and y (i.e. the value of y is influenced by x) if (class(x),class(y))\in policy-relation.
<p>
This paper proposes a compile-time mechanism for checking programs against information flow policies. Once certified, security policy breaches can only occur through out-of-band mechanisms e.g. faulty or sabotaged hardware or unmodelled communication through covert channels. Quite an old paper but well-worth reading. In particular the discussion of what constitutes a flow between two variables is interesting. Obviously the assignment 
<pre>
  x <- y
</pre>
causes a flow from y to x. But more subtle flows are also possible eg:
<pre>
  x <- 0;
  while (y > 0) do
    x <- x + 1;
    y <- y - 1;
  done
</pre>
},
 bibtexurl = {http://www.recoil.org/~djs/bibtex/certification-of-progs-sec-info-flow.bib},
 pdf = {\url{http://www.cs.cornell.edu/andru/cs711/2003fa/reading/denning77.pdf}},
 }