Introduction

Umbra is a lightweight Rust-based kernel designed to wrap binaries into runtime Trusted Execution Environments (TEEs) for Arm TrustZone-M.

It is distributed as a static library, enabling integration with third-party software such as RTOSes or bare-metal applications to create TEEs dynamically or statically. By leveraging Rust, Umbra minimizes the Trusted Computing Base (TCB) and enhances code safety.

What Umbra Does

Umbra runs in the Secure World of a Cortex-M33 microcontroller with TrustZone-M. It provides a set of Non-Secure Callable (NSC) APIs that allow a Non-Secure host application to:

• Create enclaves from signed and encrypted binaries stored in flash
• Enter and exit enclaves with full context save/restore (preemptive via SysTick, cooperative via SVC)
• Query enclave status (running, suspended, terminated, faulted)
• Demand-page enclave code from flash to SRAM on first access (Enclave Swap Space)

Supported Hardware

Current Status

Umbra supports creating TEEs from a bare-metal host with:

• Chained measurement (boot-time integrity verification)
• Runtime ESS miss recovery (demand-paged enclave blocks with HMAC validation)
• Preemptive scheduling via Secure SysTick
• Cooperative yield via SVC
• Formal verification of the integrity model via ProVerif

Project Structure

umbra/
  src/
    kernel/               # Architecture-agnostic kernel (enclave management, key storage)
    hardware/
      architecture/arm/   # ARM Cortex-M33 primitives (SAU, MPU, vector table)
      platform/stm32l552/ # STM32L5 platform (boot, drivers)
  host/
    bare_metal_arm/       # Bare-metal NS host (round-robin enclave scheduler)
    freertos_arm/         # FreeRTOS NS host (RTOS coexistence demo)
  tools/                  # Enclave protection, key generation, smoke tests
  linker/                 # Kernel linker scripts
  book/                   # This documentation (mdBook)

Prerequisites

Rust Toolchain

Install Rust via rustup:

curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh

Switch to the nightly toolchain and add the Cortex-M33 target:

rustup toolchain install nightly
rustup override set nightly
rustup target add thumbv8m.main-none-eabi

ARM Cross-Compiler

Install the ARM bare-metal toolchain. The following tools are required:

On macOS (Homebrew):

brew install --cask gcc-arm-embedded

On Ubuntu/Debian:

sudo apt install gcc-arm-none-eabi

Debug and Flash Tools

Verify Installation

Run source settings.sh from the project root. The script checks all dependencies and reports any missing tools.

Build and Run

Configure Environment

Load environment variables and verify dependencies:

source settings.sh

The script auto-detects the target MCU (STM32L552 or STM32L562) and configures paths, flash addresses, and feature flags.

Select Host Application

Umbra ships with two NS host examples. Select one before building:

# Bare-metal round-robin (default)
source ./settings.sh

# FreeRTOS RTOS demo
export HOST_APP=freertos
source ./settings.sh

See the Host Examples section for details on each.

Build Everything

./rebuild_all.sh

This performs a full clean build:

1. Generates a fresh master key (tools/master_key.bin)
2. Builds the Secure Boot ELF (secureboot_build + secureboot_bin)
3. Builds the Umbra kernel static library (lib/libumbra.a)
4. Builds the selected host application (HOST_APP, default: bare_metal)
5. Protects enclave binaries (encryption, HMAC signing via tools/protect_enclave.py)

Flash and Run

./debug.sh

This flashes both the secure bootloader and the host application to the target via GDB + OpenOCD. On STM32L562, it also programs the plaintext enclave blob to external OCTOSPI flash.

Expected UART Output (STM32L552)

Connect to the ST-Link UART at 9600 baud:

[UMBRASecureBoot] Secure Boot started
[UMBRASecureBoot] Kernel Initialized
[UMBRASecureBoot] Jumping to Non-Secure World
[USER] Hello Non-Secure World!
[USER] Enclave created
[USER] Enclave terminated! R0=0x72CA33A8
[USER] All enclaves done

