Semantics of noninterference: a natural approach
Peter W. O’Hearn · 1992
This thesis examines noninterference in imperative Algol-like languages. Noninterference is fairly well understood for simple phrases (like commands) that can be executed directly: two simple phrases don't interfere iff the evaluation or execution of one has no effect on the other. But procedures are not as straightforward because they must be supplied with arguments before being executed. The subtlety for procedural noninterference arises the need to distinguish between interference that is a result of using arguments to a call and interference that is attributable to the procedure itself. Because of this subtlety, previous semantical approaches to noninterference suffer various anomalies. We use functor categories to develop a semantics of noninterference that correctly deals with procedures. Naturality is used to detect interference that comes from a procedure instead of an argument. The semantics is used to study Reynolds' specification logic and syntactic control of interference. For specification logic (a Hoare logic for Algol-like languages), the main results involve the soundness of axioms whose validity has not previously been established, due to the above-mentioned problems involving procedures. This extends previous work of Tennent. For syntactic control of interference, we develop a model that demonstrates the correctness of syntactical restrictions that are used to control interference (e.g. to banish aliasing).