37 lines
2.5 KiB
Org Mode
37 lines
2.5 KiB
Org Mode
#+TITLE: Root Cause Analysis: Lisp-Native Formal Verification Gate
|
|
#+DATE: 2026-04-11
|
|
#+FILETAGS: :rca:security:formal-verification:autonomy:
|
|
|
|
* Executive Summary
|
|
Implemented a Lisp-Native Deterministic Prover to replace heuristic whitelisting with formal security invariants. This ensures that every high-impact action (shell, file I/O) is mathematically proven safe against the Autonomous's core mandates.
|
|
|
|
* 1. Architectural Shift: Native vs. External
|
|
** Issue
|
|
The initial draft suggested using `Z3`, an external SMT solver. However, `Z3` was not available in the environment and would add significant complexity/bloat to the Docker image.
|
|
** Resolution
|
|
Leveraged Common Lisp's inherent strength in symbol manipulation to build a **Lisp-Native Prover**. Invariants are defined as high-order predicates that operate on the structure of proposed actions. This provides a self-contained, high-performance verification layer.
|
|
|
|
* 2. Issue: Dependency Fragility
|
|
** Symptoms
|
|
System failed to load with `Package STR does not exist`.
|
|
** Root Cause
|
|
Incorrect assumption about the Quicklisp system name vs. the package name. The library is `cl-str` but the Quicklisp system is `str` and the package is `str`.
|
|
** Resolution
|
|
1. Updated `opencortex.asd` to depend on `:str`.
|
|
2. Updated all source code and literate notes to use the `str:` prefix.
|
|
3. Verified via explicit `ql:quickload` in the test runner.
|
|
|
|
* 3. Formal Invariants Implemented
|
|
- **Path Confinement:** Deterministically proves that any file operation or absolute path in a shell command is strictly within the `/home/user/memex` root.
|
|
- **No Network Exfiltration:** Prevents the shell from invoking common exfiltration tools (`nc`, `ssh`, etc.) by inspecting the parsed command structure.
|
|
|
|
* 4. opencortex Mandate Alignment
|
|
** Soundness over Heuristics
|
|
By moving to formal invariants, we have moved from "blacklisting bad things" to "proving safety." Any action that cannot be proven to satisfy all invariants is denied by default.
|
|
** Literate Granularity
|
|
The `org-skill-formal-verification.org` file follows the "one definition per block" mandate, ensuring that the logic of each invariant is individually documented and verifiable.
|
|
|
|
* 5. Permanent Learnings
|
|
- **Tooling Independence:** Whenever possible, prefer native Lisp logic over external binaries for core security gates to reduce the attack surface and deployment complexity.
|
|
- **Environment Consistency:** Always use `(setf (uiop:getenv ...) ...)` for portable environment manipulation in tests.
|