A security types preserving compiler in Haskell

Alberto Pardo

Instituto de Computación
Universidad de la República
Montevideo

Thursday, 20 May 2010, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: We show the main aspects of a compiler, written in Haskell, which preserves the property of noninterference between a simple imperative language and structured machine code with loop and branch primitives. The compiler is based on the use of typed abstract syntax (represented in terms of GADTs and type families) both for the source and target language. In this case typed abstract syntax is used to model the type system for noninterference of each language where types correspond to security types. This makes it possible to use Haskell's type checker to verify two things: that programs enforce security restrictions, and that the compiler is correct -in the sense that it preserves security restrictions- by construction.

Joint work with Cecilia Manzino from Universidad Nacional de Rosario, Argentina.

ERDF
Tarmo Uustalu
Last update 3 June 2010