security: lock sandbox macro allowlist
Jaime Fournier <jaimef@linbsd.org>
b2c1e9893b7d66164c00d41c4b242399d151b4ab
--- a/docs/kimi3-security-recommmendations.md +++ b/docs/kimi3-security-recommmendations.md @@ -642,14 +642,15 @@ Taint is opt-in; native sinks don't check it. In the safe prelude, the Macros in sandboxed code can smuggle references to bindings the allowlist excluded, depending on expansion environment semantics. -- **Do:** (a) Write the adversarial test battery first: `syntax-rules` - emitting references to `system`/`eval`/`foreign-procedure`, use of - `datum->syntax` with forged contexts, macro-defined macros. (b) If any - escapes: remove `define-syntax`/`syntax-rules` from `safe-bindings`, or - fence expansion in the restricted environment. (c) If provably closed: - document the proof sketch in `security-reference.md` §13 and lock with - tests. -- **Accept:** battery passes (or feature removed); §13 entry resolved. +- **Status:** complete. Keep `define-syntax`/`syntax-rules` in + `safe-bindings` for first-order local macros. `tools/check-restrict-closure.ss` + and `tests/security/test-k3-regressions.ss` now cover `syntax-rules` + emitting `system`, `eval`, and `foreign-procedure`, `datum->syntax` context + forging, and macro-defined macros. `make restrict-closure-check` reports 12 + failing escape attempts, and `make test-security` reports + `k3-security-regressions: 34 passed`. +- **Accept:** satisfied; the battery passes and `security-reference.md` + documents the proof sketch and regression requirement. ### K3-P1-05 — Crypto modernization: Argon2id, retire OpenSSL legacy paths **Serves:** G1, G5. **Effort:** 1 week. @@ -1017,12 +1018,15 @@ fake confidence happens. - No covert-channel analysis; Chez GC is a timing side channel (P3-07). - Seccomp tables cover x86_64/aarch64 only; Landlock needs Linux 5.13+; Seatbelt/Capsicum have thinner test coverage (P1-08). -- Taint is opt-in until P1-03; native Chez sinks never check it. +- Safe-prelude file/shell/delete sink names now check taint; source marking and + broad propagation remain P1-03 follow-up. - Distributed actor authentication is available in `(std actor transport)` and `(std actor distributed)` authenticated envelopes; compatibility raw serialization remains unauthenticated. -- Path checks are TOCTOU-raceable until P1-02. -- `define-syntax` remains in the sandbox allowlist pending P1-04's proof. +- Path checks use fd/no-follow verification where available; filesystem + capabilities are not whole-process sandboxes. +- `define-syntax` remains in the sandbox allowlist with P1-04's battery locked + in `make audit` and K3 regressions. - `run-safe-eval` output cap is on the formatted result only; no stdout/stderr capture; engine timeouts can't preempt blocked FFI (by design — the worker, P0-02, is the boundary). --- a/docs/security-reference.md +++ b/docs/security-reference.md @@ -50,7 +50,9 @@ Creates an evaluation environment containing only approved bindings. Uses Chez S `compile*`, and `open-*-file`; - evaluates escape attempts for process execution, `eval`, FFI, file output, `gensym`, `call/cc`, direct imports, and macro smuggling and requires all of - them to fail; + them to fail. The macro battery covers `syntax-rules` emitting `system`, + `eval`, and `foreign-procedure`, `datum->syntax` context-forging attempts, + and macro-defined macros; - 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 @@ -59,6 +61,17 @@ Creates an evaluation environment containing only approved bindings. Uses Chez S The current gate is a mechanical closure, documentation-contract, and escape test. It is not a formal reachability proof through Chez internals. +### Macro Allowlist Decision + +`define-syntax` and `syntax-rules` remain in `safe-bindings` for first-order +local macros. This is accepted because macro expansion still resolves emitted +identifiers against the restricted environment: dangerous targets such as +`system`, `eval`, `foreign-procedure`, `datum->syntax`, imports, and generated +macros are absent or rejected. `tools/check-restrict-closure.ss` and +`tests/security/test-k3-regressions.ss` lock these adversarial cases. Any future +addition to the macro/template surface must extend that battery in the same +change. + ### 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`. @@ -758,7 +771,6 @@ These are known gaps documented as current limitations, not implementation promi the capability API boundary. Code with raw Chez file primitives or unauthorized imports can bypass them unless the safe prelude, import-audit gate, and OS worker confinement are also in force. -- **`define-syntax` remains in the sandbox allowlist.** Macro definition in sandboxed code is possible. Whether this is a risk depends on the use case. - **Restricted-eval output is not captured.** `max-output-size` bounds only the formatted return value. It is not a stdout/stderr capture system. - **No Argon2id.** Password hashing uses PBKDF2 (via OpenSSL or Rust ring) rather than Argon2id (requires separate library). - **FFI audit (Phase 5 of parser hardening) is not started.** Null return checks, type validation, and SQL injection lint rules are unimplemented. --- a/docs/unsafe-deserialize-allowlist.sexp +++ b/docs/unsafe-deserialize-allowlist.sexp @@ -41,6 +41,6 @@ ("lsp/build-jlsp-cross.ss" 79 "runtime-load-trusted" "(load xpatch)" "cross-build helper loads configured local xpatch script") ("lsp/build-jlsp-freebsd-cross.ss" 78 "runtime-load-trusted" "(load xpatch)" "cross-build helper loads configured local xpatch script") ("mcp/test/security-test.ss" 13 "runtime-load-trusted" "(load (string-append repo-root \"/mcp/server.ss\"))" "test harness loads the repository-local MCP server under test") - ("tools/check-restrict-closure.ss" 121 "bare-read-untrusted" " [form (read port)]" "audit checker reads repository-controlled allowlist manifest from security-reference.md") - ("tools/check-restrict-closure.ss" 122 "bare-read-untrusted" " [extra (read port)])" "audit checker rejects trailing data in repository-controlled allowlist manifest") + ("tools/check-restrict-closure.ss" 125 "bare-read-untrusted" " [form (read port)]" "audit checker reads repository-controlled allowlist manifest from security-reference.md") + ("tools/check-restrict-closure.ss" 126 "bare-read-untrusted" " [extra (read port)])" "audit checker rejects trailing data in repository-controlled allowlist manifest") ) --- a/tests/security/test-k3-regressions.ss +++ b/tests/security/test-k3-regressions.ss @@ -202,6 +202,22 @@ (raises? (lambda () (restricted-eval-string "(begin (define-syntax go (syntax-rules () [(_) (system \"true\")])) (go))"))) => #t) +(check "K3-P1-04 restricted eval blocks macro-emitted eval" + (raises? (lambda () + (restricted-eval-string + "(begin (define-syntax go (syntax-rules () [(_) (eval '(+ 1 2))])) (go))"))) => #t) +(check "K3-P1-04 restricted eval blocks macro-emitted FFI" + (raises? (lambda () + (restricted-eval-string + "(begin (define-syntax go (syntax-rules () [(_) ((foreign-procedure \"exit\" (int) void) 0)])) (go))"))) => #t) +(check "K3-P1-04 restricted eval blocks datum->syntax context forging" + (raises? (lambda () + (restricted-eval-string + "(begin (define-syntax go (lambda (stx) (datum->syntax stx '(system \"true\")))) (go))"))) => #t) +(check "K3-P1-04 restricted eval blocks macro-defined macros" + (raises? (lambda () + (restricted-eval-string + "(begin (define-syntax outer (syntax-rules () [(_) (define-syntax inner (syntax-rules () [(_) (system \"true\")]))])) (outer) (inner))"))) => #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/tools/check-restrict-closure.ss +++ b/tools/check-restrict-closure.ss @@ -30,7 +30,11 @@ file-output "(open-output-file \"/tmp/jerboa-restrict-escape\")" callcc-call "(call/cc (lambda (k) (k 1)))" import-call "(import (chezscheme))" - macro-smuggle "(begin (define-syntax go (syntax-rules () [(_) (system \"id\")])) (go))")) + macro-smuggle-system "(begin (define-syntax go (syntax-rules () [(_) (system \"id\")])) (go))" ; jerboa-security: suppress non-constant-time-secret-compare -- quoted escape fixture, not a secret comparison + macro-smuggle-eval "(begin (define-syntax go (syntax-rules () [(_) (eval '(+ 1 2))])) (go))" + macro-smuggle-ffi "(begin (define-syntax go (syntax-rules () [(_) ((foreign-procedure \"exit\" (int) void) 0)])) (go))" + macro-datum-forge "(begin (define-syntax go (lambda (stx) (datum->syntax stx '(system \"id\")))) (go))" ; jerboa-security: suppress shell-injection-format-tilde-s -- quoted macro escape fixture, never passed to a shell + macro-defined-macro "(begin (define-syntax outer (syntax-rules () [(_) (define-syntax inner (syntax-rules () [(_) (system \"id\")]))])) (outer) (inner))")) ; jerboa-security: suppress shell-injection-format-tilde-s -- quoted macro escape fixture, never passed to a shell (define (add-error msg) (set! errors (cons msg errors))) (define (add-warning msg) (set! warnings (cons msg warnings)))