March 13, 2026 · Alex Potanin

How to Get sel4test Running on NVIDIA Jetson Orin Nano 8GB

A complete step-by-step guide for porting the seL4 microkernel to the NVIDIA Jetson Orin Nano 8GB Developer Kit. Covers hardware setup, serial console wiring, cross-compiling sel4test, and booting from UEFI. All 141 compiled tests pass deterministically with stock NVIDIA firmware.

The port changes 3 seL4 repositories (github.com/potanin, orin-nano branch). Stock NVIDIA firmware works unmodified. sel4test and seL4_libs run unmodified from upstream.

1. Hardware

2. Serial Console

The serial console uses UARTC on the J14 button header — the small header near the three buttons on the carrier board (not the 40-pin GPIO header).

J14 Button Header (looking at the board, buttons nearest to you):

    Pin 1   Pin 2
    Pin 3   Pin 4    <- RXD (3), TXD (4)
    Pin 5   Pin 6
    Pin 7   Pin 8    <- GND (7)
    Pin 9   Pin 10
    Pin 11  Pin 12

    DO NOT connect VCC/3.3V from the adapter to the Jetson.

Serial parameters: 115200 baud, 8N1. Connect with:

picocom -b 115200 /dev/ttyUSB0

(Your device may be /dev/ttyUSB0, /dev/ttyUSB1, or /dev/ttyACM0. Use dmesg | tail after plugging in the adapter.)

3. Jetson Linux

Before building seL4 you need JetPack 6.x on the Jetson. Follow NVIDIA's Getting Started guide to flash your Dev Kit. Stock firmware works unmodified.

Once Linux is running, extract the hardware device tree and other reference information used to create the seL4 platform port:

# Copy the device tree blob from the running Jetson
sudo cat /sys/firmware/fdt > tegra234-orin-nano.dtb

# Decompile to human-readable DTS (on host or Jetson)
dtc -I dtb -O dts -o tegra234-orin-nano.dts tegra234-orin-nano.dtb

# Save the kernel config (useful reference for clocks, drivers, etc.)
zcat /proc/config.gz > kernel-config

# Dump the memory map
cat /proc/iomem > iomem.txt

The DTS in the seL4 kernel repo (tools/dts/orin-nano.dts, 11,514 lines) is the verbatim output of this extraction. The seL4 overlay (overlay-orin-nano.dts) selects the relevant nodes — UART, GIC, timer, and memory regions — from this full device tree.

Key information extracted from Linux:

• Memory regions — /proc/iomem shows DRAM at 0x80000000–0xbe000000 and 0xc2000000–0x100000000, with the 64 MB firmware carve-out gap between them
• UARTC address — 0x0c280000, clock ID 157, in the always-on (AON) power domain
• GIC addresses — GICD at 0x0f400000, GICR at 0x0f440000
• Timer PPIs — Secure=13, Non-secure=14, Virtual=11, Hyp=10

4. Building seL4

Install build dependencies per the seL4 host dependencies guide, including the AArch64 cross-compiler (gcc-aarch64-linux-gnu).

Clone Repositories

3 forked repos (github.com/potanin, orin-nano branch) plus upstream dependencies:

mkdir -p ~/jetson/potanin-git && cd ~/jetson/potanin-git

# Forked repos (github.com/potanin, branch: orin-nano)
git clone -b orin-nano https://github.com/potanin/seL4.git kernel
mkdir -p tools
git clone -b orin-nano https://github.com/potanin/seL4_tools.git tools/seL4
mkdir -p projects
git clone -b orin-nano https://github.com/potanin/util_libs.git projects/util_libs

# Upstream repos (pinned commits)
git clone https://github.com/seL4/seL4_libs.git projects/seL4_libs
git clone https://github.com/seL4/sel4test.git projects/sel4test
git clone https://github.com/seL4/musllibc.git projects/musllibc
git clone https://github.com/seL4/sel4_projects_libs.git projects/sel4_projects_libs
git clone https://github.com/seL4/sel4runtime.git projects/sel4runtime
git clone https://github.com/nanopb/nanopb.git tools/nanopb
git clone https://github.com/riscv/opensbi.git tools/opensbi