Note: additional diagnostic output (stack info, SAU/GTZC/MPU status, HASH/AES tests) is available by building with the boot_tests feature enabled.

Smoke Tests

Automated UART validation against golden baselines:

export UMBRA_UART=/dev/cu.usbmodem211203  # your serial device
tools/smoke_test.sh

The script resets the target, captures UART output, and diffs against tools/golden_uart.log.

Hardware Setup

Selecting the Target MCU

Before building, you must select the target microcontroller in settings.sh. Open the file and set the MCU_VARIANT variable:

• stm32l552 — for the NUCLEO-L552ZE-Q board (default)
• stm32l562 — for the STM32L562E-DK Discovery board

Then source the configuration:

source settings.sh

The script auto-detects which variant is selected and configures feature flags, flash addresses, and peripheral settings accordingly.

STM32L552 — NUCLEO-L552ZE-Q

1. Connect the Nucleo board via USB (ST-Link)
2. UART debug is on LPUART1 via ST-Link VCP (9600 baud)
3. No additional wiring required

Enable TrustZone

TrustZone must be enabled once via STM32 Programmer:

make enable_security

This sets the TZEN option byte. The device resets after programming.

STM32L562 — STM32L562E-DK

1. Connect the Discovery board via USB (ST-Link)
2. UART debug is on USART1 (PA9/PA10) via ST-Link VCP (9600 baud)
3. The on-board MX25LM51245G OCTOSPI flash is used for enclave storage

Enable TrustZone

Same as L552:

make enable_security

External Flash

The L562 Discovery has an on-board Octa-SPI flash. Umbra uses it for storing encrypted enclave binaries. The OTFDEC (On-The-Fly Decryption) engine transparently decrypts data on read.

No additional configuration is needed — debug.sh handles programming the external flash.

Host Examples

Umbra ships with two Non-Secure host applications that demonstrate enclave lifecycle management through the NSC API. Both are self-contained C projects under host/ with their own Makefile, linker scripts, and startup code.

Selecting an Example

The active host is controlled by the HOST_APP environment variable:

# Bare-metal (default)
source ./settings.sh
./rebuild_all.sh
./debug.sh

# FreeRTOS
export HOST_APP=freertos
source ./settings.sh
./rebuild_all.sh
./debug.sh

settings.sh maps HOST_APP to the corresponding directory and exports HOST_DIR, HOST_NAME, and HOST_ELF. These variables are consumed by rebuild_all.sh, debug.sh, and the root Makefile targets (program_elf_host, program_enclaves_extload).

Common Enclave Payload

Both examples use the same Fibonacci enclave (app/fibonacci.c). The enclave code is linked into the ._enclave_code section, then encrypted and HMAC-signed by tools/protect_enclave.py at build time. At runtime, the Secure kernel validates and loads the enclave into the Enclave Swap Space (ESS) in Secure SRAM.

UART Output

Connect to the ST-Link UART at 9600 baud. Both examples print status messages prefixed with [USER] (bare-metal) or [FREERTOS] (FreeRTOS).

Bare-Metal Example

The bare-metal host (host/bare_metal_arm/) is the simplest way to interact with Umbra. It runs a hand-coded round-robin loop that scans flash for enclaves, creates them via NSC veneers, and executes them until termination.

How It Works

main()
  ├── Scan NS flash (0x08040000–0x08080000) for UMBR magic at 4KB page boundaries
  ├── umbra_tee_create(addr) for each enclave found
  └── Round-robin loop:
        ├── umbra_enclave_enter(id) → returns status
        │     ├── SUSPENDED  → enclave was preempted by Secure SysTick
        │     ├── TERMINATED → print R0 result, mark done
        │     └── FAULTED    → print error, mark done
        └── Repeat until all enclaves done

No RTOS, no heap, no interrupts in the NS world. The Secure SysTick handles enclave preemption; the host just re-enters suspended enclaves.

Building and Running

# Bare-metal is the default — no HOST_APP needed
source ./settings.sh
./rebuild_all.sh
./debug.sh

Expected UART Output

