MicroHasTEE: Bare-Metal Haskell for Type-Level Peripheral Ownership on Armv8-M

CCS Concepts

• The classifications cover embedded software, hardware security, embedded systems security, functional languages, and type structures.They also include the broader categories of computer systems organization and software and its engineering.Source: CCS Concepts · p. 1

Keywords

• The keywords include Haskell, Armv8-M, TrustZone-M, type-level programming, peripheral attribution, and microcontrollers.They also list TrustZone, embedded systems, functional programming, and MCU.Source: Keywords · p. 1

1 Introduction

• Separate firmware images can each type-check despite conflicting resource assumptions, leaving many mismatches to appear as faults on the target device.TrustZone-M hardware enforces configured boundaries but cannot determine whether the two applications agree about them.Source: §1 · p. 1
• MicroHasTEE’s approach complements Trusted Firmware-M by deriving both images from one typed program instead of separate partition manifests and programs.Trusted Firmware-M is described as the reference implementation of the Platform Security Architecture’s Secure Processing Environment for Armv8-M and Armv8.1-M.Source: §1 · pp. 1–2
• MicroHasTEE expresses Secure and Non-secure applications as participants in one Haskell program, then compiles it separately for each state.Each image includes the MicroHs runtime and runs bare metal; a small C layer supplies startup and raw peripheral access.Source: §1 · p. 2
• A shared account lets the type checker verify participants’ resource use, resource transfers, and calls to Secure functions exposed to Non-secure code.Disagreements become compile-time errors rather than faults discovered after deployment.Source: §1 · p. 2
• The guarantees cover operations expressed through MicroHasTEE, not arbitrary C or FFI code that directly accesses peripherals or modifies security registers.Other TrustZone-M targets require sufficient memory, a correctly established memory partition, and a backend for supported attribution operations.Source: §1 · p. 2

2.1 Memory Partitioning

• TrustZone-M places Secure and Non-secure images in disjoint flash and SRAM regions, with an NSC subregion reserved in Secure flash for gateway veneers.The linker scripts specify this layout but do not enforce hardware security attributes; disagreement with startup configuration can fault when affected memory is accessed.Source: §2.1 · p. 2, Figure 1 · p. 4

2.2 Peripheral Attribution with the GTZC

• On STM32, the GTZC’s TZSC assigns peripheral security attributes, and a Non-secure attribution permits Non-secure access rather than granting exclusive ownership.GPIO ports can attribute individual pins, while only Secure software can change those attributes.Source: §2.2 · p. 3

2.3 Interrupt Attribution

• Peripheral attribution does not set interrupt routing: the NVIC target and, on STM32, source attribution and the Non-secure vector entry must also agree before enabling an interrupt.Releasing a GPIO pin alone is insufficient; inconsistent EXTI, NVIC, or vector settings can deliver an event to the wrong state or an unsuitable handler.Source: §2.3 · p. 3

2.4 Non-secure Callable Functions and Gateway Veneers

• A Secure entry function is reached through an NSC gateway veneer: SG enters Secure state, and BXNS returns to the Non-secure caller.Secure and Non-secure images link separately but not independently: the Secure link generates the import library and veneer addresses needed by the Non-secure link, while the linker does not verify matching declarations’ types. Secure code must validate Non-secure pointer ranges and copy input before later processing.Source: §2.4 · pp. 3–4, Figure 2 · p. 4

2 Conventional Bare-Metal TrustZone-M Development

• The difficulty lies in making separate hardware and software mechanisms agree on one security policy across the two firmware images.A Non-secure button handler calling a Secure service involves peripheral and interrupt attribution, a vector entry, matching declarations, a gateway veneer, and an ordered build.Source: §2 · p. 2, §2.4 · p. 4

• TrustZone-M provides run-time isolation from compromised Non-secure firmware, while MicroHasTEE’s type system detects configuration inconsistencies introduced by a trusted but fallible developer.Source: §3 · p. 4
• The adversary may execute arbitrary Non-secure code, modify Non-secure memory, use Non-secure peripherals, and invoke NSC gateways with arbitrary pointers and messages.The model assumes the adversary cannot modify Secure firmware or attribution, directly access Secure resources, or enter Secure code outside designated gateways.Source: §3 · p. 4
• For public-interface programs, the type system checks resource transfers and use, callback placement, and callable-service registration, and prevents attribution changes after lock_configuration.These guarantees exclude raw C, foreign-function calls, and internal modules; ledgers express software authority, not exclusive hardware access.Source: §3 · p. 4
• The guarantees assume matching setup operations in the same order and correctness of MicroHasTEE, its backend, gateway, toolchain, runtime, and hardware.Malformed gateway messages are outside static typing but remain in the run-time threat model; physical attacks, fault injection, side channels, invasive debugging, rollback, denial of service, and trusted-computing-base faults are excluded.Source: §3 · p. 4

