April 26, 2026 · updated April 27, 2026 · Alex Potanin

seL4, Microkit, and Alpine Linux on the Jetson AGX Orin Devkit

Picking up from the Orin Nano port: the same Tegra T234 SoC sits in the AGX Orin Developer Kit too. With small additions we run sel4test (141/141 pass), Microkit (tutorial parts 1–4 including a tiny bare-metal libvmm guest), and a full Alpine Linux 3.19 distro under libvmm with on-board 10 GbE working and keyless SSH from the host PC. Mainline tegra-host1x + tegra-vic bind to passed-through hardware so /dev/dri/card0 exists.

All AGX-specific changes live on the orin-agx branches of the github.com/potanin forks (kernel, seL4_tools, util_libs, microkit, libvmm). The Nano port established the hard-won fixes — SDRAM-only kernel window, MT_NORMAL identity mapping, FEAT_CCIDX cache parsing, etc.; AGX inherits those wholesale.

1. Hardware

Compared to the Nano, the AGX Orin Devkit is friendlier for embedded development: the on-board USB-C debug port exposes the Tegra Combined UART (TCU) through the SPE coprocessor. No external USB-UART adapter, no level-shifting, no soldering — one cable handles both flashing and serial.

Bidirectional console: host keystrokes reach the guest via the SPE → HSP (Hardware Synchronization Primitives) mailbox → tegra-tcu driver in the guest, exposed as /dev/ttyTCU0. The reverse path takes guest output back out the TCU via the AON HSP. We use a tiny host-side tcu-term.py that pads each Enter to 8 bytes so the SPE's USB-CDC RX batch flushes immediately.

2. Boot setup — PXE proxyDHCP

The Nano blog used UEFI HTTP boot. The AGX UEFI also supports HTTP boot, but we found PXE over IPv4 faster to iterate against because the AGX picks up new payloads simply by power-cycling — no UEFI menu, no SD card.

The pattern: leave the home router's regular DHCP alone, run a proxyDHCP on the dev host that injects PXE options (next-server, boot-file). TFTP is served by stock tftpd-hpa out of /srv/tftp.

$ sudo apt install dnsmasq tftpd-hpa
$ sudo systemctl start tftpd-hpa
$ ./dhcp-sel4test.sh &       # serves agx/sel4test.efi
$ # or ./dhcp-microkit.sh &   # serves agx/microkit.efi
$ # or ./dhcp-libvmm-alpine.sh & # serves agx/libvmm-alpine.efi

Each wrapper just sets BOOTFILE and exec's a shared dhcp.sh that runs dnsmasq --dhcp-range=...,proxy --pxe-service=ARM64_EFI,.... Drop the matching .efi into /srv/tftp/agx/ and power-cycle.

One-time UEFI tweak: connect a DisplayPort monitor + USB keyboard, reboot, hit Esc on the splash, set UEFI Boot Order so the on-board NIC's UEFI PXEv4 entry is first. After that the AGX boots the EFI we serve every time.

3. sel4test

The seL4 kernel for AGX is a near-clone of the Nano's orin-nano platform. Same SoC, same UARTC at 0x0c280000, same GICv3, same A78AE errata behaviour. The new orin-agx platform entry exists because:

• The AGX has more RAM (32 GB vs 8 GB) — different memory map.
• Per-platform settings stay decoupled so future divergence (e.g. AGX's 12 cores vs the Nano's 6) doesn't have to be guarded with conditionals.

The kernel and elfloader fixes (T234 SLC cache discipline, init_downpages full-PA identity map, SDRAM-only kernel window, 2 MiB low-address reservation, UART driver init, plat_console_putchar override) carry over from the orin-nano post unchanged — that post documents them with rationale and per-file diffs. The AGX-only delta on top is the new src/plat/orin-agx/ directory + DTS, the libsel4 and util_libs platform headers, and (for libvmm guests later in this post) the HCR_TID3 trap in vcpu.h. Build flags are identical: -DARM_HYP=ON -DDEBUG=ON (the latter unlocks 9 BREAKPOINT / SINGLESTEP tests — 132/141 without it, 141/141 with).