[UMBRASecureBoot] Secure Boot started
[UMBRASecureBoot] Kernel Initialized
[UMBRASecureBoot] Jumping to Non-Secure World
[USER] Hello Non-Secure World!
[USER] Enclave created
[USER] Enclave preempted (SysTick)
[USER] Enclave preempted (SysTick)
...
[USER] Enclave terminated! R0=0x72CA33A8
[USER] All enclaves done

The number of Enclave preempted lines varies depending on the SysTick quantum (~10ms at 4 MHz MSI).

File Structure

host/bare_metal_arm/
  ├── src/
  │   ├── main.c          Entry point, enclave header, round-robin scheduler
  │   └── startup.s       NS vector table + Reset_Handler (.data/.bss init)
  ├── app/
  │   └── fibonacci.c     Enclave payload (Fibonacci + filler functions)
  ├── inc/
  │   └── fibonacci.h
  ├── linker/
  │   ├── memory.ld       MCU memory regions + Umbra aliases
  │   └── host.ld         Section layout + NSC veneer addresses (PROVIDE)
  └── Makefile

Key Design Points

• No vector table fetch: the NS VTOR is not used at runtime — the bare-metal host never triggers SVC, PendSV, or SysTick exceptions. All scheduling is done cooperatively via the round-robin loop.
• Enclave header in flash: the 48-byte header (magic, trust level, HMAC) is placed in ._enclave_header by a section attribute. protect_enclave.py overwrites the HMAC field at build time.
• NSC veneer addresses: hardcoded via PROVIDE() in host.ld. These must be updated if the Secure boot is rebuilt and veneer offsets change.

FreeRTOS Example

The FreeRTOS host (host/freertos_arm/) demonstrates that Umbra's TrustZone isolation works transparently with a standard RTOS. A single FreeRTOS task manages the entire enclave lifecycle, proving that the Secure SysTick (enclave preemption) and the NS SysTick (FreeRTOS tick) operate independently on the dual-SysTick Cortex-M33 architecture.

How It Works

main()
  ├── Set VTOR to SRAM vector table
  ├── Enable NS fault handlers (SHCSR)
  ├── xTaskCreate(vEnclaveTask, ...)
  └── vTaskStartScheduler()        // never returns

vEnclaveTask(pvParameters)
  ├── Scan NS flash for enclave headers (same logic as bare-metal)
  ├── umbra_tee_create(addr) for each enclave found
  ├── Loop: umbra_enclave_enter(id)
  │     ├── SUSPENDED  → print, re-enter
  │     ├── TERMINATED → print R0, mark done
  │     └── FAULTED    → print error, mark done
  └── vTaskDelete(NULL)            // self-delete when all done

FreeRTOS manages task scheduling in the NS world. The enclave task calls into the Secure kernel via NSC veneers — Umbra doesn't know or care that an RTOS is running.

Building and Running

export HOST_APP=freertos
source ./settings.sh
./rebuild_all.sh
./debug.sh

The first build will clone the FreeRTOS-Kernel submodule automatically if needed:

git submodule update --init host/freertos_arm/lib/FreeRTOS-Kernel

Expected UART Output

[UMBRASecureBoot] Secure Boot started
[UMBRASecureBoot] Kernel Initialized
[UMBRASecureBoot] Jumping to Non-Secure World
[FREERTOS] Starting FreeRTOS demo
[FREERTOS] Enclave task started
[FREERTOS] Enclave created
[FREERTOS] Enclave terminated! R0=0x72CA33A8
[FREERTOS] All enclaves done

File Structure

