A Haskell-Embedded DSL for Secure Information-Flow

• Cecilia Manzino Universidad Nacional de Rosario
• Gonzalo de Latorre Universidad Nacional de Rosario

Resumo

This paper presents a domain specific language, embedded in Haskell (EDSL), for enforcing the information flow policy Delimited Release. To build this language we use Haskell extensions that will allow some kind of dependently-typed programming. Considering the effort it takes to build a language from scratch, we decided to provide an information-flow security language as an EDSL, using the infrastructure of the host language to support it. The decision of using Haskell as the implementation language is because it has a powerful type system that makes it possible to encode the security type systems of the embedded language at the type level and also because it is a general purpose language. The implementation follows an approach where the type of the abstract syntax of the embedded language was decorated with security type information. This way, typed programs will correspond to secure programs, and the verification of the security invariants of programs will be reduced to type-checking. The embedded security language is designed in a way that is easy to use. We illustrate its use through two examples: an electronic purchase and a secure reading of database information.

Palavras-chave: dependently-typed programming, Haskell, information flow type systems, declassification