CTSRD – Rethinking the hardware-software interface for security
|Newflash - October 2013: We have now created a BERI open-source downloads web page that includes links to the hardware specs and build instructions for our Terasic DE4-based tablet, FreeBSD OS support, test suite, and shortly, open-source Bluespec designs.|
|Newsflash - October 2013: Google has announced Capsicum for Linux, an adaptation of the Linux kernel to support Capsicum capability mode, capabilities, and process descriptors.|
|Newsflash - August 2013: We have open sourced Smten, a programming and SMT orchestration tool intended to support computer-aided verification of hardware designs, such as the CHERI processor, presented at CAV 2013|
CTSRD is a joint research project between SRI International's Computer Science Laboratory and the University of Cambridge Computer Laboratory, supported by DARPA (part of the DARPA CRASH programme) and Google. The project is revisiting the hardware-software security interface for general-purpose CPUs to fundamentally improve security; to this end, we are integrating a hybrid capability model and continuous hardware-assisted validation of security design principles with a commodity CPU ISA and open source operating systems. We are pursuing several new software/hardware features as part of this research:
- BERI: a open-source hardware-software research and teaching platform: a 64-bit RISC processor implemented in the high-level Bluespec hardware description language (HDL), along with compiler, operating system, and applications;
- CHERI: capability hardware enhanced RISC instructions : hardware-accelerated in-process memory protection and sandboxing model based on a hybrid capability model;
- TESLA: temporally enforced security logic assertions: compiler-generated runtime instrumentation continuously validating temporal security properties;
- SOAAP: security-oriented analysis of application programs: automated program analysis and transformation techniques to help software authors utilize Capsicum and CHERI features; and
- Smten: SMT-based tools to support the formal verification of processor designs implemented in Bluespec.
There is a strong interest, throughout, in judiciously applying formal methodology and bringing formally grounded techniques to mainstream hardware and software development. This work has motivated the creation of the Bluespec extensible RISC implementation – an open-source platform for research into the hardware-software interface, with a BSD-licensed operating system and toolchain based on FreeBSD and Clang/LLVM. We are using open source, wherever possible, to transition new technologies into mainstream use.
CTSRD builds on long past experience at both institutions in security and systems research, including Multics, PSOS, the Newcastle DSS, separation kernels, the DARPA CHATS programme, PVS/SAL/YICES, LynuxWorks, the CAP computer, the MAC Framework, multi-threaded CPU design, Xen, Capsicum, and MirageOS.
- New York Times, October 2012: article on Dr Peter G. Neumann regarding clean-slate research for security.
- ACM Queue, October 2012: interview with Dr Robert N. M. Watson on research into the hardware-software interface.
- IEEE Spectrum, December 2012: interview with Dr Robert N. M. Watson on clean-slate research for security.
- Peter G. Neumann, Robert N.M. Watson. CRASH PI Meeting May 2013 - CTSRD Poster. Park Ridge, NJ, May 2013.
- Peter G. Neumann, Robert N.M. Watson. CRASH PI Meeting November 2012 - CTSRD Poster. San Diego, CA, November 2012.
- Peter G. Neumann, Robert N.M. Watson. CRASH PI Meeting May 2012 - CTSRD Poster. Boston, MA, May 2012.
- Peter G. Neumann, Robert N.M. Watson. CRASH PI Meeting November 2011 - CTSRD Poster. Arlington, VA, November 2011.
- Peter G. Neumann, Robert N.M. Watson. CRASH PI Meeting May 2011 - CTSRD Poster. Palo Alto, CA, May 2010.
- Peter G. Neumann, Robert N.M. Watson. CRASH PI Meeting November 2010 - CTSRD Poster. Washington, DC, November 2010.