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.