hermes-brain/ideas/lisp-machine-security.org

Lisp Machine Security — Unified Memory Threat Model

On a bare metal Lisp Machine with a unified Lisp image, the defense-in-depth provided by the OS kernel disappears. The gate stack and the code it protects share a single address space. An attacker who exploits a memory corruption in the browser renderer can modify the gate stack's permission tables, the policy engine's state, or the ACL2 prover's decision output. There is no kernel underneath to catch them.

This note analyzes the threat model and proposes a hardware-enforced privilege separation within the single Lisp image.

The problem

In the conventional layered model (Linux + SBCL + Passepartout), there is defense in depth. Even if the gate stack has a bug, Linux provides seccomp, namespaces, file permissions, and process isolation as a safety net. If SBCL segfaults, the kernel catches it.

On a bare metal Lisp Machine, the model collapses:

``` Everything (agent, editor, browser, shell, gate stack, ACL2) └── RISC-V hardware (no kernel) ```

The only protection is that the gate stack is verified by ACL2 to be correct. But ACL2 verification is static — it proves properties about source code. At runtime, a memory corruption in the same image invalidates the entire proof. "All defense is symbolic" is exactly right.

The solution: hardware-enforced privilege zones within the Lisp image

RISC-V provides three hardware privilege levels: M-mode (machine), S-mode (supervisor), and U-mode (user). Physical Memory Protection (PMP) enforces access control at the hardware bus level — it cannot be bypassed by software, even by code running in S-mode if configured in M-mode. The key: use these mechanisms to create zones within the shared Lisp address space.

Three-layer architecture

Layer 1 — The Gate Core (M-mode, ~500 lines of verified assembly/Lisp) One core runs permanently in M-mode with PMP configuration that cannot be modified by any other core.

• Configures PMP at boot into three fixed zones: M-zone (gate core), S-zone (gate stack), U-zone (untrusted)
• Hashes and verifies the S-mode binary against a signed Merkle manifest before booting it
• Monitors the gate stack core via watchdog timer
• Cannot be read or written from any other privilege level
• No MMU, no interrupt handling for U-mode — just PMP + timer + sanity checking
• The absolute smallest possible trusted computing base
• Loaded from ROM with a hardware root of trust

Layer 2 — The Gate Stack (S-mode, ~2,000 lines of verified Lisp) The ACL2 verifier, Screamer, policy engine, permission tables, and ECALL handler.

• Runs in supervisor mode with a thin kernel: just an ECALL dispatcher and a bounded memory allocator
• Its data structures (permissions table, policy objects, authentication state, hash of loaded binaries) live in S-zone memory protected by PMP
• U-mode cannot read or write S-zone — hardware enforced at every bus access
• Receives requests from U-mode exclusively through ECALL: "may I write to path X?", "should I execute command Y?", "query fact Z"
• The ECALL handler is the entire enforcement boundary — about 500 lines of Lisp that must correctly validate every request

Layer 3 — Untrusted Code (U-mode, arbitrarily large) The LLM interface, browser renderer, Nyxt, Lish shell when executing user commands, any LLM-generated or external code.

• Lives in U-zone memory
• Cannot access S-zone or M-zone memory (PMP enforced)
• Cannot execute privileged instructions (hardware enforced)
• Can only communicate with the gate stack via ECALL — a narrow message-passing interface
• Shared heap with S-mode for GC efficiency, but PMP prevents U-mode from reading S-mode objects

Boot chain

1. ROM loads the M-mode gate core binary, verified by hardware signature against an eFuse key
2. Gate core configures PMP to create the three zones, protecting its own memory and the gate stack's memory
3. Gate core hashes the gate stack binary, compares against signed manifest stored in M-zone
4. Gate core loads gate stack into S-mode memory, ACL2 verifies the binary structure
5. Gate stack creates a restricted heap region for U-mode with bounds checked by PMP
6. U-mode code is loaded and started — it has no way to access S-mode or M-mode memory

Failure mode analysis

U-mode browser bug exploited. The attacker controls U-mode. They can call ECALL with arbitrary arguments. The gate stack verifies every ECALL. The attacker cannot read S-mode memory (PMP), cannot execute privileged instructions (hardware), cannot modify the gate stack's state (PMP). The attacker is limited to what the ECALL handler allows — which is the gate stack's policy.

