6.5 KiB
SKILL: Formal Verification Gate (Universal Literate Note)
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).
- Isolation from Implementation: The Prover does not trust the logic inside a skill. It sits between the skill's proposal and the physical world.
- 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.
-
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)
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 Sovereign's memex.
- Network Protection: Prove that shell commands do not attempt unauthorized data exfiltration.
Phase B: Blueprint (PROTOCOL)
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
(in-package :org-agent)Invariant Registry
Global store for all registered security invariants.
(defvar *formal-invariants* (make-hash-table :test 'equal)
"Registry of security invariants used by the Formal Verification Gate.")Invariant Definition Macro
(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))))Invariant: Path Confinement
Ensures all file-related operations (including shell calls that touch files) are confined to the memex root.
(def-invariant path-confinement :all (action context)
"Forces all path-based operations to reside within the Sovereign 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))))Invariant: No Network Exfiltration
Blocks common tools and patterns used for data exfiltration via the shell.
(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)))Verification Engine
The core prover that applies all relevant invariants to an action.
(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))Registration: Skill
(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))))))