Paralocks in the Haskell type system
Information flow control can be achieved through static (i.e. compile time) or dynamic (i.e. runtime) enforcement.
Static enforcement has many benefits; errors are caught before deployment, and typically no runtime overhead is added.
However, to achieve static control, existing solutions typically implement a full type-checker, a practice that is rather
As an interesting alternative, seclib [1,2] implements static information flow control in GHC Haskell by
cleverly utilizing the type system. No separate type-checker is needed, and the whole solution can be presented as
a library, an EDSL. The drawback with SecIO, however, is that the policies that can be expressed at the type level
are very basic - too basic for practical use.
Paralocks  is a rich language for expressing information flow policies. It (or variants thereof) has been used
previously in Paragon [4,5], which uses a full type-checker solution; and in SLIO  which performs dynamic enforcement
This project would investigate the feasibility of implementing an enforcement of Paralocks (or a variant thereof)
using the SecIO approach, by implementing the enforcement mechanism using the advanced type system mechanisms found in GHC Haskell.