security: taint safe-prelude env and file sources
Jaime Fournier <jaimef@linbsd.org>
a2d0e5598155be7bdcaf70932f998c8e236d0873
diff --git a/docs/kimi3-security-recommmendations.md b/docs/kimi3-security-recommmendations.md
index 161199d..0155dea 100644
--- a/docs/kimi3-security-recommmendations.md
+++ b/docs/kimi3-security-recommmendations.md
@@ -210,7 +210,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)`, `(jerboa prelude safe)` | exists; safe prelude binds standard file/shell/delete sinks to taint-checking wrappers; source marking remains explicit | 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 and taints env/file-content reads; protocol/network 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 |
@@ -645,16 +645,18 @@ Taint is opt-in; native sinks don't check it. In the safe prelude, the
wrappers. `tests/test-safe-prelude.ss` locks rejection of tainted values
through the script-loader default prelude. Explicit taint-propagating wrappers
now cover trim/split/join, UTF-8 string/bytevector conversion, bytevector
- copy, and bytevector element reads.
-- **Remaining:** (b) Taint sources by default: HTTP request fields, env vars,
- file contents read in safe mode, network frames — wrapped at the boundary.
- (c) Performance: measure; if overhead matters, document
+ copy, and bytevector element reads. Safe-prelude `getenv`,
+ `read-file-string`, and `read-file-lines` now taint present environment
+ variables and file contents by default.
+- **Remaining:** (b) Taint sources by default for HTTP request fields and
+ network frames — wrapped at the protocol boundary. (c) Performance: measure;
+ if overhead matters, document
`*taint-enforce* #f` as an explicit, warned de-opt — never silent.
- **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 work at protocol/file/env
- boundaries.
+ existing safe-prelude tests; env/file-content reads are tainted by default;
+ `safety-guide.md` has a taint section. Full completion still requires
+ source-default work at protocol/network boundaries.
### K3-P1-04 — Decide `define-syntax` in the sandbox allowlist
**Serves:** G1. **Effort:** 2–3 days.
@@ -1157,8 +1159,9 @@ 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).
-- Safe-prelude file/shell/delete sink names now check taint; source marking and
- broad propagation remain P1-03 follow-up.
+- Safe-prelude file/shell/delete sink names now check taint, and env/file
+ content reads are source-tainted by default; protocol/network source marking
+ and performance measurement 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.
diff --git a/docs/safety-guide.md b/docs/safety-guide.md
index 10555d7..51d128b 100644
--- a/docs/safety-guide.md
+++ b/docs/safety-guide.md
@@ -287,6 +287,13 @@ and `tainted-bytevector-*` wrappers so taint remains attached until the value is
sanitized. Code that imports raw Chez or unsafe modules bypasses these wrappers;
keep `(std security import-audit)` in the build gate for applications.
+In `(jerboa prelude safe)`, `getenv`, `read-file-string`, and
+`read-file-lines` are already source wrappers: present environment variables
+are tagged as `env-input`, file contents are tagged as `file-input`, and
+missing environment-variable defaults are returned unchanged. Protocol and
+network modules still need explicit source marking unless their API documents a
+tainted-by-default boundary.
+
### What the Contracts Check
- **Type validation** before FFI calls — e.g., SQLite wrappers verify the
diff --git a/docs/security-reference.md b/docs/security-reference.md
index 15dbb99..9cd11a5 100644
--- a/docs/security-reference.md
+++ b/docs/security-reference.md
@@ -354,6 +354,11 @@ These automatically call `check-untainted!` and reject tainted arguments:
wrappers, and exports the core taint API so application code can mark input
boundaries without importing a separate module.
+The safe prelude also treats environment and file contents as taint sources:
+`getenv` returns `env-input` taint for present variables, `read-file-string`
+returns `file-input` taint, and `read-file-lines` taints each returned line.
+Missing environment-variable defaults are returned unchanged.
+
### Taint-propagating string operations
`tainted-string-append`, `tainted-string-ref`, `tainted-substring`,
@@ -909,10 +914,11 @@ These are known gaps documented as current limitations, not implementation promi
- **Landlock requires Linux 5.13+.** No equivalent on macOS, BSDs, or older Linux kernels. `landlock-available?` returns `#f` on unsupported systems.
- **Taint enforcement depends on the safe surface.** `(jerboa prelude safe)`
binds default file/shell/delete sink names to taint-checking wrappers and
- exports taint-propagating wrappers for common string/bytevector transforms,
- 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.
+ exports taint-propagating wrappers for common string/bytevector transforms.
+ Safe-prelude `getenv`, `read-file-string`, and `read-file-lines` mark
+ environment and file contents by default, but raw Chez operations and unsafe
+ imports do not check taint. Protocol and network sources still need explicit
+ `taint-*` marking until those 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
diff --git a/lib/jerboa/prelude/safe.ss b/lib/jerboa/prelude/safe.ss
index aa925c9..342e9c0 100644
--- a/lib/jerboa/prelude/safe.ss
+++ b/lib/jerboa/prelude/safe.ss
@@ -97,6 +97,9 @@
write-file-string
with-input-from-string with-output-to-string
+ ;; Safe source wrappers
+ getenv
+
;; ---- Safe APIs under STANDARD names ----
;; SQLite (literal-SQL macros over safe parameterized wrappers)
@@ -179,9 +182,10 @@
make-date make-time
open-input-file open-output-file
call-with-input-file call-with-output-file
- delete-file system
+ delete-file system getenv
atom?
meta)
+ (rename (only (chezscheme) getenv) (getenv raw-getenv))
(only (jerboa core)
def def* defrule defrules
defstruct defclass defmethod
@@ -203,7 +207,7 @@
(std misc string)
(std misc list)
(std misc alist)
- (std misc ports)
+ (except (std misc ports) read-file-string read-file-lines)
;; Safety modules
(prefix (std safe) safe:)
(prefix (std security taint) taint:)
@@ -306,6 +310,23 @@
(def call-with-safe-input-file safe:safe-call-with-input-file)
(def call-with-safe-output-file safe:safe-call-with-output-file)
+ (def getenv
+ (case-lambda
+ [(name)
+ (let ([value (raw-getenv name)])
+ (if value (taint:taint-env value) value))]
+ [(name default)
+ (let ([value (raw-getenv name)])
+ (if value (taint:taint-env value) default))]))
+
+ (def (read-file-string path)
+ (taint:taint-file
+ (call-with-safe-input-file path read-all-as-string)))
+
+ (def (read-file-lines path)
+ (map taint:taint-file
+ (call-with-safe-input-file path read-all-as-lines)))
+
;; Taint boundary API
(def taint taint:taint)
(def tainted? taint:tainted?)
diff --git a/tests/test-safe-prelude.ss b/tests/test-safe-prelude.ss
index 763e7fc..608311a 100644
--- a/tests/test-safe-prelude.ss
+++ b/tests/test-safe-prelude.ss
@@ -164,6 +164,28 @@
(equal? (cadr result) "(#t #t #t 97)")))
#t)
+(test "safe prelude taints env and file source reads"
+ (let ([path "/tmp/jerboa-safe-prelude-taint-source.txt"])
+ (when (file-exists? path)
+ (delete-file path)) ; jerboa-security: suppress missing-taint-check-at-sink -- test cleanup before creating fixture path
+ (call-with-port
+ (open-file-output-port path
+ (file-options no-fail)
+ (buffer-mode block)
+ (native-transcoder))
+ (lambda (out) (display "line1\nline2\n" out)))
+ (putenv "JERBOA_SAFE_PRELUDE_TAINT_SOURCE" "env-value")
+ (let ([result
+ (run-script-loader
+ "(import (jerboa prelude))\n(define fs (read-file-string \"/tmp/jerboa-safe-prelude-taint-source.txt\"))\n(define ls (read-file-lines \"/tmp/jerboa-safe-prelude-taint-source.txt\"))\n(define ev (getenv \"JERBOA_SAFE_PRELUDE_TAINT_SOURCE\" \"fallback\"))\n(define miss (getenv \"JERBOA_SAFE_PRELUDE_TAINT_MISSING\" \"fallback\"))\n(write (list (tainted? fs) (taint-class fs) (tainted? (car ls)) (taint-class (car ls)) (tainted? ev) (taint-class ev) miss (tainted? miss)))\n"
+ #f)])
+ (when (file-exists? path)
+ (delete-file path)) ; jerboa-security: suppress missing-taint-check-at-sink -- test cleanup of fixture path
+ (and (loader-ok? result)
+ (equal? (cadr result)
+ "(#t file-input #t file-input #t env-input \"fallback\" #f)"))))
+ #t)
+
(test "script loader unsafe flag preserves raw prelude and warns"
(let ([result
(run-script-loader