# Required build symlinks
ln -sf projects/sel4test/easy-settings.cmake easy-settings.cmake
ln -sf tools/seL4/cmake-tool/init-build.sh init-build.sh
ln -sf tools/seL4/cmake-tool/griddle griddle

Build

cd ~/jetson/potanin-git
mkdir build-orin && cd build-orin

../init-build.sh \
    -DPLATFORM=orin-nano \
    -DAARCH64=TRUE \
    -DARM_HYP=ON \
    -DSIMULATION=FALSE \
    -DRELEASE=FALSE

ninja

Output: build-orin/images/sel4test-driver-image-arm-orin-nano — a PE/COFF EFI executable (~6 MB).

5. Booting

Option A: HTTP Boot (Recommended)

HTTP boot lets you rebuild on the host and immediately reboot the Jetson without touching the SD card.

# Serve the EFI binary from the host machine
mkdir -p /srv/tftp
cp build-orin/images/sel4test-driver-image-arm-orin-nano /srv/tftp/sel4.efi
cd /srv/tftp && python3 -m http.server 8080

One-time UEFI setup: Connect DisplayPort + keyboard. Press ESC during boot to enter UEFI Setup. Add an HTTP boot entry pointing to http://<host-ip>:8080/sel4.efi. Set it as the first boot option.

Option B: SD Card Boot

# Format SD card as FAT32, then:
sudo mount /dev/sdX1 /mnt/sd
sudo mkdir -p /mnt/sd/EFI/BOOT
sudo cp build-orin/images/sel4test-driver-image-arm-orin-nano \
        /mnt/sd/EFI/BOOT/BOOTAA64.EFI
sudo umount /mnt/sd

Expected Output

The elfloader runs silently — UEFI's page tables do not map the UART MMIO region, so there is no serial output until the kernel initializes its own UART driver:

Booting all finished, dropped to user space
Starting test suite sel4test
Starting test 0: Test that there are tests
Starting test 1: SYSCALL0000
...
Test suite passed. 141 tests passed. 42 tests disabled.
All is well in the universe

6. Technical Details

UEFI boots to EL2 (not EL1), so seL4 must build with ARM_HYP=ON. The T234 has 6 Cortex-A78AE cores (ARMv8.2-A); seL4 runs single-core (non-SMP).

Memory Map

The gap at 0xbe000000 is firmware carve-out CO:43 (allocated by MB1, hardware-protected by the SNOC bus fabric). Any CPU access triggers an uncorrectable RAS error. Physical addresses 0x0–0x200000 are also reserved to prevent device untypeds covering firmware-protected addresses.

Fixes That Should Go Upstream

Several of our changes fix issues that affect other platforms, not just the T234. First the two issues that seem real and need to be fixed upstream:

• SDRAM-only kernel window (vspace.c) — upstream map_kernel_window() maps the entire PADDR_BASE–PADDR_TOP range as Normal memory. On any platform where non-DRAM addresses are protected, speculative accesses trigger faults. Our port maps only avail_p_regs[]. Upstream PR #1516 addresses kernel virtual layout but does not yet restrict the physical window to SDRAM.
• S2_START_L1 cmake bug (config.cmake) — the AARCH64_VSPACE_S2_START_L1 condition checks the wrong variable name. Affects any AArch64 platform using stage-2 page tables starting at L1.

Now the issues suggested by Claude Opus 4.6 that may not be necessary as it may not grasp the architectural details and the actual root causes of the problems:

• FEAT_CCIDX CCSIDR parsing (assembler.h) — the elfloader's cache set/way code assumes 32-bit CCSIDR format. ARMv8.2+ CPUs with FEAT_CCIDX (like the A78AE) use a 64-bit format with different field widths. Affects any ARMv8.2+ platform.
• PoU → PoC cache maintenance for page tables (machine.h, objecttype.c, vspace.c) — page table creation uses cleanCacheRange_PoU (dc cvau) and runtime PTE updates use cleanByVA_PoU. These only clean to Point of Unification, which may not reach a system-level cache sitting outside the CPU complex. The hardware page table walker reads from DRAM, so it can miss dirty PTEs stuck in the SLC. Fix: use cleanCacheRange_RAM (dc cvac, to PoC) for page table creation and cleanInvalByVA (dc civac) for PTE updates. Affects any platform with a system-level cache beyond PoU (e.g. ARM DSU-AE + external LLC).
• Non-shareable page tables in UP builds (vspace.c) — upstream uses SMP_TERNARY(SMP_SHARE, 0) for kernel page table shareability, which evaluates to non-shareable in uniprocessor builds. On hardware with a system-level cache, the page table walker participates in the inner shareable domain and may not see PTEs flushed to a non-shareable address. Fix: force inner shareable for kernel page tables regardless of SMP configuration. Affects any UP build on hardware where the page table walker is in the IS domain.
• Elfloader set/way flush does not reach system-level caches (sys_boot.c, mmu-hyp.S) — the elfloader uses dc cisw (clean+invalidate by set/way) to flush caches before enabling the MMU. Set/way operations only reach CPU-managed caches, not an external system-level cache. Page table entries get stuck in the SLC and the hardware walker reads stale data from DRAM. Fix: flush page tables with dc cvac (to PoC) while caches are still ON, then skip the set/way flush in disable_caches_hyp. Affects any platform with a system-level cache beyond L3.

7. Repository Structure

kernel/ — potanin/seL4 (12 files)

tools/seL4/ — potanin/seL4_tools (8 files)

projects/util_libs/ — potanin/util_libs (5 files)

8. Dead Ends

The port took roughly 120 iterations over 15 phases. Many of those iterations explored approaches that turned out to be wrong. Documenting them here so others can avoid the same traps.

Wrong UART: UARTA and the BPMP keepalive saga

The biggest time sink. We initially used UARTA at 0x03100000 (40-pin GPIO header), which required a custom pinmux overlay flashed into MB1. It worked at first, but the UARTA clock died after 5–10 minutes — BPMP power management aggressively gates clocks when no Linux driver holds a reference.

This led to building an entire BPMP IPC keepalive subsystem inside the seL4 kernel: IVC (Inter-VM Communication) protocol, HSP doorbell interrupts, MRQ_CLK messages, timer-tick integration. Over 40 versions (v70–v112) were spent tuning this. Results were non-deterministic (25 to 122 tests per boot depending on BPMP firmware state). Calling BPMP IPC from the timer interrupt blocked the kernel for ~10 ms and violated real-time scheduling guarantees. A fire-and-forget variant corrupted the IVC TX/RX counters.

The fix was trivial: switch to UARTC at 0x0c280000 on the J14 button header. UARTC is in the Always-On (AON) power domain and stays alive without any keepalive. All BPMP kernel code was deleted.

TCU (Tegra Combined UART) via USB

Before physical UART worked, we tried using the TCU — the Orin Nano’s default console, which operates as a USB gadget through the XUSB controller. After ExitBootServices the USB stack is gone, so no USB device appears on the host. Dead end.

Cross-boot diagnostics via SRAM and IVC shared memory

With no serial output after ExitBootServices, we tried writing diagnostic values to persistent memory (SRAM at 0x40010000, IVC shared memory regions) and reading them back on the next boot. SRAM wasn’t mapped in UEFI (crashed on access). IVC regions were cleared each boot. EFI SetVariable didn’t work after our MMU changes. Each attempt required two power cycles and none persisted reliably.

Garbled serial blamed on pinmux

When garbled bytes appeared on UARTA, investigation focused on pinmux configuration. A GPIO bit-bang test toggled pins directly — no output, because PADCTL is firewalled on T234 (CPU cannot read/write pinmux registers). The actual cause was a baud rate mismatch: UEFI released the UART clock reference at ExitBootServices, changing the effective clock rate. Fix: read UEFI’s divisor registers before ExitBootServices and re-send CLK_ENABLE afterward.

