Certifying Information Flow Properties of Programs: An Axiomatic Aproach
Gregory R. Andrews, Richard P. Reitman · 1978
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 even more powerful deductive systems. Keywords and phrases: Information flow, computer security, policy certification, program validation, proof rules, concurrency, synchronization.