Algorithmic Trace Effect Analysis, David Van Horn. August 2005. [ PDF ]

Trace effect analysis is a programming language analysis for ensuring correct and secure behavior of software with respect to so-called temporal properties of programs. Temporal properties express the well-ordering of program events, such as when files are opened or when resources are obtained. By enforcing program event order specifications, we can ensure that files are opened before being read, or that privilege activation occurs before privileged resources are acquired. In general, the ability to enforce temporal properties in programs allows a wide variety of safety and security guarantees to be made about software.

Further, this analysis is performed automatically at compile time, i.e. it takes place before program execution occurs, leading to the earlier detection of errors. A consequence of such compile time, aka static reasoning, is that if a program is deemed correct by the analysis, it will never violate its specification at run time, ensuring safe program behavior in all possible circumstances of program execution.

Common security mechanisms such as stack inspection, found in the Java programming language and .NET framework, are enforced via run time inspection of the sequence of events occurring up to the point of the inspection. These mechanisms are formalizable within trace effect analysis and thus can be enforced at compile time, implying all run time inspections are superfluous and can be eliminated. Any run time overhead associated with enforcing the security mechanism can therefore also safely be eliminated.

Our analysis consists of a program logic (a system of axioms and deduction rules) such that if a program has a derivable logical judgment, the program meets its temporal specification.

Additionally we have defined an algorithm for discovering such a judgment for a program. This algorithm has been proved sound, which is to say any judgment found by the algorithm is a valid logical judgment and represents a proof that the program meets its specification. This proof discovery procedure has been implemented for a foundational programming language with notions of atomic events, temporal assertions, and computational traces (sequences of events).