Mark V1-V3 as FIXED in security.md, add test-security Makefile target
ober
3fdfeb460a9b337f21fee3c8d1c46732cbb9e310
--- a/Makefile +++ b/Makefile @@ -7,7 +7,7 @@ CHEZ_EXT_LIBDIRS = $(CHEZ_EXT_DIR)/chez-https/src:$(CHEZ_EXT_DIR)/chez-ssl/src:$ # Shared object paths for FFI-based chez-* libraries CHEZ_EXT_LDPATH = $(CHEZ_EXT_DIR)/chez-ssl:$(CHEZ_EXT_DIR)/chez-zlib:$(CHEZ_EXT_DIR)/chez-pcre2:$(CHEZ_EXT_DIR)/chez-leveldb:$(CHEZ_EXT_DIR)/chez-epoll:$(CHEZ_EXT_DIR)/chez-inotify:$(CHEZ_EXT_DIR)/chez-crypto:$(CHEZ_EXT_DIR)/chez-sqlite:$(CHEZ_EXT_DIR)/chez-postgresql -.PHONY: test test-reader test-core test-runtime test-stdlib test-ffi test-modules test-expanded test-features test-wrappers test-phase4a test-phase4b test-phase4c test-phase4d test-phase4e test-phase4f test-phase5 test-phase5e test-phase6 test-phase7 test-phase8 test-functional test-repl clean +.PHONY: test test-reader test-core test-runtime test-stdlib test-ffi test-modules test-expanded test-features test-wrappers test-phase4a test-phase4b test-phase4c test-phase4d test-phase4e test-phase4f test-phase5 test-phase5e test-phase6 test-phase7 test-phase8 test-functional test-repl test-security clean test: test-reader test-core test-runtime test-stdlib test-ffi test-modules test-expanded @@ -242,7 +242,14 @@ test-functional: @gcc -shared -fPIC -O2 -o support/libjerboa-landlock.so support/landlock-shim.c 2>/dev/null || true @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-functional.ss -test-all: test test-features test-wrappers +test-security: + @echo "--- Security tests ---" + @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-crypto-random.ss + @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-crypto-compare.ss + @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-crypto-digest.ss + @$(SCHEME) --libdirs $(LIBDIRS) --script tests/test-security-capability.ss + +test-all: test test-features test-wrappers test-security clean: find lib -name "*.so" -delete 2>/dev/null || true new file mode 100644 --- /dev/null +++ b/docs/security.md @@ -0,0 +1,1348 @@ +# Jerboa Security Architecture + +A comprehensive security framework for building critical applications on Jerboa/Chez Scheme. This document catalogs every security-relevant feature already implemented, identifies vulnerabilities to fix, and proposes advanced features that would make Jerboa a uniquely secure platform for high-assurance software. + +--- + +## Table of Contents + +1. [Design Principles](#design-principles) +2. [Security Features Already Implemented](#security-features-already-implemented) +3. [Known Vulnerabilities to Fix](#known-vulnerabilities-to-fix) +4. [Proposed: Language-Level Safety](#proposed-language-level-safety) +5. [Proposed: Cryptographic Foundation](#proposed-cryptographic-foundation) +6. [Proposed: Network and Protocol Hardening](#proposed-network-and-protocol-hardening) +7. [Proposed: Operating System Integration](#proposed-operating-system-integration) +8. [Proposed: Supply Chain and Build Security](#proposed-supply-chain-and-build-security) +9. [Proposed: Observability and Incident Response](#proposed-observability-and-incident-response) +10. [Proposed: Distributed Systems Security](#proposed-distributed-systems-security) +11. [Implementation Roadmap](#implementation-roadmap) +12. [Architectural Position](#architectural-position) + +--- + +## Design Principles + +Every security decision in Jerboa should follow these principles: + +1. **Default deny** — nothing is permitted unless explicitly granted. Allowlists over blocklists, everywhere. +2. **Defense in depth** — language-level types + runtime contracts + OS-level sandboxing + network-level controls. No single layer is trusted alone. +3. **Least privilege** — every component receives the minimum capabilities it needs. Capabilities attenuate monotonically; they never escalate. +4. **Fail secure** — errors result in denial, not bypass. A crashed capability check denies access. +5. **Audit everything** — every security-relevant decision produces a structured, immutable log entry. +6. **Assume breach** — design for containment. Compromised components cannot escalate to the rest of the system. +7. **Constant-time for secrets** — no timing side channels in any comparison involving secret material. +8. **Minimal attack surface** — fewer dependencies, smaller trusted computing base, less code to audit. +9. **Verify, don't trust** — never rely on caller-supplied metadata. Validate at every boundary. +10. **Make the safe path the easy path** — unsafe operations should require explicit opt-in; safe defaults should require no annotation. + +--- + +## Security Features Already Implemented + +Jerboa has a remarkably deep set of security-relevant features for a project of its age. This section catalogs every existing feature and how it contributes to security. + +### Capability-Based Access Control — `(std security capability)` + +An object-capability system where access rights are represented as unforgeable tokens rather than identity-based ACLs. + +| Feature | Description | +|---------|-------------| +| **Four capability domains** | Filesystem (read/write/execute + path restrictions), Network (connect/listen + host restrictions), Process (spawn/signal), Environment (read/write) | +| **Unforgeable tokens** | Each capability carries a unique nonce | +| **Monotonic attenuation** | `attenuate-capability` can only restrict permissions, never add them | +| **Scoped contexts** | `with-capabilities` enforces that child contexts are subsets of parent contexts | +| **Violation conditions** | `&capability-violation` with structured type and detail fields | +| **Thread-safe** | Nonce generation is mutex-protected; capability context is a thread parameter | + +**Security value**: Prevents confused deputy attacks. Code that receives a read-only filesystem capability cannot escalate to write access, even if it passes through untrusted intermediaries. + +### Restricted Evaluation Sandbox — `(std security restrict)` + +Evaluates untrusted code in an environment with only 29 safe bindings. + +| Feature | Description | +|---------|-------------| +| **Explicit safe set** | Arithmetic, lists, strings, vectors, bytevectors, symbols, string ports, error handling | +| **Blocked categories** | FFI, file I/O, process execution, code loading, environment access, thread creation, module system manipulation | +| **Extra bindings** | Callers can inject additional bindings into the sandbox | +| **String evaluation** | `restricted-eval-string` for evaluating user-provided source text | + +**Security value**: Enables safe execution of user-submitted code (configuration DSLs, rule engines, plugin systems). + +### Embeddable Sandbox — `(jerboa embed)` + +A higher-level sandboxing API with configuration, error translation, and lifecycle management. + +| Feature | Description | +|---------|-------------| +| **Configuration record** | `max-eval-time`, `allowed-imports`, `capture-output` | +| **Error isolation** | Exceptions from sandboxed code are translated to `sandbox-error` records — internal details don't leak | +| **State management** | `sandbox-reset!` creates a fresh environment; `sandbox-define!` injects bindings | +| **Scoped API** | `with-sandbox` macro for deterministic lifecycle | + +**Security value**: Production-ready embedding of untrusted code with structured error boundaries. + +### Gradual Type System — `(std typed)` + +Runtime type checking with zero-overhead release mode. + +| Feature | Description | +|---------|-------------| +| **Annotated forms** | `define/t`, `lambda/t` with parameter and return type annotations | +| **Mode switching** | `*typed-mode*` parameter: `'debug` (checks enabled), `'release` (checks stripped), `'none` (no effect) | +| **Composite types** | `(listof T)`, `(vectorof T)`, `(hashof K V)`, `(-> A ... B)` | +| **Operator specialization** | `with-fixnum-ops`, `with-flonum-ops` replace generic arithmetic with safe fixed-width variants | +| **Custom predicates** | `register-type-predicate!` for user-defined types | + +**Security value**: Catches type confusion bugs at function boundaries. Fixnum specialization prevents integer overflow from silently promoting to bignum (relevant for buffer size calculations, array indices). + +### Linear Types — `(std typed linear)` + +Use-exactly-once discipline for resources that must be consumed. + +| Feature | Description | +|---------|-------------| +| **Consumption tracking** | `linear-use` marks a value as consumed; second use raises an error | +| **Scope enforcement** | `with-linear` checks that all linear values are consumed before scope exit | +| **Splitting** | `linear-split` creates N independent copies (for fork/join patterns) | +| **Read-only peek** | `linear-value` for inspection without consumption | + +**Security value**: Guarantees that resources (file handles, network connections, cryptographic keys) are used exactly once and cannot be leaked or double-freed. + +### Affine Types — `(std typed affine)` + +Use-at-most-once discipline with automatic cleanup. + +| Feature | Description | +|---------|-------------| +| **Guardian-based cleanup** | `make-affine/cleanup` registers a destructor that runs when the value is dropped | +| **Explicit drop** | `affine-drop!` runs the cleanup immediately | +| **Scope enforcement** | `with-affine` auto-drops on scope exit | +| **Peek without consumption** | `affine-peek` for read-only access | + +**Security value**: Prevents double-free bugs. Guarantees that secrets (keys, tokens) are wiped when they leave scope. Guardian integration means cleanup happens even if the programmer forgets. + +### Refinement Types — `(std typed refine)` + +Values that satisfy both a base type and an additional predicate. + +| Feature | Description | +|---------|-------------| +| **Built-in refinements** | `NonNeg`, `Positive`, `NonNull`, `NonEmpty`, `Bounded`, `NonZero`, `Natural` | +| **Annotated forms** | `define/r`, `lambda/r` inject runtime checks on function entry | +| **Flow-sensitive narrowing** | `refine-branch` and `with-refinement-context` avoid redundant checks after conditional tests | + +**Security value**: Enforces invariants like "port number is 1-65535", "buffer size is non-negative", "user ID is non-null" at every function boundary. Flow-sensitive narrowing means proven refinements are not re-checked. + +### Phantom Types — `(std typed phantom)` + +State machine invariant enforcement via type-level protocol tracking. + +| Feature | Description | +|---------|-------------| +| **Protocol registry** | Declares valid state transitions for a type | +| **State checking** | `phantom-check` asserts current state; `phantom-transition` enforces valid transitions | + +**Security value**: Encodes security protocols as types. A TLS connection in state `'handshake` cannot be used for data transfer until it transitions to `'established`. File in state `'closed` cannot be read. + +### GADTs — `(std typed gadt)` + +Type-indexed algebraic data types with safe pattern matching. + +| Feature | Description | +|---------|-------------| +| **Tagged constructors** | Each variant carries its constructor tag and fields | +| **Exhaustive matching** | `gadt-match` with catch-all `else` clause | + +**Security value**: Prevents illegal state representations. A well-typed security token can only be constructed through authorized constructors. + +### Contract System — `(std contract)` + +Design-by-contract with pre/post conditions. + +| Feature | Description | +|---------|-------------| +| **define/contract** | Functions with `(pre: ...)` and `(post: ...)` clauses | +| **Higher-order contracts** | `(-> pred ... pred)` wraps a function with argument and return checking | +| **Violation conditions** | `&contract-violation` with `who` and `message` fields | +| **Inline assertion** | `assert-contract` for ad-hoc checks | + +**Security value**: Enforces API invariants at function boundaries. Combined with refinement types, provides defense-in-depth validation. + +### Effect System — `(std effect)` and `(std typed effects)` + +Algebraic effects with handler-based control flow and effect type annotations. + +| Feature | Description | +|---------|-------------| +| **Effect handlers** | `with-handler` installs handlers for effect operations | +| **Resource effects** | `with-resources` / `acquire` for RAII-style cleanup with guaranteed destructor execution | +| **Scoped effects** | Koka-style scoped handlers with state, reader, and collection patterns | +| **Effect typing** | `define/te`, `lambda/te` annotate functions with their effect sets; `Pure T` marks effect-free code | +| **Effect inference** | `infer-effects` heuristically identifies effectful operations | +| **Effect discharge** | `check-effects!` validates all effects are handled | + +**Security value**: Makes side effects explicit and trackable. Pure code cannot perform I/O, access the filesystem, or modify global state. Effect handlers can intercept and audit all I/O operations. + +### Concurrency Safety — `(std concur)` + +Three layers of thread-safety enforcement. + +| Feature | Description | +|---------|-------------| +| **Thread-safety annotations** | `defstruct/immutable`, `defstruct/thread-local`, `defstruct/thread-safe` classify data structures | +| **Deadlock detection** | `make-tracked-mutex` with lock-order graph; BFS cycle detection prevents deadlock | +| **Resource leak detection** | `register-resource!` / `check-resource-leaks!` tracks per-thread resource ownership | +| **Lock order violations** | Recorded and queryable via `lock-order-violations` | + +**Security value**: Deadlock is a denial-of-service vector. Lock-order tracking catches potential deadlocks before they occur in production. Resource leak detection prevents file descriptor exhaustion. + +### Structured Concurrency — `(std control structured)` + +Guaranteed task lifecycle management. + +| Feature | Description | +|---------|-------------| +| **Task scopes** | `with-task-scope` guarantees all spawned tasks are cancelled on scope exit | +| **Parallel composition** | `parallel` spawns all, awaits all, collects results | +| **Race composition** | `race` spawns all, first to complete wins, cancels others | +| **Named tasks** | `scope-spawn-named` for debugging and monitoring | + +**Security value**: Prevents thread leaks and zombie tasks. Every spawned task has a defined lifetime and cleanup path. + +### Software Transactional Memory — `(std ds stm)` / `(std stm)` + +Lock-free concurrent data access. + +| Feature | Description | +|---------|-------------| +| **Transactional variables** | `make-tvar` with optimistic concurrency | +| **Atomic blocks** | `atomically` with automatic retry on conflict | +| **Composable retry** | `retry` and `or-else` for conditional blocking | +| **Snapshot isolation** | Read-set validation at commit prevents torn reads | + +**Security value**: Eliminates data races without locks. No deadlock possible. Atomic blocks are composable (unlike mutexes). + +### Rate Limiting — `(std net rate)` + +Three rate limiting algorithms, all thread-safe. + +| Feature | Description | +|---------|-------------| +| **Token bucket** | Smooth rate limiting with burst capacity | +| **Sliding window** | Precise per-window request counting | +| **Fixed window** | Efficient coarse-grained limiting | +| **Thread-safe wrapper** | `make-rate-limiter` with mutex-protected access | + +**Security value**: Prevents brute-force attacks, credential stuffing, and DoS via request flooding. + +### Schema Validation — `(std schema)` + +Structural data validation with composable validators. + +| Feature | Description | +|---------|-------------| +| **Type schemas** | `s:string`, `s:integer`, `s:number`, `s:boolean`, `s:null`, `s:any` | +| **Composite schemas** | `s:list`, `s:hash`, `s:union`, `s:enum`, `s:optional`, `s:required` | +| **Constraints** | `s:pattern`, `s:min-length`, `s:max-length`, `s:min`, `s:max` | +| **Structured errors** | `validation-error` records with path, message, and value | + +**Security value**: Validates untrusted input (API payloads, configuration files) against declared schemas before processing. + +### Connection Pooling — `(std net pool)` + +Thread-safe connection lifecycle management. + +| Feature | Description | +|---------|-------------| +| **Bounded pools** | Min/max size constraints with blocking acquire | +| **Health checking** | Periodic validation of idle connections | +| **Statistics** | Acquired, released, created, destroyed, wait counts | +| **Deterministic cleanup** | `with-connection` uses `dynamic-wind` for guaranteed release | + +**Security value**: Prevents connection leaks and resource exhaustion. Health checks detect stale/poisoned connections. + +### Thread-Safe Channels — `(std misc channel)` + +Production-quality inter-thread communication. + +| Feature | Description | +|---------|-------------| +| **Ring buffer** | Vector-based circular queue with dynamic growth | +| **Bounded/unbounded** | Backpressure via bounded channels that block on full | +| **Select** | Multiplexing across multiple channels with timeout | +| **GC-aware** | Consumed slots zeroed to help garbage collector | + +**Security value**: Bounded channels prevent memory exhaustion from producer flooding. + +### Static Analysis — `(std lint)` + +9-rule linter for code quality. + +| Feature | Description | +|---------|-------------| +| **Rules** | Empty begin, single-arm cond, missing else, deep nesting, long lambda, builtin redefinition, magic numbers, shadowed define, unused define | +| **Configurable** | Add/remove rules, set severity levels | + +**Security value**: Catches code quality issues that correlate with security bugs (shadowed variables, missing error branches). + +### Configuration with Schema Validation — `(std config)` + +Typed configuration management. + +| Feature | Description | +|---------|-------------| +| **Schema validation** | Type checking on config values (integer, string, boolean, list, symbol) | +| **Environment overrides** | `JERBOA_*` environment variables override config keys | +| **Change watchers** | Callbacks on config modification | +| **Nested access** | Dot-path navigation into config hierarchies | + +### Additional Security-Relevant Features + +| Module | Feature | Security Value | +|--------|---------|---------------| +| `(std assert)` | `assert!`, `assert-equal!`, `assert-pred`, `assert-exception` | Runtime invariant enforcement | +| `(std error)` | `Error`, `ContractViolation` condition types | Structured error classification | +| `(std debug replay)` | Record/replay execution | Deterministic reproduction of security incidents | +| `(std debug timetravel)` | Time-travel debugger with thread-safe event recording | Post-mortem analysis of security events | +| `(std pipeline)` | Data pipeline with timeout stages | Prevents unbounded computation in data processing | +| `(std rewrite)` | Term rewriting with fixed-point normalization | Formal transformation of security policies | +| `(std actor supervisor)` | OTP-style supervision with restart rate limiting | Fault tolerance; prevents restart-loop DoS | +| `(std build reproducible)` | Content-addressed artifact store with build records | Verifiable builds | +| `(jerboa lock)` | Lockfile with hash verification and diff | Dependency integrity tracking | +| `(std net tcp)` | GC-safe non-blocking I/O | Prevents thread starvation during stop-the-world GC | +| `(std foreign)` | `with-foreign-resource` deterministic cleanup, guardian thread | FFI resource safety | + +--- + +## Known Vulnerabilities to Fix + +### V1. Command Injection in Digest — ~~CRITICAL~~ FIXED + +**File**: `lib/std/crypto/digest.sls` + +**Status**: FIXED in commit `069d425` on `hardened` branch. + +**What was fixed**: +- Replaced temp file approach with stdin piping via `open-process-ports` +- No user input appears in the command string — only hardcoded algorithm names from a `case` expression +- No temp files created (eliminates TOCTOU race, predictable filenames, cleanup issues) +- 17 tests verify correct hashes against NIST vectors, bytevector input, and no temp file creation + +### V2. Forgeable Capabilities — ~~CRITICAL~~ FIXED + +**Affected files**: +- `lib/std/security/capability.sls` — `(std security capability)` +- `lib/std/capability.sls` — `(std capability)` + +**Status**: FIXED in commit `e4343d6` on `hardened` branch. + +**What was fixed**: +- Both modules now use sealed, opaque `define-record-type` with constructor NOT exported +- `(std security capability)` uses `(nongenerative std-security-capability)` +- `(std capability)` uses `(nongenerative std-capability)` — distinct types, cross-module forgery impossible +- `capability?` predicate uses the record type descriptor, which cannot be forged +- Vectors, strings, numbers, and all other types correctly rejected by `capability?` +- 66 tests verify forgery prevention, cross-module isolation, attenuation, and capability contexts + +### V3. Predictable Nonces — ~~CRITICAL~~ FIXED + +**Affected files**: +- `lib/std/security/capability.sls` +- `lib/std/capability.sls` + +**Status**: FIXED in commits `42b9fa2` (CSPRNG module) and `e4343d6` (capability hardening) on `hardened` branch. + +**What was fixed**: +- New `(std crypto random)` module reads from `/dev/urandom` via binary port with `dynamic-wind` cleanup +- Both capability modules now use `(random-bytes 16)` — 128 bits of cryptographic randomness per capability +- Revocation table in `(std capability)` uses `equal-hash`/`equal?` hashtable for bytevector nonce keys +- 23 tests verify CSPRNG correctness (length, non-determinism, UUID format, hex encoding) + +### V4. Sandbox Escape Vectors — HIGH + +**File**: `lib/std/security/restrict.sls` + +The sandbox copies the full `scheme-environment` and then blocks dangerous bindings. This is a blocklist — inherently incomplete. + +**Escape vectors**: +- `syntax-case` / `syntax-rules` can construct code that references blocked bindings indirectly +- `record-type-descriptor` access could reach runtime internals +- Any binding added in a future Chez version is automatically available +- `call/cc` (in safe list) can capture continuations that escape dynamic scope + +**Fix**: Create a bare `(environment)` and add only the 29 safe bindings. Nothing else exists. This is defense-in-depth: even if a safe binding is accidentally dangerous, the attack surface is bounded. + +### V5. Weak Distributed Actor Authentication — HIGH + +**File**: `lib/std/actor/transport.sls` + +```scheme +;; Authentication uses FNV-1a hash — NOT cryptographically secure +;; Comment in code: "Replace with HMAC-SHA256 via (std crypto hmac) for production" +``` + +**Issues**: +- FNV-1a is a non-cryptographic hash — trivially forgeable +- No TLS — all messages in plaintext over TCP +- No replay protection — captured handshakes can be replayed indefinitely +- No nonce in handshake — same cookie always produces same hash + +**Fix**: HMAC-SHA256 authentication with random nonce per connection. Mandatory TLS for all inter-node communication. Add timestamp + sequence number for replay protection. + +### V6. Shell Injection in Process Execution — HIGH + +**File**: `lib/std/misc/process.sls` + +```scheme +(define (build-command-string args) + ;; shell-quote attempts to escape, but relies on single-quote wrapping + ...) +``` + +**Issues**: +- `run-process` passes through shell — any metacharacter not in the escape set is dangerous +- `directory:` keyword is shell-interpolated — untrusted values exploitable +- Environment variables inherited by child process may contain secrets + +**Fix**: Add `run-process/exec` that uses `execvp` via FFI with an argv array — no shell involved. Make it the default. Keep `run-process/shell` as an explicit opt-in for cases that genuinely need shell features. + +### V7. Environment Variable Injection in Config — MEDIUM + +**File**: `lib/std/config.sls` + +```scheme +;; env-override! reads /proc/self/environ and overrides ANY config key +;; matching JERBOA_* prefix — no validation, no whitelist +``` + +**Fix**: Add an `env-overridable` list to the schema that explicitly declares which keys can be overridden from environment. Default: empty (no overrides). + +### V8. WebSocket Handshake Stub — MEDIUM + +**File**: `lib/std/net/websocket.sls` + +The handshake implementation returns a hardcoded test vector instead of computing `SHA-1(key + GUID)`. Not production-ready. + +**Fix**: Implement the SHA-1 computation (via `(std crypto digest)` once V1 is fixed) and proper Base64 encoding. + +### V9. Logger Information Leakage — MEDIUM + +**File**: `lib/std/logger.sls` + +- No structured logging — format strings can leak sensitive data +- No log levels enforced at compile time +- No rate limiting on log output (DoS via log flooding) +- `deflogger` is a no-op stub + +**Fix**: Add structured logging with mandatory field classification (public/internal/secret). Secret-classified fields are redacted in non-debug output. + +### V10. Unbounded Actor Mailboxes — MEDIUM + +**File**: `lib/std/actor/core.sls` + +Mailboxes have no size limit. A malicious or buggy sender can exhaust memory by flooding an actor with messages. + +**Fix**: Add configurable mailbox capacity with backpressure (sender blocks or message dropped with audit log entry). + +--- + +## Proposed: Language-Level Safety + +These features leverage Chez Scheme's macro system and Jerboa's existing type infrastructure to provide safety guarantees that most languages cannot express. + +### L1. Taint Tracking + +A compile-time/runtime system that marks data from untrusted sources and prevents it from reaching dangerous sinks without explicit sanitization. + +```scheme +;; Mark data as tainted +(define/tainted user-input (request-param req "name")) + +;; Type error: tainted string cannot flow to SQL sink +(sql-query db (format "SELECT * FROM users WHERE name = '~a'" user-input)) + +;; Safe: explicit sanitization produces clean value +(sql-query db "SELECT * FROM users WHERE name = ?" (sanitize-sql user-input)) +``` + +**Implementation**: Wrap tainted values in an opaque record type. Overload string operations to propagate taint. SQL/shell/filesystem functions check for taint and raise `&taint-violation`. Sanitization functions unwrap the taint after validation. + +**Taint categories**: +| Source | Taint Class | Required Sanitizer | +|--------|------------|-------------------| +| HTTP request params | `'http-input` | `sanitize-sql`, `sanitize-html`, `sanitize-path` | +| Environment variables | `'env-input` | `validate-config-value` | +| File contents | `'file-input` | `validate-schema` | +| Network data | `'net-input` | `sanitize-protocol` | +| Deserialized data | `'deser-input` | `validate-schema` | + +### L2. Information Flow Control + +Extend the type system with security labels that prevent secret data from flowing to public outputs. + +```scheme +;; Declare security levels +(define-security-level 'public) +(define-security-level 'internal) +(define-security-level 'secret) +(define-security-level 'top-secret) + +;; Annotate values +(define/classified api-key 'secret (getenv "API_KEY")) +(define/classified user-name 'public (request-param req "name")) + +;; Type error: secret cannot flow to public output +(log-info "Processing request for ~a with key ~a" user-name api-key) + +;; Safe: explicit declassification with audit trail +(log-info "Processing request for ~a with key ~a" + user-name (declassify api-key 'audit-reason "logging request context")) +``` + +**Implementation**: Security labels form a lattice. Data can flow up (public -> secret) but not down (secret -> public) without explicit `declassify` which logs an audit entry. Leverages Jerboa's effect system to track information flow through effect handlers. + +### L3. Capability-Typed Functions + +Combine the capability system with the type system so functions declare their required capabilities in their type signature. + +```scheme +;; This function requires filesystem read capability +(define/cap (read-config path) + (requires: (fs-read)) + (call-with-input-file path read)) + +;; This function requires no capabilities (pure) +(define/cap (parse-config sexp) + (requires: ()) + (validate-schema config-schema sexp)) + +;; Calling read-config outside a capability context is a type error +(with-capabilities + (list (make-fs-capability read: #t paths: '("/etc/myapp/"))) + (lambda () (read-config "/etc/myapp/config.scm"))) ;; OK + +(read-config "/etc/passwd") ;; ERROR: no fs-read capability in context +``` + +**Implementation**: `define/cap` expands to a function that calls `check-capability!` before executing the body. The `(requires: ...)` clause is also available to static analysis tools and documentation generators. + +### L4. Safe Arithmetic + +Extend `with-fixnum-ops` to provide overflow-checked arithmetic that raises an exception instead of silently wrapping or promoting to bignum. + +```scheme +;; Checked arithmetic: raises on overflow +(with-checked-fixnum-ops + (let ([size (fx+ header-length payload-length)]) ;; raises if overflow + (make-bytevector size))) + +;; Saturating arithmetic: clamps to fixnum range +(with-saturating-fixnum-ops + (let ([counter (fx+ counter 1)]) ;; clamps to most-positive-fixnum + counter)) +``` + +**Security value**: Buffer size calculations, array index computation, and protocol length fields must not silently overflow. + +### L5. Lifetime-Scoped Secrets + +Combine affine types with automatic memory wiping for cryptographic material. + +```scheme +;; Secret is wiped from memory when scope exits +(with-secret ([key (derive-key password salt)]) + (let ([ciphertext (encrypt key plaintext)]) + ;; key is wiped here, even on exception + ciphertext)) + +;; key is no longer accessible — affine type consumed + memory zeroed +``` + +**Implementation**: `with-secret` wraps the key in an affine type with a cleanup function that calls `bytevector-fill!` with zeros. The guardian ensures wiping even if the programmer forgets `affine-drop!`. + +### L6. Proof-Carrying Contracts + +Extend `define/contract` so that proven invariants can be propagated to callers, reducing redundant runtime checks. + +```scheme +(define/contract (safe-substring str start end) + (pre: (string? str) + (<= 0 start) (<= start end) (<= end (string-length str))) + (post: string?) + (proves: (NonNeg (string-length result)) + (<= (string-length result) (string-length str))) + (substring str start end)) + +;; Caller knows the result satisfies NonNeg length — no re-check needed +(define/contract (first-n-chars str n) + (pre: (string? str) (NonNeg n) (<= n (string-length str))) + (post: string?) + (safe-substring str 0 n)) ;; preconditions are discharged by post-conditions +``` + +### L7. Effect-Based I/O Interception + +Use the existing effect system to create auditable I/O layers where every filesystem, network, and process operation can be intercepted, logged, and policy-checked. + +```scheme +(with-handler ([file-read (lambda (path resume) + (audit-log! 'file-read `((path . ,path))) + (check-capability! 'filesystem 'read path) + (resume (real-file-read path)))] + [net-connect (lambda (host port resume) + (audit-log! 'net-connect `((host . ,host) (port . ,port))) + (check-capability! 'network 'connect host) + (resume (real-net-connect host port)))]) + (run-application)) +``` + +**Security value**: All I/O is mediated by handlers. Testing can install mock handlers. Production installs audit + policy handlers. There is no way to perform unmediated I/O. + +--- + +## Proposed: Cryptographic Foundation + +### C1. Direct libcrypto FFI — `(std crypto native)` + +Replace all shell-based crypto with direct FFI to OpenSSL's libcrypto. + +```scheme +;; Core primitives via FFI +(define-ffi-library libcrypto ("libcrypto.so") + ;; Digest + (EVP_MD_CTX_new () -> void*) + (EVP_MD_CTX_free (void*) -> void) + (EVP_DigestInit_ex (void* void* void*) -> int) + (EVP_DigestUpdate (void* u8* size_t) -> int) + (EVP_DigestFinal_ex (void* u8* void*) -> int) + (EVP_sha256 () -> void*) + (EVP_sha512 () -> void*) + + ;; CSPRNG + (RAND_bytes (u8* int) -> int) + + ;; HMAC + (HMAC (void* u8* int u8* int u8* void*) -> u8*) + + ;; Constant-time comparison + (CRYPTO_memcmp (u8* u8* size_t) -> int)) +``` + +**Eliminates**: Temp files, shell invocation, TOCTOU races, predictable random values. + +### C2. CSPRNG — `(std crypto random)` + +Cryptographically secure random number generation. + +```scheme +;; Generate random bytes +(random-bytes 32) ;; → bytevector of 32 random bytes +(random-bytes! bv) ;; Fill existing bytevector with random bytes + +;; Generate random values +(random-u64) ;; → random 64-bit unsigned integer +(random-token 32) ;; → hex-encoded random token string +(random-uuid) ;; → UUID v4 string + +;; Secure random choice +(random-choice '(a b c d)) ;; → uniformly random element +``` + +**Implementation**: `/dev/urandom` as primary source with `RAND_bytes` as fallback. Never use `(random N)` for security-relevant values. + +### C3. Timing-Safe Operations — `(std crypto compare)` + +Constant-time comparison for all secret material. + +```scheme +;; Constant-time bytevector comparison +(timing-safe-equal? bv1 bv2) ;; → boolean, constant-time + +;; Constant-time string comparison (via UTF-8 encoding) +(timing-safe-string=? s1 s2) ;; → boolean, constant-time + +;; HMAC verification (timing-safe internally) +(hmac-verify? key message expected-mac) +``` + +**Implementation**: XOR-accumulate over all bytes, check accumulator is zero. Length check returns `#f` in constant time relative to the shorter input (no early exit). + +### C4. Password Hashing — `(std crypto password)` + +Proper password storage with memory-hard KDFs. + +```scheme +;; Hash a password for storage +(password-hash "hunter2") +;; → "$argon2id$v=19$m=65536,t=3,p=4$salt$hash" + +;; Verify a password against stored hash +(password-verify? "hunter2" stored-hash) ;; → boolean (timing-safe) + +;; Configurable parameters +(password-hash "hunter2" + algorithm: 'argon2id + memory-cost: 65536 ;; KiB + time-cost: 3 ;; iterations + parallelism: 4) ;; threads +``` + +### C5. AEAD — `(std crypto aead)` + +Authenticated encryption with associated data. + +```scheme +;; Encrypt with authentication +(let-values ([(ciphertext tag) (aead-encrypt 'aes-256-gcm key nonce plaintext aad)]) + (values ciphertext tag)) + +;; Decrypt and verify (raises on tamper) +(aead-decrypt 'aes-256-gcm key nonce ciphertext tag aad) + +;; Supported algorithms +;; aes-128-gcm, aes-256-gcm, chacha20-poly1305 +``` + +### C6. Key Management — `(std crypto keys)` + +Key lifecycle management for long-running services. + +```scheme +;; Key ring with rotation +(define keyring (make-key-ring + current: (load-key "/run/secrets/current.key") + previous: (load-key "/run/secrets/previous.key"))) + +;; Encrypt with current key, decrypt tries all keys +(key-ring-encrypt keyring plaintext) +(key-ring-decrypt keyring ciphertext) ;; tries current, then previous + +;; Key derivation +(derive-subkey master-key "purpose:encryption" context) +(derive-subkey master-key "purpose:authentication" context) + +;; Secret wiping (via affine types) +(with-secret ([key (key-ring-current keyring)]) + (encrypt key data)) +;; key is zeroed here +``` + +--- + +## Proposed: Network and Protocol Hardening + +### N1. TLS Hardening — `(std net tls)` + +Secure defaults for all TLS connections. + +```scheme +;; Secure defaults (no opt-out for production) +(define tls-defaults + (make-tls-config + min-version: 'tls-1.2 + cipher-suites: '(TLS_AES_256_GCM_SHA384 + TLS_CHACHA20_POLY1305_SHA256 + TLS_AES_128_GCM_SHA256) + verify-peer: #t + verify-hostname: #t + certificate-pinning: #f ;; optional + ocsp-stapling: #t)) + +;; Certificate pinning for high-security connections +(define pinned-config + (tls-config-with tls-defaults + certificate-pinning: (pin-sha256 "base64-encoded-pin=="))) +``` + +### N2. HTTP Security Defaults — `(std net http-security)` + +Security headers and middleware for the HTTP server. + +```scheme +;; Security middleware stack (applied to all responses) +(define security-middleware + (compose-middleware + (cors-middleware allowed-origins: '("https://app.example.com") + allowed-methods: '(GET POST) + max-age: 86400) + (csp-middleware default-src: "'self'" + script-src: "'self'" + style-src: "'self' 'unsafe-inline'") + (hsts-middleware max-age: 31536000 include-subdomains: #t) + (xss-protection-middleware) + (content-type-nosniff-middleware) + (frame-options-middleware 'deny) + (request-id-middleware) + (request-size-limit-middleware max-body: (* 10 1024 1024)) ;; 10MB + (rate-limit-middleware limiter: (make-rate-limiter 100 10)))) + +;; Applied to router +(router-middleware! router security-middleware) +``` + +### N3. Input Sanitization — `(std security sanitize)` + +Context-aware input sanitization. + +```scheme +;; HTML entity escaping (XSS prevention) +(sanitize-html "<script>alert('xss')</script>") +;; → "<script>alert('xss')</script>" + +;; SQL parameterization (injection prevention) +(sql-escape "Robert'; DROP TABLE students;--") +;; → "Robert''; DROP TABLE students;--" +;; But prefer: parameterized queries always + +;; Path traversal prevention +(sanitize-path "../../etc/passwd") +;; → raises &path-traversal-violation +(safe-path-join base-dir user-input) +;; → resolves symlinks, verifies result is under base-dir + +;; Header injection prevention +(sanitize-header-value "value\r\nX-Injected: true") +;; → raises &header-injection-violation + +;; URL sanitization +(sanitize-url "javascript:alert(1)") +;; → raises &url-scheme-violation (only http/https allowed) +``` + +### N4. Connection Timeouts and Limits + +```scheme +;; TCP with deadlines +(tcp-connect host port + connect-timeout: 5000 ;; ms + read-timeout: 30000 ;; ms + write-timeout: 10000 ;; ms + idle-timeout: 60000) ;; ms + +;; HTTP request limits +(make-http-limits + max-header-size: 8192 ;; bytes + max-header-count: 100 + max-uri-length: 2048 ;; bytes + max-body-size: 10485760 ;; 10MB + request-timeout: 30000 ;; ms — Slowloris protection + keep-alive-timeout: 5000) ;; ms +``` + +### N5. Safe Process Execution — `(std misc process-safe)` + +Shell-free process execution. + +```scheme +;; Direct exec (no shell) — safe by default +(run-process/exec '("git" "log" "--oneline" "-10") + directory: "/path/to/repo" + environment: '(("PATH" . "/usr/bin:/bin")) ;; explicit, not inherited + timeout: 30000) + +;; Explicit shell (opt-in, requires capability) +(with-capabilities (list (make-process-capability spawn: #t)) + (lambda () + (run-process/shell "find . -name '*.log' | wc -l"))) +``` + +--- + +## Proposed: Operating System Integration + +### O1. seccomp-BPF Integration — `(std security seccomp)` + +Restrict available syscalls for sandboxed workers. + +```scheme +;; Define syscall whitelist +(define compute-only-filter + (make-seccomp-filter 'kill ;; default action: kill process + (allow 'read 'write 'close 'fstat 'mmap 'mprotect + 'munmap 'brk 'rt_sigaction 'rt_sigprocmask + 'clone 'exit_group 'futex))) + +;; Apply filter (irreversible — can only tighten after this) +(seccomp-install! compute-only-filter) + +;; Now: open, socket, execve, etc. → immediate SIGKILL +``` + +### O2. Landlock Integration — `(std security landlock)` + +Filesystem access control without root privileges (Linux 5.13+). + +```scheme +;; Restrict filesystem access +(with-landlock + (landlock-rules + (fs-read-only "/usr/lib" "/lib" "/etc/ssl") + (fs-read-write "/var/myapp/data") + (fs-no-access "/etc/shadow" "/root")) + (lambda () + ;; Application runs here with restricted filesystem + (start-server))) +``` + +### O3. Privilege Separation — `(std security privsep)` + +Fork-based privilege separation for critical operations. + +```scheme +;; Supervisor/worker architecture +(define-privilege-separated + (supervisor + (capabilities: (list (make-fs-capability read: #t write: #t) + (make-net-capability listen: #t))) + (on-request: (lambda (req) + (case (request-type req) + [(read-secret) (read-key-file (request-path req))] + [(audit-log) (write-audit-entry (request-data req))] + [else (error 'supervisor "unauthorized request")])))) + + (worker + (seccomp-filter: compute-only-filter) + (landlock: (fs-read-only "/usr/lib")) + (capabilities: (list (make-net-capability connect: #t))) + (entry-point: (lambda (supervisor-channel) + ;; Worker can only communicate via channel to supervisor + ;; Cannot read secrets directly, cannot write audit log directly + (let ([key (channel-request supervisor-channel 'read-secret "/run/secrets/key")]) + (process-requests key supervisor-channel)))))) +``` + +### O4. Namespace Isolation — `(std security namespace)` + +Linux namespace integration for container-like isolation. + +```scheme +;; Create isolated execution environment +(with-namespaces + (namespaces: '(mount pid net user)) + (mount-binds: '(("/usr/lib" . "/usr/lib") + ("/lib" . "/lib"))) + (network: 'loopback-only) + (lambda () + ;; Running in isolated namespace + ;; Own PID 1, own mount table, loopback-only network + (run-untrusted-plugin plugin-code))) +``` + +--- + +## Proposed: Supply Chain and Build Security + +### S1. Dependency Verification — `(std build verify)` + +Cryptographic verification of all dependencies. + +```scheme +;; Lock file with SHA-256 hashes (extend jerboa/lock.sls) +(lockfile + (entry "chez-ssl" "1.2.0" + hash: "sha256:a3f2b8c9d4e5f6a7b8c9d0e1f2a3b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1" + source: "https://github.com/ober/chez-ssl/archive/v1.2.0.tar.gz" + source-hash: "sha256:b4c5d6e7f8a9b0c1d2e3f4a5b6c7d8e9f0a1b2c3d4e5f6a7b8c9d0e1f2a3b4c5")) + +;; Build-time verification +(verify-dependencies! + lockfile: "jerboa.lock" + on-mismatch: 'abort) ;; 'abort | 'warn | 'update-lock +``` + +### S2. SBOM Generation — `(std build sbom)` + +Software Bill of Materials for auditing. + +```scheme +;; Generate SBOM in CycloneDX format +(generate-sbom + project: "myapp" + version: "1.0.0" + format: 'cyclonedx-json + include: '(runtime build test) + output: "sbom.json") + +;; Contents: +;; - Jerboa version and commit hash +;; - Chez Scheme version +;; - All chez-* library versions and hashes