host/freertos_arm/
  ├── lib/
  │   └── FreeRTOS-Kernel/    Git submodule (V11.1.0, ARM_CM33_NTZ port)
  ├── src/
  │   ├── main.c              FreeRTOS init + enclave task
  │   ├── vectors.c           SRAM vector table (aligned 512B, non-const)
  │   ├── handlers.c          NS fault handlers (in C for Thumb bit correctness)
  │   ├── port_overrides.c    vStartFirstTask override (avoids flash data read)
  │   ├── startup.s           Reset_Handler only (.data/.bss init)
  │   ├── mem.c               Minimal memset/memcpy for -nostdlib
  │   └── FreeRTOSConfig.h    Kernel config (NTZ, 4MHz, 32KB heap)
  ├── app/
  │   └── fibonacci.c         Enclave payload (same as bare-metal)
  ├── inc/
  │   └── fibonacci.h
  ├── linker/
  │   ├── memory.ld           Self-contained memory regions + Umbra aliases
  │   └── host.ld             Section layout + NSC veneer PROVIDE addresses
  └── Makefile                Standalone build (FreeRTOS sources compiled from submodule)

FreeRTOS Configuration

TrustZone Porting Notes

Porting FreeRTOS to the NS world of an STM32L5 with an active Secure kernel required solving several non-obvious issues:

SRAM Vector Table

The STM32L5 IDAU classifies 0x08040000 (NS flash) as Secure for data reads. The SAU override only applies to instruction fetch. Since the Cortex-M33 vector table fetch is architecturally a data read, the NS vector table must reside in SRAM (0x20000000+), not flash.

The vector table is defined as a non-const C array with __attribute__((aligned(512))). It lands in .data and is copied to SRAM by the startup code. VTOR_NS is set to 0x20000000 by the Secure boot.

vStartFirstTask Override

The FreeRTOS ARM_CM33_NTZ port reads *(VTOR[0]) (a data read from the vector table base) to reset MSP. This faults on STM32L5 if VTOR points to flash. port_overrides.c provides a replacement that loads MSP from the linker symbol _host_estack instead.

The override uses --allow-multiple-definition in LDFLAGS, with our object listed before FreeRTOS objects in link order.

SVC Number

FreeRTOS V11 uses SVC #102 (not #0) for START_SCHEDULER, defined in portmacrocommon.h. The override must use the correct number or the SVC handler ignores the call.

Fault Handlers in C

Assembly-defined .thumb_func labels lose the Thumb interworking bit (LSB) in R_ARM_ABS32 data relocations used by the SRAM vector table initializer. Defining fault handlers in C guarantees correct Thumb bit propagation.

NS Fault Handler Enable

The Secure boot enables Secure SHCSR but not NS SHCSR. Without SCB_SHCSR |= (1<<16)|(1<<17)|(1<<18) in NS code, all configurable NS faults silently escalate to HardFault with no diagnostic CFSR bits.

Architecture Overview

TrustZone-M

Arm TrustZone-M splits the Cortex-M33 processor into two security states:

• Secure World — runs Umbra (bootloader, kernel, drivers). Has access to all memory.
• Non-Secure World — runs the host application. Cannot access Secure memory.

Transitions between worlds are controlled by hardware:

• NS to S: Via Non-Secure Callable (NSC) regions containing SG (Secure Gateway) instructions
• S to NS: Via BLXNS instruction or exception return with special EXC_RETURN values

Umbra's Role

Umbra provides the Secure World runtime. It:

1. Boots first — the vector table is in Secure flash; Umbra initializes SAU, GTZC, MPU, and peripherals before handing control to the Non-Secure host
2. Provides APIs — 5 NSC veneers allow the host to create, enter, exit, and query enclaves
3. Manages enclaves — loads encrypted code from flash, validates integrity (HMAC), decrypts (AES), and installs into Secure SRAM
4. Enforces isolation — MPU regions protect kernel memory from enclave code; MPCBB controls 256-byte block-level SRAM security

Memory Map

Flash Bank 0 (256 KB) — Secure
  0x08000000  +-- Secure Boot (68 KB) --- vector table, handlers, boot logic
  0x08011000  +-- Kernel Text (172 KB) -- NSC API implementations, kernel code
  0x0803C000  +-- NSC Region (16 KB) ---- SG veneers (umbra_tee_create, etc.)

Flash Bank 1 (256 KB) — Non-Secure
  0x08040000  +-- Host Application ------ user code, enclave headers + encrypted blocks

SRAM0 (128 KB) — Non-Secure
  0x20000000  +-- Host stack + data

