security: bind safe prelude taint sinks
Jaime Fournier <jaimef@linbsd.org>
f072895da314ebcf37161b92440f7d4b834a7c6c
--- a/docs/JERBOA-LANG.md +++ b/docs/JERBOA-LANG.md @@ -28,9 +28,10 @@ One import gives direct scripts the safe application language: ``` When a script is run through `jerboa run`, that import is resolved as the safe -prelude. Raw FFI, `system`, `eval`, and raw thread bindings require +prelude. Raw FFI, raw shell/process bindings, `eval`, and raw thread bindings require `jerboa run --unsafe-prelude hello.ss` or `(import (jerboa prelude unsafe))`; -both escape hatches print a warning. +both escape hatches print a warning. The safe prelude still exposes `system` +under the standard name, but it is the taint-checking safe wrapper. --- @@ -82,7 +83,7 @@ Key points: combinators, ergo typing, and safe wrappers for risky APIs - **Raw prelude is explicit**: use `--unsafe-prelude` or `(import (jerboa prelude unsafe))` when you intentionally need raw Chez - bindings such as FFI, `system`, `eval`, or raw threads + bindings such as FFI, raw shell/process operations, `eval`, or raw threads - For specialized modules not in the prelude, add extra imports --- --- a/docs/kimi3-security-recommmendations.md +++ b/docs/kimi3-security-recommmendations.md @@ -208,7 +208,7 @@ when" must be answerable from `dist/release-evidence/` in minutes. | In-process bounded eval (engine timeout, result cap, fails closed on process controls) | `(std security sandbox)` `run-safe-eval` | exists; no memory limit, no FFI preemption (documented) | security-reference §6 | | Capability tokens (sealed, CSPRNG nonce, monotone attenuation, revocation) | `(std security capability)` | exists; path checks reject symlink escapes and keep create-target compatibility | [security-reference.md](security-reference.md#3-capability-based-security) | | Typed capability declarations | `(std security capability-typed)` | exists | security-reference §3 | -| Taint tracking + safe sinks | `(std security taint)` | exists; opt-in only (limitation documented) | security-reference §4 | +| Taint tracking + safe sinks | `(std security taint)`, `(jerboa prelude safe)` | exists; safe prelude binds standard file/shell/delete sinks to taint-checking wrappers; source marking remains explicit | security-reference §4 | | Kernel FS confinement (Linux 5.13+, ABI v1–v3) | `(std security landlock)`, `(std os landlock-native)` | real syscalls | security-reference §5 | | Kernel syscall filter (BPF, x86_64 + aarch64 numbers) | `(std security seccomp)`, `(std os seccomp)` | real BPF | security-reference §5 | | macOS / FreeBSD confinement | `(std security seatbelt)`, `(std security capsicum)` | exist | lib listing | @@ -303,7 +303,7 @@ when" must be answerable from `dist/release-evidence/` in minutes. | Goal | Where we stand | The gap | |---|---|---| | G1 shrink target | Managed core is memory-safe; parsers budgeted; safe prelude exists | FFI surface (91 files / 225 symbols / 432 `unsafe`) never systematically audited (phase 5); `vendor/jsqlite` is C in the TCB; safe prelude not the default entry; import conflict undermines "safe symbol wins" confidence | -| G2 cap blast radius | Capabilities, taint, kernel sandbox, egress policy objects, worker facade, and authenticated actor transport/envelopes all exist | **No native pre-exec worker backend to install kernel controls before child input**; taint opt-in; TOCTOU on paths; no memory limit story; `define-syntax` in sandbox | +| G2 cap blast radius | Capabilities, taint, kernel sandbox, egress policy objects, worker facade, and authenticated actor transport/envelopes all exist | **No native pre-exec worker backend to install kernel controls before child input**; taint source marking/propagation still incomplete; no memory limit story; `define-syntax` in sandbox | | G3 find it first | 13 harnesses, scanner w/ rule DB, lint | No corpora, no crash regression, no scheduled fuzzing, no standing AI-red-team, no exploit-shaped regression suite | | G4 fail closed | Raw-fork launchers retired correctly; `allow-degraded?` explicit | New controls must keep the invariant; degraded-mode warnings must be test-locked | | G5 recover fast | SBOM/repro/signing gates exist | TCB accounting manual; doc drift (stale tables, undocumented modules); independent-builder reproducibility not yet routine | @@ -619,19 +619,22 @@ defeats the capability. Taint is opt-in; native sinks don't check it. In the safe prelude, the *default* file/shell/delete operations should be the taint-aware wrappers. -- **Do:** (a) In `(jerboa prelude safe)`, rebind `open-input-file`, - `open-output-file`, `delete-file`, and any process-spawn to the - `safe-*` taint-checking versions (with the raw versions available only - via explicit `(std unsafe)` import). (b) Taint sources by default: HTTP - request fields, env vars, file contents read in safe mode, network - frames — wrapped at the boundary. (c) Propagation coverage: extend the - tainted-string operation set (currently four functions) to the full +- **Status:** safe-prelude sink defaults complete for file/shell/delete names. + `(jerboa prelude safe)` now exports taint API helpers and binds + `open-input-file`, `open-output-file`, `call-with-input-file`, + `call-with-output-file`, `delete-file`, and `system` to taint-checking safe + wrappers. `tests/test-safe-prelude.ss` locks rejection of tainted values + through the script-loader default prelude. +- **Remaining:** (b) Taint sources by default: HTTP request fields, env vars, + file contents read in safe mode, network frames — wrapped at the boundary. + (c) Propagation coverage: extend the tainted-string operation set to the full common string/bytevector API so taint doesn't silently launder away. (d) Performance: measure; if overhead matters, document `*taint-enforce* #f` as an explicit, warned de-opt — never silent. -- **Accept:** tests: tainted value reaching a sink in safe-prelude code - raises `&taint-violation`; untainted flows unchanged; propagation tests - for each new operation; `safety-guide.md` gains a taint section. +- **Accept:** partially satisfied: tainted values reaching standard sink names + in safe-prelude code raise `&taint-violation`; untainted flows are covered by + existing safe-prelude tests; `safety-guide.md` has a taint section. Full + completion still requires source-default and broader propagation work. ### K3-P1-04 — Decide `define-syntax` in the sandbox allowlist **Serves:** G1. **Effort:** 2–3 days. --- a/docs/safety-guide.md +++ b/docs/safety-guide.md @@ -1,7 +1,7 @@ # Jerboa Safety Guide Practical guide for writing secure Jerboa applications. Covers all safety -features as of 2026-06-25. +features as of 2026-07-27. --- @@ -15,8 +15,8 @@ safe by default: ``` The script loader resolves that import as `(jerboa prelude safe)` and evaluates -the script in a base environment with raw FFI, `system`, `eval`, `fork-thread`, -`load`, and compiler entry points removed. Specifically, you get: +the script in a base environment with raw FFI, raw `system`, `eval`, +`fork-thread`, `load`, and compiler entry points removed. Specifically, you get: - **Contract-checked stdlib** — SQLite, TCP, file I/O, and JSON functions validate arguments before FFI calls and return structured error conditions @@ -25,6 +25,9 @@ the script in a base environment with raw FFI, `system`, `eval`, `fork-thread`, - **Timeouts** — `with-timeout` and a configurable `*default-timeout*` - **Safe serialization** — `safe-fasl-read`/`safe-fasl-write` use a bounded, non-executable pure-data format and reject native FASL/runtime objects +- **Taint-checked sinks** — `open-input-file`, `open-output-file`, + `call-with-input-file`, `call-with-output-file`, `delete-file`, and `system` + reject tainted paths or commands under their standard names - **Restricted evaluator** — `run-safe-eval` for bounded, allowlisted evaluation - **Exec worker facade** — `worker-run-eval` for running restricted eval in a fresh process with pure env, deadline, and output caps @@ -253,6 +256,28 @@ When you import `(jerboa prelude safe)`, the standard names (`sqlite-exec`, `tcp-connect`, etc.) are transparently replaced with contract-checked versions from `(std safe)`. +### Taint-Checked Sinks + +The safe prelude also exports the taint API from `(std security taint)` and +binds the default file and shell/delete sink names to taint-checking wrappers: +`open-input-file`, `open-output-file`, `call-with-input-file`, +`call-with-output-file`, `delete-file`, and `system`. + +```scheme +(import (jerboa prelude)) + +(define path (taint-file "/tmp/input")) + +(guard (exn + [(taint-violation? exn) 'blocked]) + (open-input-file path)) +``` + +Use `taint-http`, `taint-env`, `taint-file`, `taint-net`, and `taint-deser` at +input boundaries. Use `untaint` only at a reviewed sanitization boundary. Code +that imports raw Chez or unsafe modules bypasses these wrappers; keep +`(std security import-audit)` in the build gate for applications. + ### What the Contracts Check - **Type validation** before FFI calls — e.g., `sqlite-exec` verifies the --- a/docs/security-reference.md +++ b/docs/security-reference.md @@ -287,9 +287,18 @@ These automatically call `check-untainted!` and reject tainted arguments: - `safe-system` - `safe-delete-file` +`(jerboa prelude safe)` binds the standard sink names +`open-input-file`, `open-output-file`, `call-with-input-file`, +`call-with-output-file`, `delete-file`, and `system` to taint-checking safe +wrappers, and exports the core taint API so application code can mark input +boundaries without importing a separate module. + ### Taint-propagating string operations -`tainted-string-append`, `tainted-string-ref`, `tainted-substring`, `tainted-string-length` -- operations on tainted strings propagate the taint to results. +`tainted-string-append`, `tainted-string-ref`, `tainted-substring`, +`tainted-string-length`, `tainted-string-upcase`, `tainted-string-downcase`, +`tainted-string->number`, and `tainted-format` -- operations on tainted strings +propagate the taint to results where the result carries untrusted data. --- @@ -740,7 +749,10 @@ These are known gaps documented as current limitations, not implementation promi - **No Common Criteria evaluation.** No Protection Profile, Security Target, or EAL evaluation has been performed. - **Seccomp architecture coverage is limited.** The BPF bytecode generator supports x86_64 and aarch64 syscall numbers. - **Landlock requires Linux 5.13+.** No equivalent on macOS, BSDs, or older Linux kernels. `landlock-available?` returns `#f` on unsupported systems. -- **Taint tracking is opt-in.** Only the `safe-*` wrappers enforce taint checks. Native Chez operations (`open-input-file`, `system`, etc.) do not check taint. No static analysis enforcement exists. +- **Taint enforcement depends on the safe surface.** `(jerboa prelude safe)` + binds default file/shell/delete sink names to taint-checking wrappers, but raw + Chez operations and unsafe imports do not check taint. Boundary sources still + need explicit `taint-*` marking until protocol modules wrap inputs by default. - **Distributed actor authentication is opt-in at the serialization layer.** `(std actor transport)` authenticates TCP traffic, and `(std actor distributed)` exposes HMAC'd envelopes with timestamp and monotonic sequence replay checks. Compatibility callers that use only `serialize-message` / `deserialize-message` still get parsing limits but no peer authentication. - **Filesystem capabilities are not process sandboxes.** They validate paths at the capability API boundary. Code with raw Chez file primitives or --- a/lib/jerboa/prelude/safe.ss +++ b/lib/jerboa/prelude/safe.ss @@ -64,7 +64,7 @@ chain chain-and assert! ;; std/text/json — safe wrappers under standard names - read-json write-json json-object->string string->json-object + read-json write-json json-object->string string->json-object ; jerboa-security: suppress unguarded-string-to-json-on-hostile -- export list only; binding below points at safe JSON wrapper ;; std/os/path path-expand path-normalize path-directory path-strip-directory @@ -107,10 +107,23 @@ tcp-connect tcp-listen tcp-accept tcp-close tcp-read tcp-write tcp-write-string - ;; File I/O (safe wrappers, renamed to standard names) + ;; File I/O and shell/delete sinks (taint-checked safe wrappers) + open-input-file open-output-file + call-with-input-file call-with-output-file + delete-file system ; jerboa-security: suppress shell-interpolation-unquoted-into-sh -- export list only; system is rebound to taint:safe-system below open-safe-input-file open-safe-output-file call-with-safe-input-file call-with-safe-output-file + ;; Taint API for explicit boundary marking/sanitization + taint tainted? taint-class taint-value untaint + taint-http taint-env taint-file taint-net taint-deser + check-untainted! + tainted-string-append tainted-string-ref tainted-substring + tainted-string-length tainted-string-upcase tainted-string-downcase ; jerboa-security: suppress string-number-radix-prefix -- export list only; tainted-string->number preserves taint and is not used for protocol lengths + tainted-string->number tainted-format + make-taint-violation taint-violation? + taint-violation-class taint-violation-sink + ;; Resource management with-resource with-resource1 register-resource-cleanup! @@ -162,6 +175,9 @@ iota 1+ 1- partition make-date make-time + open-input-file open-output-file + call-with-input-file call-with-output-file + delete-file system atom? meta) (only (jerboa core) @@ -188,6 +204,7 @@ (std misc ports) ;; Safety modules (prefix (std safe) safe:) + (prefix (std security taint) taint:) (std resource) (std error conditions) (std safe-timeout) @@ -230,12 +247,45 @@ (def tcp-write safe:safe-tcp-write) (def tcp-write-string safe:safe-tcp-write-string) - ;; File I/O - (def open-safe-input-file safe:safe-open-input-file) - (def open-safe-output-file safe:safe-open-output-file) + ;; File I/O and shell/delete sinks. The standard names are safe in this + ;; prelude: paths/commands are taint-checked before reaching raw Chez sinks. + (def open-input-file safe:safe-open-input-file) + (def open-output-file safe:safe-open-output-file) + (def call-with-input-file safe:safe-call-with-input-file) + (def call-with-output-file safe:safe-call-with-output-file) + (def delete-file taint:safe-delete-file) + (def system taint:safe-system) + + (def open-safe-input-file safe:safe-open-input-file) + (def open-safe-output-file safe:safe-open-output-file) (def call-with-safe-input-file safe:safe-call-with-input-file) (def call-with-safe-output-file safe:safe-call-with-output-file) + ;; Taint boundary API + (def taint taint:taint) + (def tainted? taint:tainted?) + (def taint-class taint:taint-class) + (def taint-value taint:taint-value) + (def untaint taint:untaint) + (def taint-http taint:taint-http) + (def taint-env taint:taint-env) + (def taint-file taint:taint-file) + (def taint-net taint:taint-net) + (def taint-deser taint:taint-deser) + (def check-untainted! taint:check-untainted!) + (def tainted-string-append taint:tainted-string-append) + (def tainted-string-ref taint:tainted-string-ref) + (def tainted-substring taint:tainted-substring) + (def tainted-string-length taint:tainted-string-length) + (def tainted-string-upcase taint:tainted-string-upcase) + (def tainted-string-downcase taint:tainted-string-downcase) + (def tainted-string->number taint:tainted-string->number) + (def tainted-format taint:tainted-format) + (def make-taint-violation taint:make-taint-violation) + (def taint-violation? taint:taint-violation?) + (def taint-violation-class taint:taint-violation-class) + (def taint-violation-sink taint:taint-violation-sink) + ;; Mode control (def *safe-mode* safe:*safe-mode*) --- a/tests/test-safe-prelude.ss +++ b/tests/test-safe-prelude.ss @@ -36,7 +36,7 @@ (define (write-temp-script source) (let ([path (make-temporary-file-name "jerboa-safe-entry")]) - (call-with-output-file path + (call-with-output-file path ; jerboa-security: suppress call-with-output-file-overwrite-fail -- explicit 'replace mode for temporary test script fixture (lambda (port) (display source port)) 'replace) path)) @@ -52,7 +52,7 @@ (jerboa-load-script path unsafe-prelude?) '(ok)))]) (guard (exn [else (void)]) - (delete-file path)) + (delete-file path)) ; jerboa-security: suppress missing-taint-check-at-sink -- internal deletion of a freshly-created temporary test fixture (list status (get-output-string out) (get-output-string err))))) @@ -98,7 +98,7 @@ (test "unsafe-import: sqlite-native flagged" (let* ([linter (make-linter)] - [results (lint-string linter "(import (std db sqlite-native))")] + [results (lint-string linter "(import (std db sqlite-native))")] ; jerboa-security: suppress raw-ffi-module-import-without-safe -- quoted fixture for unsafe-import lint regression [rules (map lint-result-rule results)]) (if (memq 'unsafe-import rules) #t #f)) #t) @@ -140,7 +140,16 @@ (test "script loader rewrites default prelude to safe surface" (let ([result (run-script-loader - "(import (jerboa prelude))\n(define (blocked? thunk)\n (guard (exn [else #t])\n (thunk)\n #f))\n(write (list\n (blocked? (lambda () foreign-procedure))\n (blocked? (lambda () system))\n (blocked? (lambda () eval))\n (blocked? (lambda () fork-thread))))\n" + "(import (jerboa prelude))\n(define (blocked? thunk)\n (guard (exn [else #t])\n (thunk)\n #f))\n(write (list\n (blocked? (lambda () foreign-procedure))\n (blocked? (lambda () eval))\n (blocked? (lambda () fork-thread))\n (blocked? (lambda () (system (taint-env \"true\"))))))\n" + #f)]) + (and (loader-ok? result) + (equal? (cadr result) "(#t #t #t #t)"))) + #t) + +(test "safe prelude standard sink names reject tainted values" + (let ([result + (run-script-loader + "(import (jerboa prelude))\n(define (blocked? thunk)\n (guard (exn [else #t])\n (thunk)\n #f))\n(write (list\n (blocked? (lambda () (open-input-file (taint-file \"/tmp/missing\"))))\n (blocked? (lambda () (open-output-file (taint-file \"/tmp/jerboa-tainted\"))))\n (blocked? (lambda () (delete-file (taint-file \"/tmp/jerboa-tainted\"))))\n (blocked? (lambda () (system (taint-env \"true\"))))))\n" #f)]) (and (loader-ok? result) (equal? (cadr result) "(#t #t #t #t)"))) @@ -168,7 +177,7 @@ (test "script loader rejects direct chezscheme import in safe mode" (loader-error? - (run-script-loader "(import (chezscheme))\n(display \"bad\")\n" #f)) + (run-script-loader "(import (chezscheme))\n(display \"bad\")\n" #f)) ; jerboa-security: suppress direct-chezscheme-import-user-code -- quoted fixture for script-loader import rejection regression #t) ;; ========================================================================= @@ -285,7 +294,7 @@ (printf "~%-- SQL safety runtime checks --~%") (test "check-sql-safety!: clean SQL passes" - (guard (exn [#t #f]) + (guard (exn [#t #f]) ; jerboa-security: suppress catch-all-guard-masks-errors -- regression expects any wrapper failure to map to a false predicate result ;; Internal function, but we can test via the safe-sqlite wrappers. ;; Since sqlite may not be loaded, test the check indirectly: ;; A clean SQL string should not raise from the safety check itself.