Summary
Developing software that runs securely on specialized Armv8-M chips can be tricky because the secure and non-secure parts need to share hardware components without conflicts. The authors created MicroHasTEE, a tool that uses the Haskell programming language to let these parts be written together safely in one program, preventing errors that only show up when the software runs. It tracks which software part owns which hardware resource and stops mistakes like using the wrong device or calling a service incorrectly. Their system can produce separate secure and non-secure firmware images that work correctly on real hardware. They demonstrated this with a smart door-lock example.
What this means in practice
- •For embedded systems developers: Create secure and non-secure firmware for Armv8-M devices with guaranteed correct access and control over hardware peripherals.
- •For iot device makers: Build trustworthy embedded software for connected devices that isolates secure functions from non-secure ones to improve safety.
Abstract
Arm TrustZone for Armv8-M isolates Secure and Non-secure software, but developers must still coordinate peripheral attribution, interrupt routing, initialization, and gateway interfaces across separately built firmware images. Inconsistent assumptions between these images can compile successfully and emerge only as faults on the target device. We present MicroHasTEE, a multiparty programming framework that expresses both firmware applications as participants in one typed Haskell program. MicroHasTEE represents peripheral authority with type-level capability ledgers and uses indexed setup computations to track resource acquisition, configuration, transfer, and finalization. Domain-specific effect types restrict peripheral operations and interrupt callbacks to the participant that holds the corresponding authority, while typed callable handles describe the Secure services available to Non-secure code. MicroHs compiles the shared program twice to produce separate bare-metal Secure and Non-secure firmware images. We implement MicroHasTEE for an STM32U5 Nucleo board, including TrustZone configuration, peripheral drivers, and a serialized gateway for cross-domain Haskell calls. For programs expressed through its interface, MicroHasTEE rejects inconsistent resource use, attribution changes after configuration, callbacks in the wrong domain, and calls to unregistered Secure services. A door-lock case study demonstrates feasibility, with firmware images occupying 232.7 KiB and 228.4 KiB of flash and approximately 220 KiB of SRAM per domain.