Msb Associates STTR Phase II Award, August 2021

Continuing advances in solid state storage technology have enabled detachable storage devices that are inexpensive, high bandwidth and high capacity, making them practical for sharing even large amounts of data among devices that need not be networked.  For this reason, they are very attractive as a mechanism for secure data storage as well as transfer. Unfortunately the current generation of memory sticks expose risks that make them unsuitable for use by US government agencies. The primary concern with these devices is the attack surface presented by the micro-controller that is required to present the storage as a USB peripheral to the host operating system. Exploits have been demonstrated in which an attacker could, with brief physical access to a memory stick, reprogram its firmware so as to enable arbitrary privilege escalation on a host operating system without needing to exploit an OS-level software vulnerability.  A reprogrammed storage device could exploit the USB protocol, which multiplexes many physical devices on logical channels and permits devices to negotiate registration (and re-registration), to masquerade as a keyboard for long enough to capture the root password via physical keystrokes.  The flash can be reprogrammed with a laptop, making tamper-resistant designs ineffective. We describe the first year of work designing and implementing a secure operating system for memory sticks that is correct-by-construction as well as amenable to formal verification.  Several key features of Twizzler make it ideally suited to the task. It structures memory---whether persistent or volatile---into coarse grained objects that are the units of access control, reducing both the number and variety of access policies that must be considered when deploying the OS. Comprising only 5K lines of code and exposing only 20 system calls to user-space, Twizzler exposes a minimal attack surface and is small enough to be a reasonable target for embedded architecture as well as for systematic verification. Moving the kernel out of the I/O path, it exposes the raw I/O latency and bandwidth  of the memory to programs. To transform Twizzler into an appropriate target for detachable storage micro-controllers requires a research and development effort along three distinct but interrelated lines: Guaranteeing via a flat permission model with no superuser role, in which cryptographically signed capabilities persistently encode access rights. Providing isolation of untrusted code both within and across threads of control via \emph{security contexts} that subsume UNIX roles, and  gated APIs that subsume system calls and IPC, providing fine-grained control of privileges without escape hatches. Ensure secure boot and integrity of trusted components via unforgeable, content-derived naming.