ECALL handler bug. The critical vulnerability. If the ECALL handler has a buffer overflow, a parsing error, or a logic mistake in permission checking, an attacker in U-mode can trick it into granting unauthorized access. This is the single point of failure for the entire system. Mitigation: the ECALL handler must be the most rigorously verified component. ACL2 must prove its correctness for all valid and all invalid inputs. It must be minimal — no filesystem access, no networking, no string parsing beyond what's needed to validate request structure.

Gate stack accepts hostile input. U-mode sends a crafted file path designed to exploit a parsing bug in the path validator. If the gate stack has a vulnerability in its input processing logic, it can be compromised from below even though hardware isolation prevents direct memory access. Mitigation: the gate stack must treat all U-mode input as hostile. It must use bounded buffers, no recursion in parsing, and ACL2-verified parsing functions.

Speculative execution. PMP does not prevent speculative reads. A Spectre gadget in U-mode can leak S-mode memory through cache timing side channels. Mitigation: use RISC-V Zkt (constant-time) extension or disable speculation on the gate core entirely. The gate core is CPU-bound verification logic with no need for branch prediction.

DMA attack via PCIe. An attacker who compromises a network card can attempt DMA into arbitrary physical memory. IOMMU constrains DMA: devices can only write to designated I/O buffers in U-zone. Gate stack memory in S-zone is outside the IOMMU window. The IOMMU must be configured before PCIe devices are initialized.

Physical attack. Cold boot, bus probing, JTAG — all bypass PMP and IOMMU. Mitigation: memory encryption with a hardware key stored in eFuse (RISC-V Scalar Cryptography extension). Out of scope for the first iteration; the system assumes a trusted physical environment.

ACL2 trust problem. ACL2 verifies the gate stack. But ACL2 itself is ~50,000 lines of Lisp. If ACL2 has a bug, it could "prove" that an incorrect gate stack is correct. Mitigation: ACL2's proof kernel is ~1,200 lines and has been verified by ACL2 itself (the bootstrap). This is the best-known technique for prover trust, but it is not a formal proof of ACL2's correctness — faith in the bootstrap is faith in the hardware that ran it and the human who reviewed the initial seed.

Comparison with conventional layered security

The conventional Linux approach: TCB is ~28 million lines of C across kernel, drivers, and runtime. Defense in depth from many layers. But each layer adds attack surface.

The Lisp Machine approach: TCB is ~2,500 lines of verified Lisp (M-mode gate core + S-mode gate stack). Attack surface is ~500 lines of ECALL handler. The TCB is roughly 10,000x smaller. This security advantage creates moats — a competitor would need to match both the hardware isolation and the verified codebase.

The fundamental trade: fewer layers, less depth, but each layer is simpler, smaller, and verified. A bug in the ECALL handler is catastrophic. A bug in the Linux kernel might be contained by seccomp or namespaces. The question is which is more likely: a bug in 500 lines of verified Lisp, or a bug in 28 million lines of C that is not contained by the remaining depth?

For most threat models, the Lisp Machine is more secure. The ECALL handler is a narrow, structured interface. There is no filesystem, no networking, no process management, no driver model, no /proc, no ptrace, no setuid, no namespace subsystem, no cgroups in the gate stack — each of which is a source of CVEs in Linux.

But this is a single-point-of-failure architecture. If the ECALL handler holds, the system is secure. If it breaks, everything is compromised. There is no fallback. This must be a conscious design choice, not an accident.

Gaps in the current design

None of this is in the architecture documents. The following are not yet specified — these architectural innovations are potential candidates for patent strategy:

1. PMP region layout — exactly what is protected and by which region
2. ECALL handler specification — the exact interface, request types, validation logic, and error handling
3. M-mode gate core specification — what it does, how it's verified, how it loads
4. IOMMU configuration for PCIe devices
5. Watchdog strategy — what happens if the gate core freezes
6. Side-channel mitigation — speculation control, timing attacks
7. ACL2 trust documentation — the bootstrap chain and what it means for the gate stack's verification
8. The boot attestation protocol — how the gate core verifies the gate stack before loading it
9. Zone transition costs — how many cycles does an ECALL take, and does that affect the 10-80-10 ratio