UCCA: A Verified Architecture for Compartmentalization of Untrusted Code Sections in Resource-Constrained Devices
Liam Tyler, Ivan De Oliveira Nunes
TL;DR
UCCA presents a hardware-based Untrusted Code Compartment Architecture that isolates untrusted code regions on resource-constrained MCUs using a parallel hardware monitor. The design is formally verified with Linear Temporal Logic (LTL) specifications by translating Verilog FSMs to SMV and checking against NuSMV, ensuring Return Integrity, Stack Integrity, and CR integrity. Implemented on an open MSP430-based platform, UCCA demonstrates low run-time overhead, supports interruptible UCCs, and incurs modest hardware, energy, and memory costs that scale linearly with the number of UCCs. The work shows that tight, formally verified isolation of untrusted code is practical for low-end MCUs and can complement existing MPU/TrustZone approaches to reduce the trusted computing base and mitigate run-time exploits in safety- and time-critical embedded systems.
Abstract
Micro-controller units (MCUs) implement the de facto interface between the physical and digital worlds. As a consequence, they appear in a variety of sensing/actuation applications, from smart personal spaces to complex industrial control systems and safety-critical medical equipment. While many of these devices perform safety- and time-critical tasks, they often lack support for security features compatible with their importance to overall system functions. This lack of architectural support leaves them vulnerable to run-time attacks that can remotely alter their intended behavior, with potentially catastrophic consequences. In particular, we note that MCU software often includes untrusted third-party libraries (some of them closed-source) that are blindly used within MCU programs, without proper isolation from the rest of the system. In turn, a single vulnerability (or intentional backdoor) in one such third-party software can often compromise the entire MCU software state. In this paper, we tackle this problem by proposing, demonstrating security, and formally verifying the implementation of UCCA: an Untrusted Code Compartment Architecture. UCCA provides flexible hardware-enforced isolation of untrusted code sections (e.g., third-party software modules) in resource-constrained and time-critical MCUs. To demonstrate UCCA's practicality, we implement an open-source version of the design on a real resource-constrained MCU: the well-known TI MSP430. Our evaluation shows that UCCA incurs little overhead and is affordable even to lowest-end MCUs, requiring significantly less overhead and assumptions than prior related work.