Skip to main content

Seminar:  The SAFE Machine: An Architecture for Pervasive Information Flow

Date:January 13, 2014 
Talk Title:The SAFE Machine: An Architecture for Pervasive Information Flow
Speaker:Benjamin Pierce, Professor, University of Pennsylvania
Time & Location:12:00pm - 1:00pm

Abstract

The CRASH/SAFE project is building a network host that is highly resiliant to cyber-attack. One pillar of the design is pervasive mechanisms for tracking information flow. At the lowest level, the SAFE hardware offers fine-grained tagging and efficient support for propagating and combining tags on each instruction dispatch. The operating system virtualizes these generic facilities to provide the information-flow abstract machine on which user programs run. In this talk, we'll take a guided tour of (a simplified model of) the SAFE hardware and software and an end-to-end proof of noninterference for this model.

Speaker Bio

Benjamin Pierce is Henry Salvatori Professor of Computer and Information Science at the University of Pennsylvania. His research centers on programming languages, static type systems, language-based security, computer-assisted proof, concurrent and distributed programming, and synchronization technologies. His books include the widely used graduate texts Types and Programming Languages and Software Foundations, a 100% machine-checked textbook on the theory of programming languages. He is also the lead designer of the popular Unison file synchronizer.