Build

cd ~/jetson-agx-orin/sel4test-src
mkdir build-orin-agx && cd build-orin-agx

../init-build.sh \
    -DPLATFORM=orin-agx \
    -DAARCH64=TRUE \
    -DARM_HYP=ON \
    -DDEBUG=ON

ninja
cp images/sel4test-driver-image-arm-orin-agx /srv/tftp/agx/sel4test.efi

Boot

$ ./dhcp-sel4test.sh &
$ ./run-sel4test.sh             # power-cycle + open picocom on /dev/ttyACM0
...
Test suite passed. 141 tests passed. 42 tests disabled.
All is well in the universe

4. Microkit (parts 1–4)

The au-ts/microkit_tutorial walks four parts: a hello PD on UARTC; two PDs sharing memory rings; a third PD with a separate input UART; finally replacing the bare-metal client with a libvmm guest VM. Adding the AGX as a Microkit board is three small changes:

1. build_sdk.py — new BoardInfo(name="orin_agx", gcc_cpu="cortex-a78ae", loader_link_address=0x88000000, kernel_options={"KernelPlatform": "orin-agx", ...}). The link address is bumped from the default 0x80500000 to 0x88000000 (128 MiB into DDR) so the Microkit "initial task" has room for a libvmm payload that embeds a Linux kernel + initrd (~36 MiB).
2. loader/src/uart.c — UARTC at 0x0c280000 for early loader prints. UEFI has already enabled the clock and divisor, so uart_init is a no-op.
3. loader/src/aarch64/util64.S — in disable_mmu, preserve SCTLR_EL2's C bit (data cache enable). Clearing it on T234 triggers writeback of dirty firmware cache lines into protected memory, which the SLC hands to the IOB and which then RAS-faults the core. Same root cause as the cache-maintenance fixes on the Nano, just surfacing in a different code path.

Part 4 — the tiny libvmm guest

Part 4 was the only one that needed a kernel change beyond the Nano's work: enable HCR_TID3 in HCR_VCPU and emulate guest reads of ID-group-3 system registers in the kernel's hypervisor stub. Without this, the guest kernel's CPU-feature probe trips on ID_AA64MMFR0_EL1.PARange (the A78AE reports 44-bit; our stage-2 page tables are configured for 40-bit, the same override we use on Nano). The trap lets the kernel return a sanitised value with PARange = 40.

// include/arch/arm/armv/armv8-a/64/armv/vcpu.h
#define HCR_VCPU   ( HCR_COMMON | HCR_TWE | HCR_TWI | HCR_TID3 )

Plus a small handler that decodes the ESR_EL2.ISS, reads the real hardware ID register, masks the offending field, and writes the sanitised value back into the guest register file. ~80 lines.

5. libvmm + Alpine Linux + SSH

The next step is swap the toy bare-metal guest from Microkit part 4 for a real Linux distro. We use au-ts/libvmm's simple example as a starting point and fork it for the AGX. End state: an Alpine 3.19 guest with on-board 10 GbE, keyless SSH from the host PC, and a working DRM card via mainline tegra-host1x + tegra-vic.

What we pass through to the guest

DMA worked out of the box without any explicit IOMMU programming: stage-2 identity-maps guest_ram (IPA = PA), and the Tegra SMMU defaults to bypass for our stream IDs. That's the unsafe part — this Section 5 path lets the guest's MGBE driver program DMA with arbitrary physical addresses. Section 6 (Path B) fixes this by moving MGBE ownership into a trusted PD; the guest only sees virtio-net with no DMA capability.

The vGIC fix