• One multiparty program describes both participants’ computations, resource assignments, and permitted interactions, and MicroHs compiles it separately for each TrustZone domain.Each build executes its own participant’s computations and uses placeholders for the other participant; linker scripts and Secure startup establish fixed flash and SRAM partitions before setup.Source: §4 · p. 5
• Type-level capability ledgers for both participants index Setup computations, tracking resource authority before and after each setup operation.Public attribution operations update hardware configuration and the corresponding ledger pair; under the stated backend and interface assumptions, the final ledgers describe the established attribution.Source: §4 · p. 5
• Setup locks configuration before callback installation or Secure-service registration, preventing later attribution changes from invalidating ledger-based checks.Configuration operations require Unlocked, while callback and service registration require Locked; lock_configuration changes the type-level setup state, not the hardware.Source: §4 · pp. 5–6
• Peripheral operations require the executing participant’s ledger to contain the resource, so the compiler rejects use by a participant without that authority.For example, it accepts Non-secure use of GPIO 7 C but rejects Secure use when the Secure ledger lacks GPIO 7 C.Source: §4 · p. 6
• A Non-secure callback requires finalized attribution, Non-secure ownership of the interrupt, and a callback computation whose effects fit the Non-secure ledger.Source: §4 · p. 6
• Registered callable Secure services must use only resources retained by the Secure participant, and typed handles let Non-secure code invoke them and receive results.A fully applied handle is invoked through sg, the interface’s operation for transferring explicit arguments and results between participants.Source: §4 · p. 6
• MicroHs generates a C source file from each build, which is linked with the domain’s runtime, startup code, glue, and drivers to produce its firmware image.Source: §4 · p. 7
• For public-interface programs, MicroHasTEE prevents duplicate acquisition, unauthorized resource use, post-finalization configuration, callbacks in the wrong participant, and calls to unregistered Secure functions.These guarantees rely on matching firmware images and the implementation, backend, and exclude raw C, FFI, internal interfaces, and malformed gateway input from the static model.Source: §4 · p. 7

5 Implementation

• The prototype targets a bare-metal STM32U5A5ZJQ; Secure startup configures the SAU and MPCBBs, while linker scripts and IDAU mapping belong to the trusted platform backend.The microcontroller has 4 MiB of flash and 2.5 MiB of SRAM.Source: §5 · p. 7

5.1 Program Partitioning and Compilation

• Each MicroHs build retains its target domain’s computations and replaces the other participant’s computations with placeholders, generating one C source file per firmware image.Both builds use the same public types, setup sequence, and division of resources and computations.Source: §5.1 · pp. 7–8, Figure 3 · p. 8

5.2 Secure Function Registration and Invocation

• Secure and Non-secure builds must execute registrations in the same order so their numeric callable identifiers match; MicroHasTEE assumes matching images are built and deployed together.The Secure build stores registered handlers in a dispatch table, while the Non-secure build creates the client-side handle.Source: §5.2 · p. 8
• Calls serialize a function identifier and arguments through the prototype’s only NSC entry point, which validates Non-secure buffers before dispatching to the Secure runtime.The receiver uses the identifier to select a handler from the dispatch table.Source: §5.2 · p. 9

5.3 Peripheral Drivers & Building the Firmware

• Both peripheral-driver builds expose identical APIs, but privileged attribution operations execute only in Secure firmware and become no-ops in the Non-secure build.Both builds type-check the same setup operations.Source: §5.3 · pp. 9–10, Figure 4 · p. 10
• The Secure image is built first to produce the linker library the Non-secure image needs for its NSC entry points.Each image links its generated C file with its domain’s runtime, startup code, gateway code, and drivers.Source: §5.1 · p. 8, §5.3 · p. 10, Figure 5 · p. 10

6.1 Case Study: A Secure Door Lock

