Providing Integrity Policies as a Library in Haskell

    This work describes an extension made to a security library in Haskell that guarantees confidentiality (i.e. that secrets are not leaked). The existence of this library is possible due to Haskell's strong type checker and controlled side-effects. This security library uses monads with type parameters to indicate security levels. The monad guarantees that once data is inside of it, there is no way of getting it out. More precisely stated, the monad can be used to enforce information-flow policies for confidentiality.

    This work shows that integrity policies (i.e. policies that avoids data from being intentionally or unintentionally destroyed) can be incorporated as well, and thus defining a richer set of security policies. More precisely, the kind of integrity policies that are incorporated are access control, data invariants and information-flow integrity policies. Access control is implemented using a wrapper data type to define permissions for resources (a variation of an access-control list (ACL)), and uses a security lattice for permissions. Data invariants are enforced at end points (inputs and outputs to a program). This is done by extending the data types for files and checking that the property holds, when an input or output operation is performed. Information-flow integrity policies reuses the same techniques that enforce confidentiality, by simply extending the security lattice with integrity levels.

    Confidentiality and integrity are two key aspects of information security, and by incorporating both in a light-weight library, we seek to increase the use of language-based security when writing security critical applications.

    A Password Administrator is used as an interesting case study. The case study is organized in the modules Login, for authenticating, Reset, for changing passwords, and Backup for backing up and restoring passwords. This application involves confidentiality policies as well as the different integrity policies described above.

  • The master thesis can be downloaded here