SRAM1 (64 KB) — Secure (alias 0x30020000)
  0x20020000  +-- ESS (Enclave Swap Space) -- loaded enclave code blocks
  0x30030000  +-- Kernel .data / .bss (56 KB)
  0x3003E000  +-- NSC data (8 KB)

Crate Structure

Umbra is organized as four Rust crates with clear responsibilities:

kernel (no_std, no external deps)
  |
  +-- arm (depends on: cortex-m, kernel)
  |     Architecture-specific: SAU, MPU, vector table (.s)
  |
  +-- drivers (depends on: peripheral_regs, kernel)
  |     Platform-specific: RCC, GPIO, UART, DMA, HASH, AES, GTZC, OTFDEC, OCTOSPI
  |
  +-- boot (depends on: arm, drivers, kernel, peripheral_regs, cortex-m)
        Entry point: secure_boot(). Handlers, API implementations, validator

kernel

Architecture-agnostic core logic:

• Enclave descriptor management
• Key storage server (key generation, derivation)
• Memory protection traits (MemorySecurityGuardTrait)
• Enclave Swap Space (ESS) data structures
• NSC API symbol declarations

Optimized for size (opt-level = "z").

arm

ARM Cortex-M33 hardware abstraction:

• SAU driver — Secure Attribution Unit region configuration
• MPU driver — Memory Protection Unit with ARMv8-M RBAR/RLAR format
• startup.s — vector table, exception handlers, save_enclave_context, SVC dispatch

drivers

STM32L552/L562 peripheral drivers:

• RCC — clock gating for all peripherals
• GPIO — pin mode, alternate function, set/reset
• UART — LPUART1 (L552) / USART1 (L562) at 9600 baud
• DMA — 16-channel queue-based transfer manager
• HASH — SHA-256, HMAC with context save/restore
• AES — hardware (L562) or software emulated (L552)
• GTZC — MPCBB block-level SRAM security
• OTFDEC — on-the-fly decryption (L562 only)
• OCTOSPI — memory-mapped external flash (L562 only)

boot

The binary crate (entry point):

• main.rs — secure_boot() initialization sequence
• secure_kernel.rs — Kernel struct, ESS miss handling, block loading
• handlers.rs — exception handlers (HardFault, MemManage, UsageFault, SecureFault, BusFault)
• api_impl.rs — NSC API implementations (_imp functions)
• validator.rs — HMAC verification + AES decryption (formal model analog)
• raw_print.rs — low-level UART output for exception contexts

Boot Flow

Startup Sequence

1. Reset_Handler (assembly, startup.s)

   • Copies .data from flash to SRAM
   • Zeros .bss
   • Calls secure_boot() in Rust

2. secure_boot() (Rust, main.rs)

   Step	What	Why
   GPIO + LED	Configure board LED	Visual boot indicator
   UART	Init LPUART1/USART1 at 9600 baud	Debug output
   SAU	Configure Secure Attribution Unit regions	Define S/NS/NSC memory boundaries
   GTZC	Configure MPCBB for SRAM block security	256-byte granularity SRAM protection
   MPU	Enable Memory Protection Unit	Isolate kernel from enclaves
   Fault enables	MEMFAULT, BUSFAULT, USGFAULT, SECUREFAULT	Fault isolation for ESS recovery
   DMA	Enable DMA1/DMA2 + NVIC interrupts	Block loading from flash to SRAM
   Crypto	Init HASH (SHA-256) + AES (HW or SW)	Integrity verification + decryption
   Kernel	Create Kernel instance, derive session keys	Central state for enclave management
   OCTOSPI (L562)	Memory-mapped external flash + OTFDEC	Transparent enclave decryption
   SysTick	Disable (enabled per-enclave by SVC handler)	Preemptive scheduling
   VTOR_NS	Set NS vector table to 0x08040000	Host exception handling
   trampoline_to_ns()	Set MSP_NS, BLXNS to host entry	Transfer to Non-Secure World

After Boot

The host application runs in Non-Secure World. It discovers enclaves in flash, creates them via umbra_tee_create(), and schedules them via umbra_enclave_enter(). Each enter triggers an SVC into Secure World where the kernel restores enclave context and enables SysTick for preemption.

