Dynamic Enforcement of Dynamic Policies

This paper presents SLIO, an information-flow control mechanism enforcing dynamic policies: security policies which change the relation between security levels while the system is running. SLIO builds on LIO, a floating-label information-flow control system embedded in Haskell that uses a runtime monitor to enforce security. We identify an implicit flow arising from the decision to change the policy based on sensitive information and introduce a corresponding check in the enforcement mechanism. We provide a formal security guarantee for SLIO, presented as a knowledge-based property, which specifies that observers can only learn information in accordance with the level ordering. Like LIO, SLIO is a generic enforcement mechanism, parametrised on the concrete instantiation of security labels and their policy change mechanism. To illustrate the applicability of our results, we implement well-known label models such as DLM, the Flowlocks framework, and DC labels in SLIO