Paralocks in the Haskell type system

Potential supervisors: 
Description: 

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
heavy-weight. 

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 [3] 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 [6] which performs dynamic enforcement
in Haskell.

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.

[1] https://hackage.haskell.org/package/seclib-1.1.0.2
[2] http://www.cse.chalmers.se/~russo/seclib.htm
[3] http://www.cse.chalmers.se/research/group/paragon/publications/BS10.pdf
[4] http://www.cse.chalmers.se/research/group/paragon/
[5] http://www.cse.chalmers.se/research/group/paragon/publications/BDS13.pdf
[6] http://www.cse.chalmers.se/~buiras/publications/plas2015.pdf