Unwinding and Inference Control

This paper discusses two main ideas, unwinding and inference control. While both concern computer security, they are not closely related to each other. Unwinding is a verification technique for general security requirements based on noninterference assertions as in Goguen & Meseguer 82a. The inference control problem concerns preventing inference of unauthorized information by combining authorized information. The main result in this paper is an unwinding theorem that gives a very simple necessary and sufficient condition for a system to satisfy the MLS security policy system. A subsidiary topic is secure interfaces, which we show how to treat with noninterferce assertions.