CRASH-Worthy, Trustworthy Systems R&D
SRI and the University of Cambridge are designing, prototyping, and analyzing computer systems that can be gradually adopted with high reliability, resilience, and assurance, effectively letting developers ‘wipe the slate clean' in incremental steps.
Together with the University of Cambridge Computer Laboratory, SRI is developing an incrementally adoptable computer security system platform, under the Defense Advanced Research Projects Agency's Clean-slate design of Resilient, Adaptive, Survivable Hosts (CRASH) program.
Called CRASH-worthy Trustworthy Systems Research and Development (CTSRD), the high-performance platform is robust and programmer-friendly. The platform can enhance data protection, fault tolerance, and system resilience, plus reduce risk from malicious behavior. Intended to support a variety of applications, the hardware-software solution includes a number of formally supported assurance and protection principles. For example, it can restrict access to only what is essential for a given program, following the principle of least privilege.
CTSRD's resulting systems will enable existing operating systems and applications to execute securely while at the same time supporting evolutionary adoption of advanced security features. This hybrid strategy involves development of new security-oriented capability-based hardware, trustworthy low-layer hypervisor software, and high-risk applications.
For efficient software implementation, two major components reinforce the software security and design: Capability Hardware Enhanced RISC Instructions (CHERI) and Temporally Enforced Security Logic Assertions (TESLA).
CHERI allows incremental adoption of higher-assurance approaches, with a focus on security-critical components. At each system layer, hardware capability semantics may be selected to support different risk-protection approaches, such as high-assurance design (for separation kernel and type-safe language runtimes) or hybrid models that blend traditional virtual addressing with capability operation (for commodity kernels and applications).
TESLA adapts techniques of static model checking into dynamically executed run-time software assertions that are evaluated on the fly. Programmers may represent these assertions as simple temporal properties, which are mapped into explicit automata.
The researchers expect to achieve short-term sufficiently secure backward compatibility with legacy software, along with longer-term migration of these and new applications to the high-assurance capabilities.
This University of Cambridge website includes open-source code for the CHERI hardware and system architecture, CheriBSD, CHERI Clang/LLVM, TESLA, Smten, SOAAP, and recent PI meeting slides and poster.