NSF Safe-OSE: Ensuring Trusted Computing Systems by Safeguarding the Tock Secure Embedded Operating System

University Of Virginia Main Campus, Charlottesville VA

Investigators

Abstract

Ensuring modern computing systems are secure is critical for preventing malicious adversaries from intercepting data, compromising infrastructure, and stealing intellectual property. Today’s computers rely on dedicated security chips as the foundation for overall system-level security. Increasingly, vendors are using the Tock operating system on these chips because Tock solves a key need in this industry: secure and reliable software. The security of computing devices (e.g., datacenters, laptops, and smartphones) then ultimately relies on Tock’s correctness and robustness, and Tock’s development ecosystem must remain trustworthy and resistant to compromise. This project will develop new techniques to ensure that malicious attackers cannot introduce covert flaws into the Tock project that would undermine the robustness and security of the operating system. This project will provide layered defenses against increasingly patient and capable adversaries using techniques including automated robustness analysis of software dependencies; compatibility checkers between hardware, the operating system, and applications; and open-source contribution review aids. In addition to ensuring Tock remains a trusted platform for security chips, these advancements could be generalized to support the robustness of other high-assurance software projects. Vendors rely on Tock because it is implemented in a memory-safe language (Rust), provides robust isolation and least-privilege guarantees, and is open-source. However, as an embedded operating system, Tock must support and directly interface with numerous hardware platforms while meeting resource constraints. These requirements mean that existing system-, software-, and language-level features for reliability and correctness are inadequate, and a large contributor base is needed to support diverse hardware platforms. This makes Tock susceptible to covert development attacks targeting the software supply chain, the trusted-computing-base, and the open-source code review practices for low-level systems code. This project will develop mechanisms to protect the Tock open-source project. These include detectors for unsafe and unsound code in Tock and its dependencies, automatic generation of system call interfaces that prevents exploitable incompatibilities between user space and the kernel, and code trust tiers to guide manual code review scrutiny to critical components. These defenses will enhance the guarantees of using a memory-safe language for low-level code while addressing weaknesses in the open-source contribution model. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.