DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SP.1984.10019
Joseph A. Goguen , SRI International
José Meseguer , SRI International
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.