Proving Noninterference and Functional Correctness Using Traces
John McLean · Journal of Computer Security · 1992
The trace method of software specification is extended to provide a natural semantics for a procedural programming language. This extension provides a method for proving program correctness that permits a direct proof of program Noninterference witho