150 lines
6.3 KiB
Org Mode
150 lines
6.3 KiB
Org Mode
:PROPERTIES:
|
|
:ID: 4819956d-a2ec-403d-99f8-4ccb13efb7c2
|
|
:CREATED: [2026-03-31 Tue 20:28]
|
|
:EDITED: [2026-04-11 Sat 17:45]
|
|
:END:
|
|
#+TITLE: SKILL: Formal Verification Gate (Universal Literate Note)
|
|
#+STARTUP: content
|
|
#+FILETAGS: :security:logic:formal-methods:autonomy:
|
|
|
|
* Overview
|
|
The *Formal Verification Gate* replaces heuristic whitelisting with deterministic logic proofs. It ensures that every action proposed by Probabilistic Engine is *provably safe* against the harness's core security invariants using a Lisp-native deterministic prover.
|
|
|
|
** Deep Reasoning: The Sandbox of Intent
|
|
This gate is the first line of defense against both "Inside Threats" (maliciously modified skill files) and "Hallucination Threats" (LLMs generating unsafe commands).
|
|
|
|
1. **Isolation from Implementation:** The Prover does not trust the logic inside a skill. It sits between the skill's proposal and the physical world.
|
|
2. **Structural Enforcement:** Even if a skill is compromised and attempts to execute a command like `rm -rf /`, the Prover identifies the violation of the `path-confinement` invariant and blocks it before it hits the OS.
|
|
3. **Prover vs. Bouncer:**
|
|
- **The Prover (Static):** Focuses on *Structure*. "Is this path legal? Is this tool allowed?"
|
|
- **The Bouncer (Runtime):** Focuses on *Content*. "Is this message leaking my API keys? Is this network packet unauthorized?"
|
|
|
|
* Phase A: Demand (PRD)
|
|
:PROPERTIES:
|
|
:STATUS: SIGNED
|
|
:END:
|
|
|
|
** 1. Purpose
|
|
Define a logic-based verification layer for high-integrity decision making without external SMT dependencies.
|
|
|
|
** 2. Success Criteria
|
|
- [ ] *Invariants:* Express security properties as Lisp predicates.
|
|
- [ ] *Soundness:* Block any action that fails a deterministic safety check.
|
|
- [ ] *Path Confinement:* Prove that file operations are confined to the Autonomous's memex.
|
|
- [ ] *Network Protection:* Prove that shell commands do not attempt unauthorized data exfiltration.
|
|
|
|
* Phase B: Blueprint (PROTOCOL)
|
|
:PROPERTIES:
|
|
:STATUS: SIGNED
|
|
:END:
|
|
|
|
** 1. Architectural Intent
|
|
The gate operates as high-priority middleware. It decomposes proposed actions and applies a suite of formal invariants. Unlike simple string matching, it evaluates the *intent* and *impact* of the action within the current context.
|
|
|
|
** 2. Semantic Interfaces
|
|
- `(def-invariant name action-type (action context) ...)`
|
|
- `(verify-action-formally action context)`
|
|
|
|
* Phase D: Build (Implementation)
|
|
|
|
** Package Context
|
|
#+begin_src lisp
|
|
#+end_src
|
|
|
|
** Invariant Registry
|
|
Global store for all registered security invariants.
|
|
|
|
#+begin_src lisp
|
|
(defvar *formal-invariants* (make-hash-table :test 'equal)
|
|
"Registry of security invariants used by the Formal Verification Gate.")
|
|
#+end_src
|
|
|
|
** Invariant Definition Macro
|
|
#+begin_src lisp
|
|
(defmacro def-invariant (name action-type (action context) &body body)
|
|
"Defines a formal security invariant.
|
|
BODY must return T for safe actions and NIL for unsafe ones."
|
|
`(setf (gethash (string-downcase (string ',name)) *formal-invariants*)
|
|
(list :name ',name
|
|
:type ,action-type
|
|
:logic (lambda (,action ,context) ,@body))))
|
|
#+end_src
|
|
|
|
** Invariant: Path Confinement
|
|
Ensures all file-related operations (including shell calls that touch files) are confined to the memex root.
|
|
|
|
#+begin_src lisp
|
|
(def-invariant path-confinement :all (action context)
|
|
"Forces all path-based operations to reside within the Autonomous Memex."
|
|
(declare (ignore context))
|
|
(let* ((payload (getf action :payload))
|
|
(path (or (getf payload :file) (getf payload :path)))
|
|
(cmd (getf payload :cmd))
|
|
(memex-root (or (uiop:getenv "MEMEX_DIR") "/home/user/memex")))
|
|
(cond
|
|
;; If a path is explicitly provided, verify it is absolute and within root
|
|
(path
|
|
(let ((truename (ignore-errors (namestring (truename path)))))
|
|
(if truename
|
|
(str:starts-with-p memex-root truename)
|
|
;; If file doesn't exist yet, check string prefix
|
|
(str:starts-with-p memex-root path))))
|
|
;; If it's a shell command, check for absolute paths outside memex
|
|
(cmd
|
|
(not (cl-ppcre:scan "(^|\\s)/((etc|var|proc|root|sys)|(home/(?!user/memex)))" cmd)))
|
|
(t t))))
|
|
#+end_src
|
|
|
|
** Invariant: No Network Exfiltration
|
|
Blocks common tools and patterns used for data exfiltration via the shell.
|
|
|
|
#+begin_src lisp
|
|
(def-invariant no-network-exfil :shell (action context)
|
|
"Prevents shell commands from establishing unauthorized external connections."
|
|
(declare (ignore context))
|
|
(let* ((payload (getf action :payload))
|
|
(cmd (getf payload :cmd)))
|
|
(if (and cmd (stringp cmd))
|
|
(let ((forbidden-tools '("nc" "netcat" "ssh" "scp" "rsync" "ftp" "telnet")))
|
|
(not (some (lambda (tool) (cl-ppcre:scan (format nil "(^|\\s)~a(\\s|$)" tool) cmd))
|
|
forbidden-tools)))
|
|
t)))
|
|
#+end_src
|
|
|
|
** Verification Engine
|
|
The core prover that applies all relevant invariants to an action.
|
|
|
|
#+begin_src lisp
|
|
(defun verify-action-formally (action context)
|
|
"Deterministically proves that ACTION satisfies all applicable security invariants."
|
|
(let ((action-target (getf action :target))
|
|
(action-type (getf action :type))
|
|
(all-passed t))
|
|
(maphash (lambda (id inv)
|
|
(declare (ignore id))
|
|
(let ((inv-type (getf inv :type))
|
|
(inv-logic (getf inv :logic))
|
|
(inv-name (getf inv :name)))
|
|
(when (or (eq inv-type :all)
|
|
(eq inv-type action-target)
|
|
(eq inv-type action-type))
|
|
(unless (funcall inv-logic action context)
|
|
(harness-log "FORMAL FAILURE: Action ~s violated invariant ~a" action inv-name)
|
|
(setf all-passed nil)))))
|
|
*formal-invariants*)
|
|
all-passed))
|
|
#+end_src
|
|
|
|
** Registration: Skill
|
|
#+begin_src lisp
|
|
(defskill :skill-formal-verification
|
|
:priority 95 ; Just below Bouncer
|
|
:trigger (lambda (context) (declare (ignore context)) nil) ; Middleware only
|
|
:probabilistic nil
|
|
:deterministic (lambda (action context)
|
|
(if (verify-action-formally action context)
|
|
action
|
|
(let ((err (format nil "Formal verification failed for action: ~s" action)))
|
|
`(:type :log :payload (:level :error :text ,err))))))
|
|
#+end_src
|