Institut für Informatik
Ludwig-Maximilians-Universität München
Tuesday, 11 December 2007, 11:00 (note the unusual weekday and time!)
Cybernetica Bldg (Akadeemia tee 21), room B101
Slides from the talk [pdf]
Abstract: Non-interference is a base-line security property of systems which stipulates that secret data cannot influence publicly visible output of a system. In the talk, we will summarise a popular approach to ensure non-interference of simple imperative programs using type systems, and then present a type system that applies at the bytecode level. In contrast to previous type systems, the our calculus applies not only to code resulting from structure-preserving compilation from a high-level language, but to unstructured code, and is compatible with local low-level program transformations. This flexibility is obtained by exposing the relational nature of non-interference (i.e.the fact that its formulation involves two executions of a program for different initial secret data), and the tracking of value identities throughout a pair of computations, instead of tracking formal variable dependencies.