Design and implementation of facets of dynamic policies
In Information Flow Control (IFC) expressiveness, i.e. being able to model multiple scenarios, is a crucial aspect, especially in the context of dynamically evolving security requirements. Those dynamic scenarios introduce complexities due to varying security interpretations. Broberg et al. identified “facets of dynamic policies”, patterns of information flow that may be considered secure or insecure depending on the context. Typically, most existing definitions of security conditions do not delve into the analysis of these facets, making it difficult to model a wide range of scenarios. Therefore, our research aims to establish a robust framework that facilitates the design and implementation of the different interpretations of facets within a single, modular enforcement mechanism. We propose, in Haskell, an abstract definition of a monadic IFC mechanism, that, based on the instantiation, can account for the different interpretations of facets. Our ongoing work involves the formalization of the respective security conditions, the study of their combination and a LiquidHaskell proof mechanization. This with the aspiration to improve the reasoning about dynamic policies and their associated facets, especially in the case of future extensions.