CBB ERD and IOB/ACI ERRCTLR — masking vs fixing RAS

We tried masking RAS errors at the bus fabric level. Setting the CBB (Control Backbone) Error Response Disable register at 0x13a3a004 converted bus errors into benign responses. But the IOB (I/O Bridge) generates its own RAS error independently of CBB. The error path is: SLC eviction → writeback → SCF → IOB → RAS. CBB is downstream of where the IOB error fires.

Writing directly to IOB/ACI ERRCTLR registers failed too — they are Secure-only. Writes from NS-EL2 are silently ignored.

SDEI handlers to catch RAS

Registered SDEI (Software Delegated Exception Interface) handlers for all 13 RAS events. The handlers were called successfully. But ATF unconditionally powers off the faulting core after dispatching the SDEI event, regardless of the handler’s return value. The core was killed anyway.

Custom BL31 — unnecessary in the end

Built custom NVIDIA ATF from source, modifying tegra234_ras_handler() to log errors instead of killing the core. Required a complex QSPI flashing journey (USB Recovery Mode, A/B boot slots, TOS image packing). Achieved deterministic 141/141 pass — but treated the symptom (core kill) rather than the cause (speculative accesses to protected memory).

Three software-only fixes later eliminated the RAS errors entirely: MT_NORMAL identity mapping in the elfloader, SDRAM-only kernel window, and 2 MiB low-address reservation. Stock BL31 restored.

XN-only (execute-never) mapping

Mapped the full PA range with UXN=1 instead of leaving non-DRAM unmapped. XN prevents speculative instruction fetches but not speculative data reads. The A78AE still speculatively reads data from Normal-mapped addresses. RAS errors persisted. Only leaving non-DRAM regions completely unmapped works.

PE/COFF sensitivity misdiagnosis

Removing UEFI ConOut code from efi_init.c caused a Synchronous Exception. We initially blamed NVIDIA’s PE/COFF loader being sensitive to binary layout changes. The actual cause: the default weak plat_console_putchar calls uart_8250_putchar(), which writes to UART MMIO at 0x0c280000. UEFI doesn’t map that address → data abort. Fix: override with a no-op (7 lines).

Implementation-defined CPU registers

Attempted to modify speculative behavior via ACTLR_EL2 and other implementation-defined registers. On the A78AE (r0p1), ATF traps and silently discards all EL2 writes to these registers. No CPU-level workarounds are possible from EL2.

MCE ROC_FLUSH_CACHE SMC calls

Tried T186-era MCE commands (ROC_FLUSH_CACHE, ROC_CLEAN_CACHE) via SMC to flush the SLC. Not supported on T234 — both return SMC_UNK. The SLC cannot be flushed from NS-EL2 on T234.

dc ivac to discard dirty SLC lines

Tried dc ivac (invalidate without clean) to discard dirty cache lines at protected addresses without triggering a writeback. The A78AE implementation cleans dirty lines before invalidating — dc ivac triggers the same writeback as dc civac. IOB RAS fires, core killed.

QSPI flash from the running system

During the custom BL31 phase, we tried every approach to write QSPI from a running OS: Linux MTD, /dev/mem, UEFI Shell mm, UEFI FirmwareManagement Protocol, NorFlashDxe, OP-TEE TA. All failed because the T234 CBB firewall blocks all Non-Secure CPU access to the QSPI controller at 0x03270000. Only USB Recovery Mode works (BROM exposes USB, MB1/MB2 have Secure access to QSPI).

BPMP IPC for UARTC clock enable

After switching to UARTC, we added BPMP IPC code to the elfloader to explicitly enable the UARTC clock (CLK_ENABLE + SET_RATE + RESET_DEASSERT) before ExitBootServices. ~60 lines of shared-memory IPC and doorbell code. Turned out to be completely redundant — firmware (MB1/MB2/BPMP/SPE) already enables UARTC from power-on (serial output appears at timestamp 0000.066, long before our EFI application loads). Removed.