• dynamic enforcement
• dynamic policies
• facets of dynamic policies
• Haskell
• information flow control
• knowledge based security
• non-interference

Information flow control (IFC) is a set of techniques for securing computing systems. It ensures the secure propagation of information through program execution and prevents unwanted leaks.
In those techniques, the security is formally expressed by a security property that the system is guaranteed to enforce.
Non-interference is the core security property for IFC. It states that two runs of the same program with different secret inputs should result in the same public observation.
Mechanisms that enforce security properties can be static or dynamic. In the static case, the type system is usually used to enforce the property. Instead, for the dynamic ones, a monitor tracks information at runtime, and the language's semantics guarantees security.
Information flow policies are used to model the security level of information and its propagation.
Usually, these policies use labels to represent security levels so that any information has its own. Then they define a relation to express how data can flow from one label to another.
We call dynamic those policies that allow to change at runtime, either the label assigned to some information or the flow relations.
Non-interference, though, is too restrictive in these dynamic contexts. For example, it doesn't allow for declassification, i.e., a decrease in the sensitivity of the information, since it doesn't allow any flow from the secret to the public level.
Knowledge-based security conditions supersede non-interference and can be used with dynamic policies. They are formulated based on the knowledge (information) that an attacker at a security level is able to gather. In this way, one can check that the attacker is only learning what it is allowed to do by the policy.
Those dynamic contexts are also not trivial to model with policies. This is because different interpretations of secure or insecure contexts may arise depending for instance on the semantics that one uses for dynamic policies definition. We call those interpretations facets and list some of them with examples.
Usually, the enforcing mechanisms do not allow the user to choose between different interpretations.
We present DypLIO, which is a Haskell enforcement mechanism for dynamic policies that allows the user to choose different interpretations of two facets called time-transitive and replaying flow.
The time-transitive flows arise when information moves from level A to level C via a third level B, and there is no moment in time where A can flow to C.
A replaying flow instead consists of a release of information that can be repeated.
In this system, the user assigns a label to data, and a monad tracks the policy state and access to information to prevent leaks.
The resulting DypLIO is parametrized on the label type, the state implementing the dynamic policy, and the state used to track replaying flows.
This work shows how we designed and implemented the facets in DypLIO. We present the formalization of the language and prove that the semantics is progress-insensitive secure. As a final contribution, we also provide the current state of the mechanization of the security proof in LiquidHaskell.