Enclave Swap Space (ESS)

Concept

Enclaves are stored encrypted in flash. They cannot execute directly from flash — they must be loaded into Secure SRAM, validated (HMAC), and decrypted (AES) before execution.

The Enclave Swap Space (ESS) manages this process as a demand-paged cache:

• Enclave code is split into 256-byte Enclave Flash Blocks (EFBs)
• Only a subset of blocks are loaded into SRAM at any time
• When the CPU fetches an instruction from an unloaded block, a UsageFault (UNDEFINSTR) fires
• The fault handler loads the missing block on-demand (ESS miss recovery)

ESS Miss Recovery Flow

1. Enclave executes code in block N
2. CPU fetches instruction from block M (not yet loaded) — hits a UDF trap (undefined instruction)
3. UsageFault fires, assembly trampoline saves context, calls umbra_usage_fault_dispatch()
4. Dispatcher identifies the faulting PC, looks up which enclave and block it belongs to
5. handle_ess_miss() is called:
   • Fetch: DMA transfer from flash to scratch buffer (L552) or CPU copy from OCTOSPI (L562)
   • Validate: HMAC-SHA256 verification against on-flash signature
   • Decrypt: AES-CTR decryption (L552 software, L562 via OTFDEC)
   • Evict: If cache is full, evict LFU (Least Frequently Used) block
   • Install: DMA copy to ESS slot, MPCBB flip to Secure, cache invalidate
6. Fault handler returns — CPU re-executes the faulting instruction, now hitting valid code

Block Layout on Flash

Each block on flash has this structure (with chained_measurement + ess_miss_recovery features):

[HMAC (32B)] [Metadata (32B)] [Ciphertext (256B)]
 +-- 64B header --+               +-- EFB payload --+

Total: 320 bytes per block.

Prefetch Pipeline

To reduce ESS miss latency, Umbra speculatively prefetches reachable blocks. Each block's metadata includes a reachability list — blocks that are control-flow successors. After installing a block, the prefetch pipeline asynchronously loads reachable blocks via DMA.

STM32L552 — NUCLEO-L552ZE-Q

Board Overview

The NUCLEO-L552ZE-Q is the primary development board for Umbra. It features a Cortex-M33 with TrustZone-M but without hardware AES or external flash.

Key Characteristics

UART Connection

The ST-Link provides a Virtual COM Port. No additional wiring needed.

• Serial device (macOS): /dev/cu.usbmodem*
• Serial device (Linux): /dev/ttyACM0
• Baud rate: 9600

STM32L562 — STM32L562E-DK

Board Overview

The STM32L562E-DK Discovery board extends L552 capabilities with hardware AES and an on-board Octa-SPI flash. This enables transparent on-the-fly decryption of enclaves via OTFDEC.

Key Characteristics

OTFDEC Operation

On the L562, enclave blocks are stored encrypted in external flash. The boot sequence:

1. Loads plaintext enclave blob to OCTOSPI via external loader
2. Uses OTFDEC in ENC mode to encrypt and write back to flash
3. Switches OTFDEC to DEC mode for runtime
4. Memory-mapped reads from 0x90000000 return decrypted data transparently

This means the CPU never sees ciphertext during normal operation — OTFDEC is a bus-level transform.

OCTOSPI Pin Assignment

NSC API Reference

Umbra exposes 5 Non-Secure Callable (NSC) functions. These are the only way the host application can interact with the Secure World.

Each function is implemented as an assembly veneer containing a SG (Secure Gateway) instruction, followed by a branch to the Rust implementation. The veneers are placed in the .umbra_nsc_api section at fixed addresses starting at 0x0803C000.

umbra_tee_create

uint32_t umbra_tee_create(uint32_t base_addr);

Creates a TEE from an enclave binary at base_addr in Non-Secure flash.

• Reads and validates the enclave header (magic 0x524D4255 = "UBMR")
• Performs chained measurement (HMAC chain over all blocks)
• Registers the enclave in the Enclave Swap Space
• Returns: enclave ID (bits 31:16) | status (bits 15:0). Status 0 = success.

