diff --git a/ideas/passepartout-economics/common-logic-iso-24707.org b/ideas/passepartout-economics/common-logic-iso-24707.org new file mode 100644 index 0000000..83fc8e3 --- /dev/null +++ b/ideas/passepartout-economics/common-logic-iso-24707.org @@ -0,0 +1,51 @@ +:PROPERTIES: +:ID: 04c2f221-c54f-51e5-b40a-48822cd16d45 +:END: +#+title: Common Logic (ISO 24707) — Relevance to Passepartout +#+filetags: :passepartout:knowledge:logic:standards:iso: + +Common Logic (ISO/IEC 24707) is a framework for first-order logic languages designed for knowledge exchange. It defines an abstract syntax and model-theoretic semantics. Any concrete syntax (dialect) that maps to the abstract syntax inherits the semantics — and all CL dialects are automatically interoperable. + +Three standard dialects: CLIF (Common Logic Interchange Format), CGIF (Conceptual Graph Interchange Format), XCL (XML-based). Additionally, RDF and OWL can be mapped to CL, making them interoperable with any CL dialect. + +**Relevance to Passepartout** + +The fact store interchange format. Passepartout's fact store uses plists internally — fast, native to Lisp, zero serialization cost. But between instances (Agora sync, backup/restore, export), a standardized format is needed. CLIF is a strong candidate because its first-order logic is a direct match for the gate rules ACL2 verifies. A CLIF-to-ACL2 translator is mechanically straightforward — both operate on first-order formulas. + +The dialect architecture mirrors Passepartout. CL's defining insight: define abstract semantics, let any concrete syntax map to it, get interoperability for free. This is the exact same pattern as Passepartout's "one gate stack, many skills" — the gate stack defines the security ontology (abstract semantics), and skills (dialects) map their operations to it. CL's approach validates Passepartout's design choice and provides a theoretical framework for it. + +ISO standard as a credential. For regulated industries, "the knowledge representation follows ISO/IEC 24707" is a strong signal. It says the format is not proprietary, has formal semantics, and has been reviewed by an international body. This matters for HIPAA, SOC2, FedRAMP, and any compliance framework that asks about data representation standards. It is a checkbox that enterprise procurement requires. + +The RDF/OWL bridge. CL has defined translations to RDF and OWL. This means Passepartout can consume knowledge from the semantic web without building a separate RDF parser. The fact store stays in plists internally; CL is the serialization and interchange layer. Any enterprise knowledge graph expressed in OWL can be ingested as CLIF, translated to plists, and verified by ACL2. + +Multiple implementations exist. There are CL reference implementations (some in Lisp) that can be adapted or used as guides rather than writing from scratch. + +**What Common Logic is NOT for Passepartout** + +Not a replacement for ACL2. CL is a knowledge representation standard, not a theorem prover. ACL2 proves theorems about gate rules. CLIF encodes the gate rules themselves. They are complementary: ACL2 verifies CLIF-encoded rule sets. + +Not the internal representation. CLIF is verbose and not optimized for in-process use. The fact store should stay as plists internally. CL is the serialization layer — on the wire between Agora instances, in export files, in backup archives. This is the same pattern as JSON for web APIs: internal data structures are whatever is fastest, JSON is the interchange format. + +Not a dialect to implement. Passepartout should not implement a full CLIF parser. The right approach is a thin translation layer: export plist → CLIF, import CLIF → ACL2-verified → plist. The AC Lisp ecosystem likely has CLIF libraries that can be wrapped. + +**The higher-order question** + +CL allows quantification over predicate and function symbols, which is technically a higher-order feature, despite being marketed as a first-order framework. This is directly relevant to Passepartout's roadmap: the system eventually wants a CIC prover for dependent types, and CL's approach — start from first-order, carefully extend with specific higher-order features — is the same strategy Passepartout uses with ACL2 + macro layers. + +CL's treatment of higher-order features is instructive: it extends first-order semantics with specific mechanisms rather than adopting a full dependent type theory. The result is less expressive but more practical, easier to implement, and easier to verify. Passepartout's planned CIC prover should consider the same trade. + +**Verdict** + +Common Logic is relevant not as something to implement or replace, but as: +1. A natural serialization format for the fact store (Agora Notes, inter-instance sync) +2. An enterprise procurement checkbox (ISO standard) +3. A theoretical validation of Passepartout's dialect-based architecture +4. A bridge to RDF/OWL data sources +5. A cautionary example for the CIC prover design (careful about higher-order scope) + +The right time to integrate it: when Agora Notes need a standard knowledge interchange format for inter-instance communication. Before that, it is a reference worth reading but not implementing. + +See also: +[[file:sufficiency-flip.org][Sufficiency flip]] +[[file:gate-rule-encoding.org][Gate rule encoding]] +[[file:cost-structure.org][Cost structure]] diff --git a/ideas/passepartout-economics/lisp-machine-security.org b/ideas/passepartout-economics/lisp-machine-security.org new file mode 100644 index 0000000..d8b47b5 --- /dev/null +++ b/ideas/passepartout-economics/lisp-machine-security.org @@ -0,0 +1,111 @@ +:PROPERTIES: +:ID: 1c95ce7d-a2db-506a-9608-df68f9ae211b +:END: +#+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. + +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. + +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: + +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 + +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]] diff --git a/ideas/passepartout-economics/passepartout-economics.org b/ideas/passepartout-economics/passepartout-economics.org index 66a5095..2e1129b 100644 --- a/ideas/passepartout-economics/passepartout-economics.org +++ b/ideas/passepartout-economics/passepartout-economics.org @@ -14,6 +14,9 @@ Total addressable market: ~$960B/year across cloud, AI, OS, social media, paymen The business model is the AWS of provable computing: AGPL infrastructure is free, revenue comes from verification appliances, gate rules, certification, namespace registry, hosted PDS, and a compute marketplace. Network effects are positive sum — every instance feeds the regression suite and grows the marketplace. +[[file:lisp-machine-security.org][Lisp Machine security — unified memory threat model]] +[[file:common-logic-iso-24707.org][Common Logic (ISO 24707) — relevance to the triad]] + Key analytical frames: - [[file:investment-thesis.org][Investment thesis — the unified view]] - [[file:lisp-economics.org][Why Lisp is economically viable now]] diff --git a/ideas/passepartout-economics/self-driving-lisp-machine.org b/ideas/passepartout-economics/self-driving-lisp-machine.org index f7aa09b..8c9e47f 100644 --- a/ideas/passepartout-economics/self-driving-lisp-machine.org +++ b/ideas/passepartout-economics/self-driving-lisp-machine.org @@ -14,4 +14,4 @@ Every subdomain involved is software — the most codifiable domain. RISC-V ISA, The Tenstorrent approach is dramatically simpler than FPGA because the microcode is RISC-V assembly (software), not FPGA bitstream (hardware with minutes-per-iteration synthesis). -See also: [[file:verification-appliance.org][Verification appliance]], [[file:time-estimates.org][Time estimates]], [[file:sufficiency-flip.org][Sufficiency flip]], [[file:upgrade-lifecycle.org][Upgrade lifecycle]], [[file:lisp-economics.org][Lisp economics]] +See also: [[file:lisp-machine-security.org][Lisp Machine security]], [[file:verification-appliance.org][Verification appliance]], [[file:time-estimates.org][Time estimates]], [[file:sufficiency-flip.org][Sufficiency flip]], [[file:upgrade-lifecycle.org][Upgrade lifecycle]], [[file:lisp-economics.org][Lisp economics]]