• The door lock rejects requests after three consecutive incorrect PINs, with the PIN and failure counter stored in Secure flash so power cycling cannot reset attempts.The Secure service checks the persistent count before verifying a PIN and is exposed to Non-secure code through a registered Callable handle.Source: §6.1 · pp. 10–11
• The shared setup fixes both effect ledgers before registering the Secure service, allowing keypad access without transferring either Secure GPIO handle.Non-secure owns the seven keypad pins and UART; Secure retains the gate and lockout-indicator pins.Source: §6.1 · pp. 10–11

6.2 Trusted Computing Base

• The MicroHasTEE framework is 400 SLoC within 4,548 SLoC of produced code, while its just-over-13k-SLoC MicroHs base-library closure is a conservative estimate.The reported TCB scope omits the compiler, libc, linker, and assembler; unused definitions are pruned before code generation.Source: §6.2 · p. 12

6.3 Memory Requirements

• The runtime uses 76 KiB of flash per image; the serialized program uses 67.9 KiB Secure and 67 KiB Non-secure, while the Non-secure peripheral library uses 2.5 KiB less flash.Table 2 attributes the door-lock images’ flash footprint by component using linker maps.Source: §6.3 · p. 12, Table 2 · p. 12
• Each firmware image requires at least 220 KiB of runtime SRAM; exhausting the allocated heap makes the MicroHs runtime crash.Together, the Secure and Non-secure images require 440 KiB on the STM32U5A5ZJQ, which has 2.5 MiB of SRAM.Source: §6.3 · p. 12

TrustZone-M frameworks

• TF-M provides a trusted execution environment, whereas MicroHasTEE adopts TrustZone-M’s minimal model and checks peripheral attribution and separation at compile time.The comparison includes TF-M’s multiple isolated Secure partitions; MicroHasTEE currently supports a single Secure application.Source: §7 · pp. 12–13, Table 3 · p. 13
• TF-M’s PSA Client API uses runtime-sized iovecs, while MicroHasTEE’s typed service arguments let the compiler reject wrong call arity or argument types before firmware builds.TF-M manifests describe Secure partition resources without tying them to the Non-secure application’s assumptions, so mismatches can surface during execution.Source: §7 · p. 13

Other secure-language systems

• Rust’s experimental TrustZone-M support supplies a CMSE calling convention and gateway veneer, but leaves attribution and coordination of the two images to developers.HasTEE [9] inspired MicroHasTEE’s multiparty model but targets SGX and relies on a patched GHC runtime rather than bare-metal MicroHs.Source: §7 · p. 13
• GoTEE [6] partitions Go programs around SGX secure routines and channels, while J𝐸 uses information-flow control and a compiler pass to check interactions between partitions.The cited descriptions distinguish these systems’ partitioning and interaction checks from MicroHasTEE’s hardware-resource attribution focus.Source: §7 · p. 13

Embedded and multiparty languages

• LispBM targets resource-constrained MCU programming, while Synchron [10] provides a functional-language VM for embedded concurrency; MicroHasTEE instead tracks peripheral authority across paired TrustZone-M images.HasChor and Haste.App address multitier or endpoint partitioning, whereas MicroHasTEE centers hardware attribution and gateway authority.Source: §7 · pp. 13–14

8 Conclusions & Future Work

• For programs using its public interface, MicroHasTEE checks peripheral attribution, resource use, interrupt placement, and cross-domain interfaces for agreement before deployment.In the door-lock case study, the keypad and UART are Non-secure while the solenoid GPIO is Secure; inconsistent configurations are rejected by the type checker.Source: §8 · p. 14
• Roughly 230 KiB of flash per firmware image and 220 KiB of SRAM are required, indicating a somewhat well-provisioned device despite fitting the tested STM32U5.The tested device has 4 MiB of flash and 2.5 MiB of SRAM.Source: §8 · p. 14
• The evaluation covers one application on one STM32U5 and only a subset of implemented peripherals, without a formal soundness proof or execution-time, energy, or real-time measurements.The results support static-consistency, feasibility, and memory-requirement claims, but do not establish production readiness.Source: §8 · p. 14
• Further evaluation should compare gateway latency, worst-case execution time, and energy consumption against an equivalent C implementation.The framework demonstrates that a shared typed program can make cross-domain peripheral agreement a compile-time property on bare-metal TrustZone-M.Source: §8 · p. 14