umbra_enclave_enter

uint32_t umbra_enclave_enter(uint32_t enclave_id);

Enters (or resumes) an enclave. This triggers an SVC into Secure World where the kernel:

1. Restores the enclave's saved context (r4-r11, PSP, CONTROL)
2. Enables Secure SysTick for preemption (~10ms quantum)
3. Returns to the enclave via crafted EXC_RETURN

The function blocks until the enclave is preempted (SysTick), yields (SVC #1), terminates, or faults.

• Returns: (enclave_id << 16) | (status << 8) where status is one of:
  • 3 = Suspended (preempted by SysTick or voluntary yield)
  • 4 = Terminated (enclave returned normally)
  • 5 = Faulted (unrecoverable fault)

umbra_enclave_exit

uint32_t umbra_enclave_exit(uint32_t enclave_id);

Terminates a suspended enclave from the host side. Only valid when the enclave is in Suspended state.

• Returns: (enclave_id << 16) | (status << 8)

umbra_enclave_status

uint32_t umbra_enclave_status(uint32_t enclave_id);

Queries the current state of an enclave.

• Returns: If terminated, returns the enclave's final R0 value. Otherwise returns the status code.

umbra_debug_print

void umbra_debug_print(const char* str_ptr);

Prints a null-terminated string from Non-Secure memory to the Secure UART. Useful for host-side debug logging via the Secure World UART driver.

Formal Verification

Overview

Umbra's integrity model is formally verified using ProVerif, an automatic cryptographic protocol verifier.

Two models are maintained in docs/formal/:

What Is Verified

Both models prove two key properties:

1. Execution implies request: Every executed block was explicitly requested by the kernel

   inj-event(Execute(b, d)) ==> inj-event(Request(b))
   

2. Execution implies registration: Every executed block was registered in the ESS

   event(Execute(b, d)) ==> event(RegisterBlock(b, d))
   

These properties guarantee that an attacker cannot cause the CPU to execute unvalidated code, even if they can tamper with flash contents or DMA transfers.

Running Verification

Install ProVerif, then:

cd docs/formal
proverif UmbraIntegrityFixValidator.pv
proverif UmbraIntegrityRaceValidatorFix.pv

Both should report RESULT lines ending with is true.

When to Re-verify

Re-run ProVerif after modifying:

• Kernel::handle_ess_miss (block loading and validation flow)
• validate_block (HMAC computation or comparison)
• Fault dispatchers in handlers.rs (UsageFault, SecureFault, BusFault)
• On-flash block layout in protect_enclave.py
• ESS cache insertion or eviction logic

Contributing

Build from Source

git clone https://github.com/HiSA-Team/umbra.git
cd umbra
source settings.sh
./rebuild_all.sh

See Prerequisites for required tools.

Code Conventions

• Rust edition: 2021, nightly toolchain
• Target: thumbv8m.main-none-eabi (Cortex-M33)
• No std: all crates are #![no_std]
• Naming: snake_case for functions/variables, UPPER_CASE for statics, PascalCase for types
• Assembly: separate .s files in asm/ directories (not global_asm!)

Testing

Compilation Gate

Both variants must compile without warnings:

# L552 (default)
source settings.sh   # select L552
./rebuild_all.sh

# L562
source settings.sh   # select L562
./rebuild_all.sh

On-Target Smoke Tests

export UMBRA_UART=/dev/cu.usbmodem211203
tools/smoke_test.sh                    # Normal boot + enclave execution
tools/smoke_test_fault.sh              # Fault injection
tools/smoke_test_fault_runtime.sh      # Runtime fault recovery

Formal Verification

cd docs/formal
proverif UmbraIntegrityFixValidator.pv
proverif UmbraIntegrityRaceValidatorFix.pv

Pull Request Process

1. Create a branch from main
2. Ensure both L552 and L562 build with 0 warnings
3. Run smoke tests on at least one hardware variant
4. Open a PR with a description of what changed and why