security: enforce restricted allowlist manifest
ober
b70fd0f8ab6125c39f9488026668cc86fc8a1ef7
--- a/docs/kimi3-security-recommmendations.md +++ b/docs/kimi3-security-recommmendations.md @@ -390,30 +390,26 @@ controls that already exist individually. API. ### K3-P0-03 — Prove the restricted-environment allowlist closed -**Serves:** G1, G4. **Effort:** 2–3 days. **Status:** mechanical closure -gate landed 2026-07-27; full reachability audit through Chez internals remains -open. +**Serves:** G1, G4. **Effort:** 2–3 days. **Status:** mechanical closure, +escape, and documentation-contract gate landed 2026-07-27; formal +reachability proof through Chez internals remains P3. -The allowlist is Jerboa's crown jewel; it currently rests on manual curation. +The allowlist is Jerboa's crown jewel. It now has a CI-enforced manifest in +`security-reference.md` §2, so code and documentation drift fails `make audit`. - **Where:** new `tools/check-restrict-closure.ss`; `lib/std/security/restrict.ss`. -- **Do:** (a) Mechanically verify every symbol in `safe-bindings` exists in - the pinned Chez version (catches typos that silently *widen* to - nothing or, worse, drift after a Chez upgrade). (b) Forbid-list sweep: - assert none of `system process open-*-file foreign-* load eval compile* - getenv putenv fork-thread import library call/cc call-with-current-continuation - gensym read read-eval` appears. (c) Reachability audit: expand each allowed - binding's definition in the vendored Chez source and flag any that can - reach a forbidden primitive (e.g. a seemingly-safe builtin that calls - `system` internally). Start with a documented manual audit table; automate - what's automatable. (d) Publish the resulting per-binding justification - into `security-reference.md` §2. -- **Accept:** `make audit` runs the checker; removing a binding fails CI if - any doc/test references it; adding a binding requires editing the - justification table. A unit test evaluates escape attempts - (`(eval ...)`, `(system ...)`, `((foreign-procedure ...))`, macro-based - smuggling) inside `restricted-eval` and asserts `&assertion`/`unbound` - failures. +- **Done:** (a) `tools/check-restrict-closure.ss` constructs the restricted + environment, which mechanically verifies every symbol in `safe-bindings` + exists in the pinned Chez runtime. (b) The checker rejects dangerous + exact/prefix classes including `system`, file/process/environment access, + `foreign-*`, `load`, `eval`, `compile*`, `fork-thread`, imports, + continuations, `gensym`, and raw `read`. (c) The checker parses the audited + allowlist manifest in `security-reference.md` §2 and requires it to match + `safe-bindings` exactly and in order. (d) K3 regression tests cover + `(eval ...)`, `(system ...)`, `foreign-procedure`, `call/cc`, and + macro-based smuggling inside `restricted-eval`. +- **Remaining:** formal or source-expanded reachability proof through Chez + internals, tracked as P3-06. ### K3-P0-04 — Triage and close raw `read` / native FASL paths on untrusted input **Serves:** G1. **Effort:** 3–5 days. **Status:** first scanner-driven --- a/docs/security-reference.md +++ b/docs/security-reference.md @@ -46,19 +46,123 @@ Creates an evaluation environment containing only approved bindings. Uses Chez S - constructs the restricted environment, which fails if any listed Chez binding is missing in the pinned runtime; - rejects duplicate bindings and dangerous exact/prefix classes such as - `system`, `eval`, `gensym`, `foreign-*`, `compile*`, and `open-*-file`; + `system`, `eval`, `read`, `gensym`, environment access, `foreign-*`, + `compile*`, and `open-*-file`; - evaluates escape attempts for process execution, `eval`, FFI, file output, - `gensym`, and `call/cc` and requires all of them to fail; + `gensym`, `call/cc`, direct imports, and macro smuggling and requires all of + them to fail; +- parses the allowlist manifest below and requires it to match + `safe-bindings` exactly, in order; - keeps an allowed arithmetic/list smoke test so the environment is not merely broken closed. -The current gate is a mechanical closure and escape test. It is not a formal -reachability proof through Chez internals. +The current gate is a mechanical closure, documentation-contract, and escape +test. It is not a formal reachability proof through Chez internals. ### What's allowed Core syntax (`lambda`, `if`, `begin`, `let`, `cond`, `case`, `when`, `unless`, `do`, `define-syntax`, `syntax-rules`, `quasiquote`), arithmetic (including bitwise ops), comparison, booleans, pairs/lists, strings, characters, vectors, bytevectors, symbols, string-port I/O, hashtables, error handling, `apply`, `values`, `dynamic-wind`, `sort`, `format`, `void`. +### Audited Allowlist Manifest + +Each entry is `(category "justification" (bindings ...))`. This block is +machine-checked by `tools/check-restrict-closure.ss`; adding, removing, or +reordering a restricted-environment binding requires updating this manifest in +the same change. + +<!-- restrict-allowlist-begin --> +((core-syntax + "Lexical binding, local control flow, quotation, local mutation, and first-order macro templates; no import, library, process, file, or environment access." + (lambda if begin define set! quote + let let* letrec letrec* + cond case and or when unless do + define-syntax syntax-rules + quasiquote unquote unquote-splicing + let-values)) + (arithmetic + "Pure numeric predicates and operations, including bitwise operations, with no ambient authority." + (+ - * / = < > <= >= zero? positive? negative? + add1 sub1 abs min max gcd lcm + quotient remainder modulo + expt sqrt floor ceiling truncate round + number? integer? rational? real? complex? + exact? inexact? exact->inexact inexact->exact + number->string string->number + bitwise-and bitwise-ior bitwise-xor bitwise-not + bitwise-arithmetic-shift-left bitwise-arithmetic-shift-right)) + (comparison + "Pure identity and equality predicates." + (eq? eqv? equal? not)) + (booleans + "Pure boolean predicates and equality." + (boolean? boolean=?)) + (pairs-lists + "In-memory pair/list construction, traversal, folds, and membership over caller-supplied data." + (cons car cdr pair? null? list? list + caar cadr cdar cddr + length append reverse map for-each + filter fold-left fold-right + assoc assv assq member memv memq + list-ref list-tail + exists for-all)) + (strings + "In-memory string predicates, indexing, copying, conversion, and case transforms." + (string? string-length string-ref string-append + string=? string<? string>? string<=? string>=? + substring string->list list->string + string-upcase string-downcase + string-copy)) + (characters + "Pure character predicates, comparisons, conversion, and case transforms." + (char? char=? char<? char>? + char-alphabetic? char-numeric? char-whitespace? + char->integer integer->char char-upcase char-downcase)) + (vectors + "In-memory vector allocation, indexing, mutation, copying, mapping, and conversion." + (vector? vector vector-length vector-ref vector-set! + make-vector vector->list list->vector vector-copy + vector-fill! vector-map vector-for-each)) + (bytevectors + "In-memory bytevector allocation, indexing, mutation, copying, and UTF-8 conversion." + (bytevector? make-bytevector bytevector-length + bytevector-u8-ref bytevector-u8-set! + bytevector-copy bytevector-copy! + utf8->string string->utf8)) + (symbols + "Symbol predicates and string conversion; `gensym` is excluded, and callers must still bound untrusted symbol creation at parser boundaries." + (symbol? symbol->string string->symbol)) + (control + "Procedure application, multiple values, and dynamic-wind; continuations via `call/cc` are excluded." + (apply call-with-values values + dynamic-wind)) + (hashtables + "In-memory hash table allocation, lookup, mutation, enumeration, sizing, and pure hash functions." + (make-hashtable make-eq-hashtable + hashtable? hashtable-ref hashtable-set! + hashtable-delete! hashtable-contains? + hashtable-keys hashtable-entries + hashtable-size + equal-hash string-hash symbol-hash)) + (string-port-io + "String-port-only I/O and character I/O on caller-provided ports; file ports, current ports, and raw `read` are excluded." + (open-input-string open-output-string + get-output-string + write display newline + port? input-port? output-port? + eof-object? eof-object + read-char peek-char write-char)) + (errors + "Condition construction, handlers, guards, and assertion reporting; no process exit or debugger entry." + (error assert assertion-violation + condition? message-condition? condition-message + guard with-exception-handler raise)) + (misc + "Pure formatting/sorting helpers and void value construction." + (void + sort + format))) +<!-- restrict-allowlist-end --> + ### What's blocked - All file I/O (`open-input-file`, `open-output-file`, etc.) --- a/tests/security/test-k3-regressions.ss +++ b/tests/security/test-k3-regressions.ss @@ -75,6 +75,14 @@ (check "K3-AI-01 restricted eval blocks system" (raises? (lambda () (restricted-eval-string "(system \"true\")"))) => #t) +(check "K3-P0-03 restricted eval blocks eval" + (raises? (lambda () (restricted-eval-string "(eval '(+ 1 2))"))) => #t) +(check "K3-P0-03 restricted eval blocks call/cc" + (raises? (lambda () (restricted-eval-string "(call/cc (lambda (k) (k 1)))"))) => #t) +(check "K3-P0-03 restricted eval blocks macro smuggling" + (raises? (lambda () + (restricted-eval-string + "(begin (define-syntax go (syntax-rules () [(_) (system \"true\")])) (go))"))) => #t) (check "K3-AI-14 run-safe thunk entry is fail-closed" (raises-pred? sandbox-error? (lambda () (run-safe (lambda () 1)))) => #t) (check "K3-AI-01 run-safe-eval blocks system" --- a/tests/test-native-loader-policy.sh +++ b/tests/test-native-loader-policy.sh @@ -94,8 +94,15 @@ if test "$(id -u)" -ne 0; then exit 1 fi - # A production home beneath a group-writable checkout is rejected. - if env -u JERBOA_NATIVE_LIB -u JERBOA_DEV_NATIVE JERBOA_HOME="$root" \ + # A production home beneath a group-writable component is rejected. Build + # the fixture explicitly instead of relying on the checkout permissions. + mkdir -p "$trusted_tmp/group-writable-production/lib" + cp "$bundled_native" "$trusted_tmp/group-writable-production/lib/$(basename "$bundled_native")" + chmod go-w "$trusted_tmp/group-writable-production/lib" \ + "$trusted_tmp/group-writable-production/lib/$(basename "$bundled_native")" + chmod g+w "$trusted_tmp/group-writable-production" + if env -u JERBOA_NATIVE_LIB -u JERBOA_DEV_NATIVE \ + JERBOA_HOME="$trusted_tmp/group-writable-production" \ "$scheme" --libdirs "$root/lib:$root/vendor/jsqlite/src" \ --script "$root/tests/test-crypto-digest.ss" >/dev/null 2>&1; then echo "group-writable production JERBOA_HOME was accepted" >&2 --- a/tools/check-restrict-closure.ss +++ b/tools/check-restrict-closure.ss @@ -7,12 +7,20 @@ (define errors '()) (define warnings '()) +(define documentation-path "docs/security-reference.md") +(define allowlist-begin-marker "<!-- restrict-allowlist-begin -->") +(define allowlist-end-marker "<!-- restrict-allowlist-end -->") + (define forbidden-exact '(system process load eval getenv putenv fork-thread import library - call/cc call-with-current-continuation gensym read-eval + call/cc call-with-current-continuation gensym read read-eval open-input-file open-output-file call-with-input-file call-with-output-file delete-file rename-file file-exists? directory-list current-directory - compile compile-file compile-program foreign-procedure)) + current-input-port current-output-port current-error-port + scheme-environment interaction-environment top-level-value + define-top-level-value set-top-level-value! exit + compile compile-file compile-library compile-program + foreign-procedure load-shared-object)) (define escape-attempts '(system-call "(system \"id\")" @@ -20,7 +28,9 @@ ffi-call "((foreign-procedure \"exit\" (int) void) 0)" gensym-call "(gensym)" file-output "(open-output-file \"/tmp/jerboa-restrict-escape\")" - callcc-call "(call/cc (lambda (k) (k 1)))")) + callcc-call "(call/cc (lambda (k) (k 1)))" + import-call "(import (chezscheme))" + macro-smuggle "(begin (define-syntax go (syntax-rules () [(_) (system \"id\")])) (go))")) (define (add-error msg) (set! errors (cons msg errors))) (define (add-warning msg) (set! warnings (cons msg warnings))) @@ -35,6 +45,17 @@ [m (string-length s)]) (and (>= m n) (string=? suffix (substring s (- m n) m))))) +(define (all? pred xs) + (let loop ([rest xs]) + (or (null? rest) + (and (pred (car rest)) (loop (cdr rest)))))) + +(define (append-map-local proc xs) + (let loop ([rest xs] [out '()]) + (if (null? rest) + (apply append (reverse out)) + (loop (cdr rest) (cons (proc (car rest)) out))))) + (define (symbol-prefix? prefix sym) (string-prefix? prefix (symbol->string sym))) @@ -55,6 +76,78 @@ [(memq (car rest) seen) (loop (cdr rest) seen (cons (car rest) dups))] [else (loop (cdr rest) (cons (car rest) seen) dups)]))) +(define (list-missing wanted available) + (let loop ([rest wanted] [missing '()]) + (cond + [(null? rest) (reverse missing)] + [(memq (car rest) available) (loop (cdr rest) missing)] + [else (loop (cdr rest) (cons (car rest) missing))]))) + +(define (doc-category? value) + (and (list? value) + (= (length value) 3) + (symbol? (car value)) + (string? (cadr value)) + (> (string-length (cadr value)) 0) + (list? (caddr value)) + (all? symbol? (caddr value)))) + +(define (read-allowlist-manifest) + (guard (exn [else + (add-error + (format "cannot read ~a allowlist manifest: ~a" + documentation-path + (with-output-to-string + (lambda () (display-condition exn))))) + #f]) + (let* ([text (read-file-string documentation-path)] + [begin-pos (string-contains text allowlist-begin-marker)] + [end-pos (string-contains text allowlist-end-marker)]) + (cond + [(not begin-pos) + (add-error (format "~a is missing ~a" documentation-path allowlist-begin-marker)) + #f] + [(not end-pos) + (add-error (format "~a is missing ~a" documentation-path allowlist-end-marker)) + #f] + [else + (let* ([start (+ begin-pos (string-length allowlist-begin-marker))] + [block (substring text start end-pos)]) + (if (<= end-pos start) + (begin + (add-error (format "~a allowlist manifest markers are reversed" documentation-path)) + #f) + (let* ([port (open-input-string block)] + [form (read port)] + [extra (read port)]) + (when (eof-object? form) + (add-error (format "~a allowlist manifest is empty" documentation-path))) + (unless (eof-object? extra) + (add-error (format "~a allowlist manifest has more than one top-level form" documentation-path))) + (if (and (list? form) (all? doc-category? form)) + form + (begin + (add-error + (format "~a allowlist manifest must be ((category \"reason\" (symbols ...)) ...)" + documentation-path)) + #f)))))])))) + +(define (check-documentation-contract) + (let ([categories (read-allowlist-manifest)]) + (when categories + (let* ([doc-symbols (append-map-local caddr categories)] + [doc-dups (duplicates doc-symbols)] + [missing-doc (list-missing safe-bindings doc-symbols)] + [extra-doc (list-missing doc-symbols safe-bindings)]) + (unless (null? doc-dups) + (add-error (format "allowlist documentation contains duplicate bindings: ~s" doc-dups))) + (unless (null? missing-doc) + (add-error (format "safe-bindings missing from documentation: ~s" missing-doc))) + (unless (null? extra-doc) + (add-error (format "documented bindings absent from safe-bindings: ~s" extra-doc))) + (when (and (null? missing-doc) (null? extra-doc) (not (equal? doc-symbols safe-bindings))) + (add-error "allowlist documentation contains the right set in the wrong order")))))) + (define (attempt-fails? env source) (guard (exn [else #t]) (restricted-eval-string source env) @@ -100,12 +193,14 @@ (define (main) (check-safe-bindings) + (check-documentation-contract) (let ([env (check-environment-constructs)]) (when env (check-allowed-smoke env) (check-escape-attempts env))) (display "restrict-closure:\n") (display " safe-bindings: ") (write (length safe-bindings)) (newline) + (display " documented-bindings: enforced by docs/security-reference.md\n") (display " forbidden-patterns: exact, foreign-*, compile*, open-*-file\n") (display " escape-attempts: ") (write (/ (length escape-attempts) 2)) (newline) (for-each