Concepedia

TLDR

The paper discusses two main ideas: unwinding and inference control. Both unwinding and inference control are computer security concepts that are not closely related, with inference control aiming to prevent unauthorized inference from authorized data. Unwinding is a verification technique based on noninterference assertions, and the paper also treats secure interfaces using similar assertions. The main result is an unwinding theorem providing a simple necessary and sufficient condition for a system to satisfy the MLS security policy.

Abstract

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.