- You are subscribed to this talk through .
- You are watching this talk through .
- You are subscribed to this talk. (unsubscribe, watch)
- You are watching this talk. (unwatch, subscribe)
- You are not subscribed to this talk. (watch, subscribe)
The CRASH/SAFE project is building a network host that is highly resilient 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.
Benjamin Pierce is Henry Salvatori Professor of Computer and Information Science at the University of Pennsylvania and a Fellow of the ACM. 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.
He serves as co-Editor in Chief of theJournal of Functional Programming, as Managing Editor for Logical Methods in Computer Science, and as editorial board member of Mathematical Structures in Computer Science and Formal Aspects of Computing. He is also the lead designer of the popular Unison file synchronizer.