Normalize all passepartout-economics to inline wiki links
Replaced every bottom-of-section 'See also:' block with inline Org-mode file: links at the first natural mention in body text. All 29 files across the economics directory now use wiki-style inline cross-references rather than standalone reference blocks.
This commit is contained in:
@@ -4,7 +4,7 @@
|
||||
#+title: Lisp Machine Security — Unified Memory Threat Model
|
||||
#+filetags: :passepartout:security:lisp-machine:pmp:isolation:
|
||||
|
||||
On bare metal 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.
|
||||
On a bare metal [[file:self-driving-lisp-machine.org][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.
|
||||
|
||||
@@ -21,7 +21,7 @@ Everything (agent, editor, browser, shell, gate stack, ACL2)
|
||||
|
||||
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**
|
||||
**The solution: [[file:verification-appliance.org][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.
|
||||
|
||||
@@ -82,7 +82,7 @@ ACL2 trust problem. ACL2 verifies the gate stack. But ACL2 itself is ~50,000 lin
|
||||
|
||||
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.
|
||||
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 [[file:moats.org][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?
|
||||
|
||||
@@ -92,7 +92,7 @@ But this is a single-point-of-failure architecture. If the ECALL handler holds,
|
||||
|
||||
**Gaps in the current design**
|
||||
|
||||
None of this is in the architecture documents. The following are not yet specified:
|
||||
None of this is in the architecture documents. The following are not yet specified — these architectural innovations are potential candidates for [[file:patent-strategy.org][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
|
||||
@@ -103,9 +103,3 @@ None of this is in the architecture documents. The following are not yet specifi
|
||||
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
|
||||
|
||||
See also:
|
||||
[[file:verification-appliance.org][Verification appliance]]
|
||||
[[file:self-driving-lisp-machine.org][Self-driving Lisp Machine]]
|
||||
[[file:moats.org][Moats]]
|
||||
[[file:patent-strategy.org][Patent strategy]]
|
||||
|
||||
Reference in New Issue
Block a user