Abstract
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 without having to produce an intermediate finite state machine and unwinding conditions. This approach provides a uniform framework for reasoning about abstract software system specifications and their implementations. It also allows us to prove security at an abstract level so that changes to programs that do not affect functional behavior will not affect the security proof.
Get full access to this article
View all access options for this article.