5.7 KiB
5.7 KiB
SKILL: Formal Verification Gate (Universal Literate Note)
Overview
The Formal Verification Gate replaces heuristic whitelisting with symbolic logic proofs. It ensures that every action proposed by System 1 is provably safe against the kernel's core security invariants using a Lisp-native symbolic prover.
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 symbolic 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)
"Symbolically 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)
(kernel-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
:neuro nil
:symbolic (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))))))