Organick Lecture Series
Peter Neumann
Principal Scientist
SRI International
Wednesday, March 27, 2013
102 lower WEB
Reception 3:20 p.m.
Lecture 3:40 p.m.
Title: Clean-Slate Formally Motivated Hardware and Software for Highly Trustworthy Systems
Peter Neumann
Principal Scientist
SRI International
Wednesday, March 27, 2013
102 lower WEB
Reception 3:20 p.m.
Lecture 3:40 p.m.
Title: Clean-Slate Formally Motivated Hardware and Software for Highly Trustworthy Systems
Abstract
This talk examines an ongoing joint project at SRI and the University of Cambridge for the DARPA CRASH program (Clean-slate Resilent, Adaptive, Secure Hosts), and -- as time permits -- a companion project for the DARPA MRC (Mission-oriented Resilient Cloud) program. The first project involves the development, implementation, and formal analysis of a tagged/typed capability-based architecture for the hardware, FPGA-based hardware specified in the Bluespec hardware definition language (with modules, abstraction, and types), a highly principled software development appproach with hardware-aware separation kernel virtual machine hypervisors, and capabiity-aware programming language extensions. The hybrid architecture enables the coexistence of suitably sandboxed legacy code with highly trustworthy system and application code -- without adverse interference. The developed systems are also being used to pursue trustworthy Software Defined Networking and trustworthy servers for the companion project. (The previous evening's talk is not a prerequisite; however, it is expected that duplication will be relatively minimal.)
This talk examines an ongoing joint project at SRI and the University of Cambridge for the DARPA CRASH program (Clean-slate Resilent, Adaptive, Secure Hosts), and -- as time permits -- a companion project for the DARPA MRC (Mission-oriented Resilient Cloud) program. The first project involves the development, implementation, and formal analysis of a tagged/typed capability-based architecture for the hardware, FPGA-based hardware specified in the Bluespec hardware definition language (with modules, abstraction, and types), a highly principled software development appproach with hardware-aware separation kernel virtual machine hypervisors, and capabiity-aware programming language extensions. The hybrid architecture enables the coexistence of suitably sandboxed legacy code with highly trustworthy system and application code -- without adverse interference. The developed systems are also being used to pursue trustworthy Software Defined Networking and trustworthy servers for the companion project. (The previous evening's talk is not a prerequisite; however, it is expected that duplication will be relatively minimal.)