A new approach to information flow in sequential and parallel programs is presented. Flow proof rules that capture the information flow semantics of a variety of statements are given and used to construct program flow proofs. The method is illustrated by examples. The applications of flow proofs to certifying information flow policies and to solving the confinement problem are considered. It is also shown that flow rules and correctness rules can be combined to form an even more powerful proof system.

Interesting program properties other than functional correctness can be addressed and proved using axiomatic logic. An information flow logic that defines the flow semantics of a parallel programming language is presented. Proofs in this logic can be used to certify programs with respect to information security policies. The flow logic can also be combined with correctness logics to form an even more powerful deductive system.

Denning and Denning have shown how the information security of sequential programs can be certified by a compile-time mechanism [3]. This paper extends their work by presenting a mechanism for certifying parallel programs. The mechanism is shown to be consistent with an axiomatic description of information transmission.