MicroHasTEE：面向Armv8-M的裸机Haskell类型级外设所有权

中文摘要 AI 辅助

Arm TrustZone for Armv8-M隔离了安全与非安全软件，但开发者仍必须跨独立构建的固件镜像协调外设归属、中断路由、初始化及网关接口。这些镜像之间不一致的假设可能编译成功，却仅在目标设备上以故障形式显现。我们提出MicroHasTEE，一个多方编程框架，将两个固件应用表达为单个类型化Haskell程序中的参与者。MicroHasTEE用类型级能力账本表示外设权限，并使用索引设置计算来跟踪资源获取、配置、转移和终结。领域特定效应类型将外设操作和中断回调限制为持有相应权限的参与者，而类型化可调用句柄描述非安全代码可用的安全服务。MicroHs两次编译共享程序，生成独立的裸机安全与非安全固件镜像。我们在STM32U5 Nucleo板上实现了MicroHasTEE，包括TrustZone配置、外设驱动及用于跨域Haskell调用的序列化网关。对于通过其接口表达的程序，MicroHasTEE拒绝不一致的资源使用、配置后的归属变更、错误域中的回调以及调用未注册的安全服务。一个门锁案例研究证明了可行性，固件镜像占用232.7 KiB和228.4 KiB闪存，每个域约220 KiB SRAM。

英文摘要

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.

发表机构

• Chalmers University of Technology（查尔姆斯理工大学）
• The University of Gothenburg（哥德堡大学）

机构由 AI 辅助整理，请以论文原文为准。