Projet Everest
INRIA Sophia Antipolis
Monday, 12 April 2004, 14:00 (note the unusual weekday!)
Cybernetica Bldg (Akadeemia tee 21), room B101
Abstract: Initiating from the seminal work of Volpano and Smith, there has been sample evidence that type systems may be used to enforce confidentiality of programs through non-interference. However, most type systems operate on high-level languages and calculi, and low-level languages have not received much attention in studies of secure information flow. Further, security type systems for low-level languages should appropriately relate to their counterparts for high-level languages; however, we are not aware of any study of type-preserving compilers for type systems for information flow.
In answer to these questions, we introduce a security type system for a low-level language featuring jumps and calls, and show that the type system enforces termination-insensitive non-interference. Then, we introduce a compiler from a high-level imperative programming language to our low-level language, and show that the compiler preserves security types.
(Joint work with Gilles Barthe and Amitabh Basu.)