libvmm's vgic_v3 emulator was built and tested against odroid-c4 / qemu; on T234 the guest's first GICR_ISENABLER write fell into a branch that printed "Unknown enable register encoding" and no IRQs were ever delivered. Three small additions to src/arch/aarch64/vgic/vgic_v3.c + headers fix it; the changes are board-agnostic and should go upstream.

Initrd: Alpine + bake-in openssh + pinned MAC

build-initrd.sh takes Alpine's aarch64 minirootfs tarball and packs it through Linux's gen_init_cpio. At build time we also chroot into the rootfs (under sudo chroot; binfmt_misc's qemu-aarch64 with the F flag handles the ABI swap transparently) to:

• apk add openssh-server — bake sshd in
• ssh-keygen -A — bake host keys
• chpasswd root:libvmm — bake the demo password
• copy ~/.ssh/id_rsa.pub to /root/.ssh/authorized_keys

We also pin the guest MAC in the device tree (local-mac-address = [02 c2 0a 00 01 01]) so DHCP returns the same lease across reboots. mini-init.sh on first boot mounts devpts, brings eth0 up, runs udhcpc, starts sshd, and prints the IP on TCU.

Boot & SSH in

$ ./run-libvmm-alpine.sh
[l4t] building libvmm + wrapping into EFI...
[l4t] deploying to /srv/tftp/agx/libvmm-alpine.efi...
[l4t] starting dhcp-libvmm-alpine.sh in background...
[l4t] power-cycling jetson...
[l4t] opening /dev/ttyACM0 with tcu-term.py...
...
>>> Alpine shell on /dev/ttyTCU0 — welcome <<<
~ # uname -a
Linux (none) 6.6.1 #9 SMP PREEMPT aarch64 Linux
~ # cat /etc/alpine-release
3.19.1
>>> sshd up: ssh root@192.168.100.180 (key or pw: libvmm)

# from the host:
$ ssh root@192.168.100.180   # keyless, your pubkey is baked in
~ # ls /dev/dri/
card0  renderD128
~ # drm_info /dev/dri/card0 | head
Driver: tegra (NVIDIA Tegra graphics) version 1.0.0
Device: host1x nvidia,tegra234-host1x

6. Path B — sDDF-mediated network (NEW Apr 27)

Section 5 above gets Alpine on the wire by directly passing through MGBE0 to the guest: the guest's mainline tegra-mgbe driver writes the MAC controller registers, the AQR113C PHY autonegotiates, the guest's own DMA engine moves packets. That works — you've seen the SSH demo — but it has a fundamental security problem:

• MGBE has a DMA master. The guest programs descriptors with arbitrary physical addresses. Without an SMMU context configured by something trusted, that DMA engine can read or write anywhere in physical RAM — seL4 kernel memory, other PD memory, libvmm's own pages. seL4's stage-2 isolation is meaningless against a peripheral the guest controls.
• No traffic mediation. Packets flow directly between guest and wire. The seL4 side has zero visibility — can't firewall, can't sniff, can't pause. The whole "trusted base sees what the guest does on the network" research point disappears.
• BPMP/clock access leaks. Bring-up needs BPMP IPC for clocks/resets/power-domains. Hand BPMP to the guest and it can also turn off the GPU, the display, or other CPU clusters — anything the BPMP firmware controls.

Path B moves all of that into a trusted protection domain. The guest now sees a plain virtio-net device. The full PD layout looks like this:

                ┌─────────────────────────────────────┐
                │  CLIENT_VMM (prio 100)              │
                │   client_vmm.elf                    │
                │   ┌───────────────────────────────┐ │
                │   │ client_linux  (VirtualMachine)│ │
                │   │   guest sees:                 │ │
                │   │     virtio-net@160000         │ │
                │   │     MAC 02:c2:0a:00:01:01     │ │
                │   │     192.168.100.180           │ │
                │   └───────────────────────────────┘ │
                └────────────────▲────────────────────┘
                                 │  virtio queues
                                 ▼
                ┌─────────────────────────────────────┐
                │  client0_net_copier (prio 200)      │
                │   network_copy.elf  [stock sDDF]    │
                └────────────────▲────────────────────┘
                                 │ sDDF net queues
                   ┌─────────────┴─────────────┐
                   ▼                           ▼
       ┌────────────────────┐       ┌────────────────────┐
       │ net_virt_rx (200)  │       │ net_virt_tx (200)  │
       │ network_virt_rx.elf│       │ network_virt_tx.elf│
       │   [stock sDDF]     │       │   [stock sDDF]     │
       └─────────▲──────────┘       └──────────┬─────────┘
                 │                             │
                 └──────────────┬──────────────┘
                                ▼
                ┌─────────────────────────────────────┐
                │  eth_driver (prio 200)              │
                │   eth_driver.elf  ← NEW (Path B)    │
                │                                     │
                │   maps into PD vaddr space:         │
                │     0x50000000  bpmp_tx  (shmem)    │
                │     0x50001000  bpmp_rx  (shmem)    │
                │     0x50002000  hsp_dbell           │
                │   plus MGBE MMIO + IRQ              │
                │                                     │
                │   talks to: BPMP (clk/reset MRQs)   │
                │             AQR113C PHY (MDIO C45)  │
                │             XPCS UPHY (init only)   │
                └────────────────▲────────────────────┘
                                 │
                                 ▼
                        ┌────────────────┐
                        │  T234 MGBE0    │
                        │  + AQR113C PHY │
                        │  + RJ45        │
                        └────────────────┘

The eth_driver PD is the only thing in the system that touches MGBE registers, BPMP shmem, or the HSP doorbell. The guest has no DMA capability beyond its own RAM, no view of MAC registers, no BPMP access. net_virt_rx, net_virt_tx and network_copy are stock upstream sDDF binaries — we only had to write eth_driver. A future "firewall PD" or "sniffer PD" slots in cleanly between net_virt_rx and the copier without touching the guest at all.

What had to be written

sDDF doesn't ship a Tegra MGBE driver. We wrote one (~1,700 LOC of BSD-2 across ethernet.c, bpmp.c, aquantia.c, xpcs_pcs.c) using OE4T's nvethernetrm register headers (MIT) for the MGBE/XGMAC core, with a clean-room clause-45 driver for the AQR113C and a clean-room BPMP IVC client. The driver does its own:

• BPMP IPC handshake to gate 8 MGBE0 clocks + cycle 2 resets (bpmp.c; same wire protocol as ATF's bpmp_ipc/);
• XPCS UPHY lane bring-up — the ~130-LOC sequence from mainline's dwmac-tegra.c, rewritten clean-room;
• AQR113C clause-45 autoneg with vendor advertisement registers (aquantia.c, designed to drop into dep/sddf/drivers/network/phy/aquantia/ later);
• Live link supervisor in handle_irq() that reacts to MAC_ISR.LSI, decodes the negotiated speed, and keeps MAC TMCR aligned.

The five bugs that took the longest

"Driver compiles, link comes up, packets flow" took five register-level fixes that no amount of reading vendor headers would have surfaced. The unblocking diagnostic was to boot the working Linux kernel (Section 5's passthrough Alpine), ssh in, dump every relevant MGBE register via a small mmap("/dev/mem")-based reader, then diff against our driver's writes. Highlights:

1. Wrong ring-length register offsets. MGBE_DMA_CHX_TDRL and RDRL are at 0x3130 and 0x3134 in real MGBE/XGMAC2 (matches upstream Linux dwxgmac2.h), not 0x3128/0x3130 as the offsets I was deriving suggested. The result: RX ring length register held 0x20000000 (low 10 bits = 0), MGBE thought the ring had zero descriptors and silently dropped almost all received packets.
2. Misleading vendor macro names. nvethernetrm's MGBE_DMA_CHX_TX_CNTRL2 and RX_CNTRL2 macros target the same offsets as the ring-length registers above. Writing the ORRQ/OWRQ values they suggest stomped the ring lengths.
3. SPH (Split Header) bit on by default. Alpine's working CHX_CTRL = 0x01010000 includes bit 24, which makes MGBE write each frame across two descriptors (header in one, payload in the next). Linux's stmmac handles SPH; sDDF's flat net_buff_desc_t doesn't. Disabled it.
4. Driver MAC didn't match guest virtio-net MAC. sdfgen auto-generates a MAC for each virtio-net device; net_virt_rx routes inbound packets by destination MAC. The driver's pinned 02:c2:0a:00:01:01 and the guest's auto-MAC didn't match, so unicast packets had no client to route to and got dropped. Fix: pin both ends to the same MAC in meta.py.
5. Half a dozen smaller register-state diffs. DMA_SBUS, CHX_TX_CTRL, CHX_RX_CTRL, CHX_INTREN — all had values the docs would let you choose, but the working Linux kernel had picked specific bit patterns we needed to match (notably TIE for TX completion IRQ, which we had been omitting in favour of just the NIE umbrella).

The "diff against a working kernel via /dev/mem" technique unlocked everything in one session. Vendor docs and even mainline driver source are useful, but neither tells you what your specific board firmware ended up programming — the live state of a working kernel does.

Result

$ ssh root@192.168.100.180
Linux (none) 6.6.1 #9 SMP PREEMPT aarch64
Alpine Linux 3.19.1
~ # ip addr show eth0
2: eth0: <BROADCAST,MULTICAST,UP,LOWER_UP> mtu 1500 qdisc pfifo_fast state UP qlen 1000
    link/ether 02:c2:0a:00:01:01 brd ff:ff:ff:ff:ff:ff
    inet 192.168.100.180/24 brd 192.168.100.255 scope global eth0

Same Alpine, same IP, same MAC as Section 5's passthrough variant — but the route the bytes take is now seL4-mediated. The guest has zero direct hardware capability beyond what its virtio-net device exposes. The same trusted-driver pattern carries over unchanged to the L4T-as-guest plan in Section 7: keep GPU/HDMI passthrough for CUDA & display, but route eth0 through Path B.

7. Repository Structure

All AGX changes live on orin-agx branches in the github.com/potanin forks. Each repo's branch is small — the heavy lifting was done on orin-nano; AGX adds a sibling platform plus the libvmm-only HCR_TID3 trap.

kernel/ — potanin/seL4 (6 files)

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

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

microkit — potanin/microkit (3 files)

libvmm — potanin/libvmm (10 files)

8. Coming soon — GPU passthrough & L4T as guest

Section 6 already showed the seL4-mediated network working with Alpine. The remaining piece is the graphics stack — bringing CUDA, NVDISPLAY/HDMI, and the rest of the L4T stack online under libvmm with the same trusted-base story.

Phase 2 (started) — mainline graphics stack

tegra-host1x and tegra-vic already bind under our minimal libvmm; /dev/dri/card0 exists. The actual GA10B Ampere GPU has no upstream driver in mainline today — Nouveau doesn't yet support Tegra Ampere — so a real GPU device is blocked on upstream Nouveau work.

Phase 3 (started) — L4T as the libvmm guest

For CUDA / HDMI / proper GPU we need NVIDIA's downstream stack, which means running L4T's kernel and userspace under libvmm. First milestone reached: L4T's 5.15.148-tegra kernel boots successfully under our libvmm, runs init, drops to a shell, and nvethernet / nvgpu modules load (binding still requires extracting the rich nvidia,* properties from L4T's NV-DTB into our guest device tree).

The end-state target: pass GPU + NVDISPLAY through to the L4T guest directly, but route eth0 through Section 6's sDDF stack — the same trusted-driver pattern that already works for Alpine. Once the L4T guest boots far enough to bring up the network, it'll inherit the seL4-mediated path for free, and a small "firewall PD" can slot in between net_virt_rx and the copier. Future post when GPU passthrough lands.