From 9477a92140168cf19c2e343458057f22086619dc Mon Sep 17 00:00:00 2001 From: Reuben Brooks Date: Mon, 6 Jul 2026 11:15:29 -0500 Subject: [PATCH 1/6] shen.typecheck: read the judgment as one 'EXPR : TYPE' triple MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The embed helper read the type standalone, but read-from-string cooks expression and type positions differently: in expression position a compound form of three or more elements is curried into application syntax — (may alice read doc1) becomes ((((fn may) alice) read) doc1) — so any check against a 3+-ary user-datatype type silently returned false, in both engine modes. Only the form after : is kept as raw type syntax, so the helper now reads "EXPR : TYPE" together, the same triple shape (load)'s work-through consumes, and validates it is exactly three forms with : in the middle (which also fail-closes attempts to smuggle extra forms through either string). Simple (list X) types never tripped this — currying starts at two arguments — which is how the existing specs missed it. The regression tests use the examples/policy/policy_proof.shen authorization encoding, where the 4-ary (may S A R) is exactly the shape that broke. Co-Authored-By: Claude Fable 5 --- shen.lua | 31 ++++++++++++++++++++++--------- test/typecheck_api_spec.lua | 28 ++++++++++++++++++++++++++++ 2 files changed, 50 insertions(+), 9 deletions(-) diff --git a/shen.lua b/shen.lua index 0be9a08..e31b25c 100644 --- a/shen.lua +++ b/shen.lua @@ -97,11 +97,21 @@ end -- `shen.typecheck("[1 2]", "(list number)")`, not an evaluated list value). -- `ty` may use type variables: shen.typecheck("[1 2]", "A") infers. -- --- Two kernel traps this helper absorbs, both learned in production embeds: +-- Three kernel traps this helper absorbs, all learned in production embeds: -- 1. (shen.typecheck X A) takes the SYNTAX TREE of X — the form the reader -- produces — not X's value. Passing an evaluated value silently returns -- false for anything non-atomic. --- 2. The kernel's inference counter (shen.*infs*) is GLOBAL and cumulative, +-- 2. The reader cooks expression and type positions DIFFERENTLY, so the +-- two strings must be read together as one "EXPR : TYPE" triple — the +-- shape (load)'s work-through consumes. In expression position a +-- compound form of three or more elements is curried into application +-- syntax: (may alice read doc1) read standalone becomes +-- ((((fn may) alice) read) doc1), and a type in that shape makes every +-- check silently return false. Only the form after : is kept as raw +-- type syntax. ((list number) survives standalone reading — currying +-- starts at two arguments — which is how this bug hid behind simple +-- list types.) +-- 3. The kernel's inference counter (shen.*infs*) is GLOBAL and cumulative, -- and shen.typecheck never resets it; only the REPL's toplevel does. -- A long-lived embedder calling the kernel entry point directly crosses -- *maxinferences* (default 1,000,000) after enough checks, after which @@ -111,16 +121,19 @@ end -- Override the budget with shen.eval("(set shen.*maxinferences* N)"). function shen.typecheck(expr, ty) ensure_boot() - local eforms = P.F["read-from-string"](expr) - if not R.is_cons(eforms) then - error("shen.typecheck: no expression in " .. tostring(expr), 2) + local forms = P.F["read-from-string"](expr .. " : " .. ty) + local elems, n = {}, 0 + while R.is_cons(forms) do + n = n + 1 + elems[n] = forms[1] + forms = forms[2] end - local tforms = P.F["read-from-string"](ty) - if not R.is_cons(tforms) then - error("shen.typecheck: no type in " .. tostring(ty), 2) + if n ~= 3 or elems[2] ~= R.intern(":") then + error("shen.typecheck: expected one expression and one type in \"" + .. tostring(expr) .. " : " .. tostring(ty) .. "\"", 2) end P.GLOBALS["shen.*infs*"] = 0 - local ok, res = pcall(P.F["shen.typecheck"], eforms[1], tforms[1]) + local ok, res = pcall(P.F["shen.typecheck"], elems[1], elems[3]) if not ok then return false end -- budget exhausted or kernel error: fail closed return res end diff --git a/test/typecheck_api_spec.lua b/test/typecheck_api_spec.lua index 2c52a55..bfe4d75 100644 --- a/test/typecheck_api_spec.lua +++ b/test/typecheck_api_spec.lua @@ -56,6 +56,34 @@ check("datatype + verified premise holds", tyname(shen.typecheck('["hi"]', "spec check("verified premise fails", shen.typecheck('[""]', "spec-box"), false) check("wrong element type fails", shen.typecheck("[37]", "spec-box"), false) +-- ---- the regression: compound types of 3+ elements --------------------------- +-- The reader cooks expression and type positions differently: read standalone, +-- (may alice write doc1) curries to ((((fn may) alice) write) doc1) and the +-- check silently returns false. The helper must read "EXPR : TYPE" as ONE +-- triple (the (load) work-through shape) so the type stays raw syntax. Simple +-- (list X) types never trip this — currying starts at two arguments — so the +-- checks above can't catch it; this is the examples/policy/policy_proof.shen +-- authorization encoding, where a term of (may S A R) is a proof of permission. +shen.eval([[ +(datatype spec-authz + ______________________________ + [owns-fact] : (owns alice doc1); + + ______________________________________ + [alice-tenant] : (same-tenant alice doc1); + + P : (owns S R); Q : (same-tenant S R); + ====================================== + [by-owner P Q] : (may S A R);) +]]) +check("4-ary compound type inhabited", + shen.typecheck("[by-owner [owns-fact] [alice-tenant]]", "(may alice write doc1)")) +check("4-ary compound type: infs consumed (not a silent false)", + shen.value("shen.*infs*") > 0, true) +check("4-ary compound type uninhabited fails", + shen.typecheck("[by-owner [owns-fact] [alice-tenant]]", "(may bob write doc1)"), false) +check("2-ary compound type still fine", shen.typecheck("[owns-fact]", "(owns alice doc1)")) + -- ---- the regression: cumulative inference exhaustion ------------------------ -- Lower the budget so the bug (were it present) would trip in tens of checks, -- then run 200: with the per-call reset every check must keep agreeing. From 3f03114f68ce071265721c2ea5647f433fd83a12 Mon Sep 17 00:00:00 2001 From: Reuben Brooks Date: Mon, 6 Jul 2026 11:20:06 -0500 Subject: [PATCH 2/6] examples: proof-carrying requests (pcr) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The runtime-typechecking counterpart to the policy example's compiled decision tier: the client attaches a proof term (X-Proof) and the OpenResty gate CHECKS it against the judgment (may subject action resource) built from the request — it never searches. Checking a given term is bounded by its size (the demo's deepest proof: 50 inferences, ~400 us warm, ~2.5k checks/sec/core), so the expensive open-ended direction never runs at request time, and every allowed request is logged with the proof that justified it. A delegation rule shows why proofs beat booleans and bearer scopes: carol's authority is a nested term carrying the whole justification chain (alice delegated AND alice owns AND alice is in the tenant), re-verified on every use — and a chain built on the wrong subterm fails to connect. The proof is treated as hostile input, each defense a selftest case: judgment atoms pass a bare-symbol whitelist so request data cannot smuggle syntax into the type; the shen.typecheck triple shape blocks smuggling a different judgment through the proof string; reader errors, oversized terms and over-budget terms (per-check *maxinferences*, counter reset per call) all fail closed. Proofs are read, never evaluated. Selftest passes under both engine modes (native and SHEN_TYPECHECK_NATIVE=off); exercised end-to-end through openresty. Depends on the shen.typecheck triple-read fix — 3+-ary compound types like (may S A R) were unreadable through the embed helper before it. Co-Authored-By: Claude Fable 5 --- .gitignore | 7 +- examples/README.md | 1 + examples/pcr/README.md | 102 +++++++++++++++++++++++++ examples/pcr/app.lua | 135 +++++++++++++++++++++++++++++++++ examples/pcr/json_shim.lua | 148 +++++++++++++++++++++++++++++++++++++ examples/pcr/nginx.conf | 71 ++++++++++++++++++ examples/pcr/rules.shen | 48 ++++++++++++ examples/pcr/selftest.lua | 67 +++++++++++++++++ 8 files changed, 578 insertions(+), 1 deletion(-) create mode 100644 examples/pcr/README.md create mode 100644 examples/pcr/app.lua create mode 100644 examples/pcr/json_shim.lua create mode 100644 examples/pcr/nginx.conf create mode 100644 examples/pcr/rules.shen create mode 100644 examples/pcr/selftest.lua diff --git a/.gitignore b/.gitignore index c41455a..ccbfdd5 100644 --- a/.gitignore +++ b/.gitignore @@ -5,4 +5,9 @@ build/shen-bundle.lua .fasl-test/ luacov.stats.out luacov.report.out -examples/openresty/logs/ +examples/*/logs/ +examples/*/client_body_temp/ +examples/*/fastcgi_temp/ +examples/*/proxy_temp/ +examples/*/scgi_temp/ +examples/*/uwsgi_temp/ diff --git a/examples/README.md b/examples/README.md index 2fec0ca..a1cc931 100644 --- a/examples/README.md +++ b/examples/README.md @@ -12,6 +12,7 @@ has a `selftest.lua` that runs off-nginx): | [`configc/`](configc/) | a typed config **compiler**: one config validates *and* generates a Kubernetes Deployment + nginx server block; a generator type-bug is caught at load. `luajit examples/configc/configc.lua` | | [`policy/`](policy/) | a typed **authorization** gateway: one rule set enforced at the OpenResty edge and previewed in the browser, plus authz-as-type-inhabitation (a permission *is* a proof). `luajit examples/policy/selftest.lua` | | [`crdt/`](crdt/) | a **CRDT** sync hub: replicas converge via a typed join-semilattice merge whose laws are checked by execution *and* by machine-checked sequent-calculus proof. `luajit examples/crdt/selftest.lua` | +| [`pcr/`](pcr/) | **proof-carrying requests**: the client attaches a proof term, the OpenResty gate *checks* it against `(may subject action resource)` — never searches — and logs the proof as the audit trail; delegation makes proofs compose into justification chains. `luajit examples/pcr/selftest.lua` | | [`openresty/`](openresty/) | a complete web app — typed Shen validators + a Shen router on OpenResty (nginx + LuaJIT), with a front end that runs the **same** rules in the browser (Ratatoskr-shaken, ShenScript-compiled). Runs standalone via `luajit examples/openresty/selftest.lua`; see [its README](openresty/README.md) to serve it. | The last three (`configc/`, `policy/`, `crdt/`) are a themed trio: each extracts diff --git a/examples/pcr/README.md b/examples/pcr/README.md new file mode 100644 index 0000000..df7e1bf --- /dev/null +++ b/examples/pcr/README.md @@ -0,0 +1,102 @@ +# Proof-carrying requests + +An authorization gateway where the client **carries the proof** and the edge +only **checks** it. Every request to `/protected/` presents a proof term in +`X-Proof`; the gate builds the judgment `(may SUBJECT ACTION RESOURCE)` from +the request and asks Shen's sequent-calculus typechecker whether the presented +term inhabits it. No proof that checks, no access — and every allowed request +is logged **with its proof**: the audit trail is the justification itself, +machine-checked at the moment of use. + +``` +luajit examples/pcr/selftest.lua # everything below, off-nginx + +mkdir -p examples/pcr/logs # or serve it: +openresty -p "$PWD/examples/pcr" -c nginx.conf +``` + +## The idea: check, don't search + +[`examples/policy/policy_proof.shen`](../policy/policy_proof.shen) shows +authorization as type inhabitation — a permission *is* a proof, checked +offline when the file loads. This example promotes that from a demonstration +to a **wire protocol**, and the move that makes it affordable at request time +is an asymmetry: + +* **Searching** for a proof (is `(may S A R)` inhabited at all?) is the + open-ended, expensive direction. +* **Checking** a *given* term against a *given* type is bounded by the size + of the term. + +So search never runs at request time. The client obtained its proof earlier — +at token issuance, from a policy service, or built from the same rules +client-side (the [`openresty/`](../openresty/) example runs Shen rules in the +browser) — and the gate's entire per-request cost is one bounded check: +the demo's deepest proof (a delegation chain) checks in **50 inferences, +~400 µs warm** on this port, several thousand checks per second per core. +That fits anywhere an LLM call, a database query, or a network hop is already +in the loop — agent/MCP tool gates, internal APIs, admin planes. + +## Proofs compose: delegation as an audit chain + +The payoff of carrying proofs instead of booleans or bearer scopes is that +proofs **compose**. `rules.shen` has a delegation rule: + +``` +P : (may S A R); Q : (delegates S T); +===================================== +[by-delegation P Q] : (may T A R); +``` + +so carol's authority to write `doc1` is the *nested* term + +``` +[by-delegation [by-owner [owns-fact] [alice-tenant]] [deleg-fact]] +``` + +— readable, machine-checked provenance: carol may write **because** alice +delegated to her **and** alice owns it **and** alice is in the resource's +tenant. A bearer token says *that* you may; a proof term says *why*, and the +why is re-verified on every use. Swap the inner proof for bob's read-only one +and the chain no longer connects (`[deleg-fact]` proves `(delegates alice +carol)`, not bob) — the check fails. Run the selftest to see it. + +## Threat model (the proof is hostile input) + +The proof term is attacker-controlled, so the gate treats it accordingly — +each line is a selftest case: + +| attack | defense | +|---|---| +| present someone else's proof | a proof is bound to the **exact judgment**: alice's ownership proof does not establish `(may bob write doc1)` — denied | +| smuggle a different judgment inside the proof string | `shen.typecheck` reads `"PROOF : TYPE"` as one triple and rejects any other shape — denied as malformed | +| inject syntax through subject/action/resource | judgment atoms pass a bare-symbol whitelist before the reader ever sees them — parens, brackets, colons, whitespace never reach the type | +| unreadable / unbalanced term | reader error is trapped — fail closed | +| adversarially deep term | `*maxinferences*` acts as a **per-check budget** (the helper resets the counter per call) — fail closed, next request unaffected | +| oversized term | byte cap before parsing | +| evaluate something | proofs are **read, never evaluated** — a term is syntax judged by the typechecker | + +What remains trusted: the rules file (loaded under `(tc +)` at worker start), +the ~30-line gate glue, and — for this demo — the headers standing in for an +authenticated subject. In production the subject comes from a verified +JWT/session; the *proof* is exactly where it belongs, presented by the client. + +## The two tiers compose + +This is the runtime half of a staged architecture. For decisions over a +**finite, statically known** domain, compile the policy to a certified +decision procedure at deploy time and pay nanoseconds per request (the +[`policy/`](../policy/) example's `decide` is that tier). Proof-carrying +requests are the tier for what that cannot cover: judgments over **dynamic +data** — delegation chains, per-request facts, open-ended agent tool calls — +where enumeration is impossible but checking a presented justification is +cheap, bounded, and leaves an audit artifact. + +## Files + +| file | what it is | +|---|---| +| `rules.shen` | the logic: facts, grant rules, delegation — a term of `(may S A R)` is a permission | +| `app.lua` | the gateway: judgment construction, hostile-input handling, the check, the audit log | +| `selftest.lua` | every allow/deny/attack case off-nginx, plus the warm timing loop | +| `nginx.conf` | the OpenResty wiring and curl walkthrough | diff --git a/examples/pcr/app.lua b/examples/pcr/app.lua new file mode 100644 index 0000000..11fec9e --- /dev/null +++ b/examples/pcr/app.lua @@ -0,0 +1,135 @@ +-- examples/pcr/app.lua — proof-carrying requests: the gateway CHECKS, never searches. +-- +-- The client attaches a proof term (X-Proof) to the request. The gate builds +-- the judgment (may SUBJECT ACTION RESOURCE) from the request and asks the +-- kernel's sequent-calculus typechecker whether the presented term inhabits +-- it. Allowed requests carry their own justification — the proof term IS the +-- audit trail, and it is logged with the inference count of its checking. +-- +-- The proof is UNTRUSTED input. It is read (parsed), never evaluated; the +-- judgment is built only from atoms that pass a whitelist, so request data +-- cannot smuggle syntax into the type; shen.typecheck reads "PROOF : TYPE" as +-- one triple and rejects any other shape, so a proof string cannot smuggle a +-- different judgment past the check; and a per-check inference budget makes +-- adversarially deep terms fail closed. A proof is bound to the EXACT +-- judgment: presenting alice's ownership proof on bob's request checks +-- (may bob ...), which that term does not establish. +-- +-- Kernel boot + the typed load of rules.shen happen ONCE per worker. + +local APP_DIR = debug.getinfo(1, "S").source:match("^@(.*)[/\\][^/\\]+$") or "." + +local shen = require("shen") +local P = shen.prims + +local cjson +do + local ok, m = pcall(require, "cjson.safe") + if not ok then ok, m = pcall(require, "cjson") end + cjson = ok and m or assert(loadfile(APP_DIR .. "/json_shim.lua"))() +end + +shen.boot{quiet = true} +shen.eval("(tc +)") +P.F["load"](APP_DIR .. "/rules.shen") +shen.eval("(tc -)") + +-- shen.typecheck resets shen.*infs* per call, so *maxinferences* acts as a +-- per-check budget: a term needing more than this fails closed. The demo's +-- deepest proof (delegation) checks in 50 inferences. +shen.eval("(set shen.*maxinferences* 10000)") +local MAX_PROOF_BYTES = 1024 + +-- Judgment atoms: bare symbols only. Anything a client could use to alter +-- the shape of the type — parens, brackets, whitespace, colon, quotes — +-- is refused before the reader ever sees it. +local function atom_ok(s) + return type(s) == "string" and s ~= "" and s:match("^[%w%-%.%_]+$") ~= nil +end + +-- ---- check one request ------------------------------------------------------ +-- Returns authorized(bool), reason(string), audit(table|nil). +local function check(subject, action, resource, proof) + if not (atom_ok(subject) and atom_ok(action) and atom_ok(resource)) then + return false, "malformed subject/action/resource", nil + end + if type(proof) ~= "string" or proof == "" then + return false, "no proof presented", nil + end + if #proof > MAX_PROOF_BYTES then + return false, "proof too large", nil + end + local judgment = "(may " .. subject .. " " .. action .. " " .. resource .. ")" + -- pcall: an unreadable term or a smuggled extra form errors — fail closed + local ok, res = pcall(shen.typecheck, proof, judgment) + if not ok then + return false, "malformed proof", nil + end + if res == false then + return false, "proof does not establish " .. judgment, nil + end + return true, "proof checks", { + judgment = judgment, + proof = proof, + infs = shen.value("shen.*infs*"), + } +end + +-- ---- request handling (pure; shared with selftest) -------------------------- +local function dispatch(method, path, body) + if path == "/api/check" and method == "POST" then + body = body or {} + local authorized, reason, audit = check(body.subject, body.action, body.resource, body.proof) + local out = { authorized = authorized, reason = reason } + if audit then out.judgment, out.infs = audit.judgment, audit.infs end + return 200, out + end + return 404, { error = "not found" } +end + +local M = { dispatch = dispatch, check = check, json = cjson } + +function M.handle() + local method = ngx.req.get_method() + local decoded + if method == "POST" then + ngx.req.read_body() + local raw = ngx.req.get_body_data() + if raw and raw ~= "" then + local d = cjson.decode(raw) + if d == nil then + ngx.status = 400; ngx.header.content_type = "application/json" + ngx.say(cjson.encode({ error = "invalid JSON" })); return + end + decoded = d + end + end + local status, body = dispatch(method, ngx.var.uri, decoded) + ngx.status = status + ngx.header.content_type = "application/json" + ngx.say(cjson.encode(body)) +end + +-- ---- the enforcement gate (access_by_lua on /protected/) -------------------- +-- Subject and resource come from headers for the demo; in production the +-- subject comes from a verified JWT/session. The PROOF though is exactly +-- where it belongs: presented by the client, per request. +function M.gate() + local h = ngx.req.get_headers() + local action = ngx.req.get_method() == "GET" and "read" or "write" + local authorized, reason, audit = + check(h["x-subject"], action, h["x-resource"], h["x-proof"]) + if not authorized then + ngx.status = 403 + ngx.header.content_type = "application/json" + ngx.say(cjson.encode({ error = "forbidden", reason = reason })) + return ngx.exit(403) + end + -- the audit line: who did what, justified by which proof, at what cost + ngx.log(ngx.INFO, "authorized ", audit.judgment, + " by ", audit.proof, " (", audit.infs, " inferences)") + ngx.header["X-Proof-Checked"] = tostring(audit.infs) .. " inferences" + -- fall through to the protected content +end + +return M diff --git a/examples/pcr/json_shim.lua b/examples/pcr/json_shim.lua new file mode 100644 index 0000000..0cd6bc6 --- /dev/null +++ b/examples/pcr/json_shim.lua @@ -0,0 +1,148 @@ +-- examples/openresty/json_shim.lua — a minimal JSON codec. +-- +-- Used ONLY when the real lua-cjson is unavailable (i.e. running the example +-- off-nginx under plain luajit, e.g. selftest.lua). OpenResty bundles cjson, +-- so under the actual server this file is never loaded. It implements just +-- the surface app.lua uses: decode, encode, and an empty_array sentinel. + +local json = {} + +-- A unique sentinel so an empty Lua table can be encoded as [] not {}. +json.empty_array = setmetatable({}, { __tostring = function() return "[]" end }) + +-- ---- encode ---------------------------------------------------------------- +local escapes = { ['"'] = '\\"', ['\\'] = '\\\\', ['\n'] = '\\n', + ['\r'] = '\\r', ['\t'] = '\\t' } +local function enc_str(s) + return '"' .. s:gsub('[%z\1-\31"\\]', function(c) + return escapes[c] or ('\\u%04x'):format(c:byte()) + end) .. '"' +end + +local encode +local function enc_table(v, out) + if v == json.empty_array then out[#out + 1] = "[]"; return end + local n = #v + local is_array = n > 0 + if is_array then + out[#out + 1] = "[" + for i = 1, n do + if i > 1 then out[#out + 1] = "," end + encode(v[i], out) + end + out[#out + 1] = "]" + else + -- object (or empty table -> {}) + out[#out + 1] = "{" + local first = true + for k, val in pairs(v) do + if not first then out[#out + 1] = "," end + first = false + out[#out + 1] = enc_str(tostring(k)); out[#out + 1] = ":" + encode(val, out) + end + out[#out + 1] = "}" + end +end + +encode = function(v, out) + local t = type(v) + if t == "string" then out[#out + 1] = enc_str(v) + elseif t == "number" then out[#out + 1] = tostring(v) + elseif t == "boolean" then out[#out + 1] = v and "true" or "false" + elseif t == "nil" then out[#out + 1] = "null" + elseif t == "table" then enc_table(v, out) + else error("json: cannot encode " .. t) end +end + +function json.encode(v) + local out = {} + encode(v, out) + return table.concat(out) +end + +-- ---- decode (small recursive-descent parser) ------------------------------- +local function decode_error(s, i, msg) + error(("json: %s at byte %d"):format(msg, i), 0) +end + +local parse_value +local function skip_ws(s, i) + local _, j = s:find("^[ \t\r\n]*", i) + return (j or i - 1) + 1 +end + +local function parse_string(s, i) + i = i + 1 -- skip opening quote + local buf = {} + while i <= #s do + local c = s:sub(i, i) + if c == '"' then return table.concat(buf), i + 1 + elseif c == '\\' then + local e = s:sub(i + 1, i + 1) + local map = { ['"'] = '"', ['\\'] = '\\', ['/'] = '/', n = '\n', + t = '\t', r = '\r', b = '\b', f = '\f' } + if map[e] then buf[#buf + 1] = map[e]; i = i + 2 + elseif e == 'u' then + local hex = s:sub(i + 2, i + 5) + buf[#buf + 1] = string.char(tonumber(hex, 16) % 256); i = i + 6 + else decode_error(s, i, "bad escape") end + else buf[#buf + 1] = c; i = i + 1 end + end + decode_error(s, i, "unterminated string") +end + +local function parse_number(s, i) + local j = s:find("[^%d%+%-eE%.]", i) or (#s + 1) + local num = tonumber(s:sub(i, j - 1)) + if not num then decode_error(s, i, "bad number") end + return num, j +end + +parse_value = function(s, i) + i = skip_ws(s, i) + local c = s:sub(i, i) + if c == '"' then return parse_string(s, i) + elseif c == '{' then + local obj = {} + i = skip_ws(s, i + 1) + if s:sub(i, i) == '}' then return obj, i + 1 end + while true do + local key; key, i = parse_string(s, skip_ws(s, i)) + i = skip_ws(s, i) + if s:sub(i, i) ~= ':' then decode_error(s, i, "expected ':'") end + local val; val, i = parse_value(s, i + 1) + obj[key] = val + i = skip_ws(s, i) + local d = s:sub(i, i) + if d == '}' then return obj, i + 1 + elseif d == ',' then i = skip_ws(s, i + 1) + else decode_error(s, i, "expected ',' or '}'") end + end + elseif c == '[' then + local arr = {} + i = skip_ws(s, i + 1) + if s:sub(i, i) == ']' then return arr, i + 1 end + while true do + local val; val, i = parse_value(s, i) + arr[#arr + 1] = val + i = skip_ws(s, i) + local d = s:sub(i, i) + if d == ']' then return arr, i + 1 + elseif d == ',' then i = i + 1 + else decode_error(s, i, "expected ',' or ']'") end + end + elseif s:sub(i, i + 3) == "true" then return true, i + 4 + elseif s:sub(i, i + 4) == "false" then return false, i + 5 + elseif s:sub(i, i + 3) == "null" then return nil, i + 4 + else return parse_number(s, i) end +end + +-- cjson.safe-style: returns nil, errmsg on failure rather than throwing. +function json.decode(s) + local ok, v = pcall(parse_value, s, 1) + if not ok then return nil, v end + return v +end + +return json diff --git a/examples/pcr/nginx.conf b/examples/pcr/nginx.conf new file mode 100644 index 0000000..5b2d804 --- /dev/null +++ b/examples/pcr/nginx.conf @@ -0,0 +1,71 @@ +# examples/pcr/nginx.conf — proof-carrying requests on OpenResty. +# +# mkdir -p examples/pcr/logs +# openresty -p "$PWD/examples/pcr" -c nginx.conf +# +# The client carries the proof; the gate only CHECKS it (never searches). +# +# # allowed — alice owns doc1, and her proof says so: +# curl -i -H 'X-Subject: alice' -H 'X-Resource: doc1' \ +# -H 'X-Proof: [by-owner [owns-fact] [alice-tenant]]' \ +# -X POST localhost:8093/protected/ +# +# # allowed — carol acts under alice's delegation; the nested proof is the +# # whole audit chain (carol may write BECAUSE alice delegated AND alice owns): +# curl -i -H 'X-Subject: carol' -H 'X-Resource: doc1' \ +# -H 'X-Proof: [by-delegation [by-owner [owns-fact] [alice-tenant]] [deleg-fact]]' \ +# -X POST localhost:8093/protected/ +# +# # denied — bob presents ALICE's proof: it does not establish (may bob write doc1): +# curl -i -H 'X-Subject: bob' -H 'X-Resource: doc1' \ +# -H 'X-Proof: [by-owner [owns-fact] [alice-tenant]]' \ +# -X POST localhost:8093/protected/ +# +# # denied — bob's member proof grants read, and GET asks read, so this passes: +# curl -i -H 'X-Subject: bob' -H 'X-Resource: doc1' \ +# -H 'X-Proof: [by-member-read [member-fact] [tenant-fact]]' \ +# localhost:8093/protected/ + +daemon off; +worker_processes 1; +pid logs/nginx.pid; +error_log logs/error.log info; # the proof audit lines land here + +events { worker_connections 256; } + +http { + access_log logs/access.log; + + types { + application/json json; + text/plain shen; + } + default_type application/octet-stream; + + init_by_lua_block { + local prefix = ngx.config.prefix() + package.path = prefix .. "../../?.lua;" .. prefix .. "?.lua;" .. package.path + } + + # boot Shen + typed load once per worker + init_worker_by_lua_block { require("app") } + + server { + listen 8093; + + # preview endpoint: POST {subject, action, resource, proof} + location /api/ { + content_by_lua_block { require("app").handle() } + } + + # the enforcement gate: the proof is checked BEFORE the content runs + location /protected/ { + access_by_lua_block { require("app").gate() } + content_by_lua_block { ngx.header.content_type = "application/json" + ngx.say('{"ok":true,"secret":"the protected resource"}') } + } + + # serve the logic itself (one source of truth) + location = /rules.shen { default_type text/plain; alias rules.shen; } + } +} diff --git a/examples/pcr/rules.shen b/examples/pcr/rules.shen new file mode 100644 index 0000000..1049d50 --- /dev/null +++ b/examples/pcr/rules.shen @@ -0,0 +1,48 @@ +\\ examples/pcr/rules.shen — the authorization logic for proof-carrying requests. +\\ +\\ A term of type (may S A R) is a PROOF that subject S may perform action A on +\\ resource R. The gateway never SEARCHES for such a term — the client carries +\\ one with the request (X-Proof), and the gateway merely CHECKS it against the +\\ judgment built from the request. Checking a given term is bounded by the +\\ term's size; search is the expensive, open-ended direction, and it never +\\ runs at request time. +\\ +\\ Same logic as examples/policy/policy_proof.shen, promoted from an offline +\\ demonstration to the wire protocol — plus a delegation rule, because the +\\ payoff of carrying PROOFS instead of booleans is that proofs COMPOSE: a +\\ delegated permission is a nested term whose subterms are the entire audit +\\ chain of *why*. + +(datatype authz + \\ -- environment facts (axioms; a directory or DB would supply these) ------ + ______________________________ + [owns-fact] : (owns alice doc1); + + ______________________________________ + [alice-tenant] : (same-tenant alice doc1); + + _________________________________ + [member-fact] : (has-role bob member); + + ____________________________________ + [tenant-fact] : (same-tenant bob doc1); + + ______________________________________ + [deleg-fact] : (delegates alice carol); + + \\ -- grant rules (universal in S, A, R, T) --------------------------------- + \\ an owner inside the resource's tenant may take ANY action on it + P : (owns S R); Q : (same-tenant S R); + ====================================== + [by-owner P Q] : (may S A R); + + \\ a member inside the resource's tenant may READ it + P : (has-role S member); Q : (same-tenant S R); + =============================================== + [by-member-read P Q] : (may S read R); + + \\ whatever S may do, S may delegate: the delegate's proof CONTAINS the + \\ delegator's proof — the full justification chain travels with the request + P : (may S A R); Q : (delegates S T); + ===================================== + [by-delegation P Q] : (may T A R);) diff --git a/examples/pcr/selftest.lua b/examples/pcr/selftest.lua new file mode 100644 index 0000000..7d1148b --- /dev/null +++ b/examples/pcr/selftest.lua @@ -0,0 +1,67 @@ +-- examples/pcr/selftest.lua — verify the proof-carrying-request gateway off-nginx. +-- +-- luajit examples/pcr/selftest.lua (from the repo root) +-- +-- Drives the SAME check() the edge gate uses: the allow cases (including a +-- nested delegation proof), every category of denial — no proof, wrong rule, +-- a spoofed proof bound to someone else's judgment, judgment injection, proof +-- smuggling, oversized and over-budget terms — and a warm timing loop. +-- No nginx, no network. + +local root = arg[0]:match("^(.*)/examples/pcr/[^/]+$") or "." +package.path = root .. "/?.lua;" .. root .. "/examples/pcr/?.lua;" .. package.path + +local app = require("app") +local shen = require("shen") + +local fail = 0 +local function expect(label, want, subject, action, resource, proof) + local authorized, reason = app.check(subject, action, resource, proof) + io.write((" %-28s %-5s %s\n"):format(label, authorized and "ALLOW" or "DENY", reason)) + if authorized ~= want then fail = fail + 1; print(" FAIL: expected " .. tostring(want)) end +end + +local owner_proof = "[by-owner [owns-fact] [alice-tenant]]" +local member_proof = "[by-member-read [member-fact] [tenant-fact]]" +local deleg_proof = "[by-delegation " .. owner_proof .. " [deleg-fact]]" + +print("== proofs that check ==") +expect("owner writes", true, "alice", "write", "doc1", owner_proof) +expect("same proof, any action", true, "alice", "delete", "doc1", owner_proof) +expect("member reads", true, "bob", "read", "doc1", member_proof) +expect("delegate writes", true, "carol", "write", "doc1", deleg_proof) + +print("\n== denials: the proof is bound to the exact judgment ==") +expect("read proof, delete asked", false, "bob", "delete", "doc1", member_proof) +expect("spoof: alice's proof, bob", false, "bob", "write", "doc1", owner_proof) +expect("delegation chain broken", false, "carol", "read", "doc1", + "[by-delegation " .. member_proof .. " [deleg-fact]]") + +print("\n== denials: hostile input fails closed ==") +expect("no proof", false, "alice", "write", "doc1", nil) +expect("unreadable proof", false, "alice", "write", "doc1", "[by-owner [owns-fact") +expect("smuggled judgment", false, "bob", "delete", "doc1", + member_proof .. " : (may bob read doc1)") -- extra forms: shape check trips +expect("judgment injection", false, "doc1) (may bob delete doc1", "write", "doc1", owner_proof) +expect("oversized proof", false, "alice", "write", "doc1", + "[by-owner " .. string.rep("[owns-fact] ", 200) .. "]") + +-- a term needing more inferences than the budget fails closed, and the next +-- check recovers (shen.typecheck resets the counter per call) +local prev_max = shen.value("shen.*maxinferences*") +shen.eval("(set shen.*maxinferences* 1)") +expect("over budget", false, "alice", "write", "doc1", owner_proof) +shen.eval("(set shen.*maxinferences* " .. tostring(prev_max) .. ")") +expect("recovers after budget", true, "alice", "write", "doc1", owner_proof) + +print("\n== warm cost of checking (this is the whole per-request price) ==") +for _ = 1, 200 do app.check("carol", "write", "doc1", deleg_proof) end -- warmup +local N = 2000 +local t0 = os.clock() +for _ = 1, N do app.check("carol", "write", "doc1", deleg_proof) end +local us = (os.clock() - t0) * 1e6 / N +io.write((" nested delegation proof: %.0f us/check (%d inferences), ~%d checks/sec/core\n") + :format(us, shen.value("shen.*infs*"), math.floor(1e6 / us))) + +if fail == 0 then print("\nOK — all checks passed") +else print(("\n%d check(s) FAILED"):format(fail)); os.exit(1) end From 680a2824b38cb48a0ce11f7711b9d163b46bb822 Mon Sep 17 00:00:00 2001 From: Reuben Brooks Date: Mon, 6 Jul 2026 14:02:38 -0500 Subject: [PATCH 3/6] examples/pcr: dynamic facts + revocation (PCR-Live) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Facts stop being axioms. One side-condition rule replaces them all — if (pcr.fact? Pred S R) ... [fact Pred S R] : (Pred S R) — discharged against a versioned live fact store (facts.lua) at proof-check time through the typed lua.function bridge. Granting a fact makes proofs start checking; revoking it makes the SAME proof bytes stop checking on the very next request, on every worker: neither engine memoizes answers (the only caches hold translated clause code), so revocation has zero staleness at the checker. The fact leaf carries its ground triple because a side condition can only check, never bind — a bare-token leaf breaks under by-delegation, where S is not in the final judgment. The store is ONE atomically-written {version, synced_at, facts} blob in a lua_shared_dict (pure-Lua cell under plain luajit): one blob = one epoch, so a check can never mix two fact worlds, an evicted or undecodable blob is a deny, and freshness can never be stamped by a failed sync. Authoritative mode (demo: /admin/grant + /admin/revoke) has structurally zero staleness; replica mode (periodic pull stub of period W) hard-caps the window at 3W by denying everything when the sync ages out — outages degrade to denial, never frozen grants. Fact values may be numbers: absolute expiry checked against the live clock, i.e. time-limited grants that need no revoke call. The audit line gains the fact-world version and the exact fact leaves consumed; archiving {version, facts} per bump makes any logged triple offline-replayable. New Enemy variant 1 is bounded by W; variant 2 is documented with the zookie-style min-version extension as the named path, not built. Hostile-input posture: nothing reaches the reader un-vetted (the symbol table is permanent, ~194 B/symbol) — subject/action/resource and every proof token must be static vocabulary or an atom of a seen fact world, monotone so revocation denies at the type level with the honest reason, with a bounded distinct-atom budget as backstop (selftest: 10k distinct hostile atoms, zero heap growth). The guard allowlists fact predicates (a leaf can never assert (may ...)), rejects "/" (store-key forgery) and non-strings (unbound pvars), and a throwing store denies without poisoning the next check. Engine parity is a tested invariant: side conditions MUST use the typed bridge (a raw P.F guard passed native but failed CPS for a byte-identical rule), and the selftest parity leg asserts identical verdicts AND inference counts under SHEN_TYPECHECK_NATIVE=off. Datatype reloading as the fact substrate was disqualified by measurement (hundreds of ms + permanent leak per reload, compiler wall near 200 axioms): the datatype compiles once; the store changes. Verified: selftest green in both engine modes with byte-identical deterministic output; make test 471/471; make certify 100%; live through openresty with worker_processes 2 — 30 concurrent requests split across both workers all 403 on the first request after one revoke, and the boot path (bridge -> tc+ load -> fasl record/replay) probed identical across {native,CPS} x {fasl cold,warm}. ~517 us/check warm for the delegation proof (50 inferences, cheaper than the 69 the static axioms cost). Co-Authored-By: Claude Fable 5 --- examples/README.md | 2 +- examples/pcr/README.md | 199 ++++++++++++++++++++++++-------------- examples/pcr/app.lua | 160 +++++++++++++++++++++++------- examples/pcr/facts.lua | 183 +++++++++++++++++++++++++++++++++++ examples/pcr/nginx.conf | 48 +++++---- examples/pcr/rules.shen | 45 +++++---- examples/pcr/selftest.lua | 139 ++++++++++++++++++++------ 7 files changed, 598 insertions(+), 178 deletions(-) create mode 100644 examples/pcr/facts.lua diff --git a/examples/README.md b/examples/README.md index a1cc931..a76e3c1 100644 --- a/examples/README.md +++ b/examples/README.md @@ -12,7 +12,7 @@ has a `selftest.lua` that runs off-nginx): | [`configc/`](configc/) | a typed config **compiler**: one config validates *and* generates a Kubernetes Deployment + nginx server block; a generator type-bug is caught at load. `luajit examples/configc/configc.lua` | | [`policy/`](policy/) | a typed **authorization** gateway: one rule set enforced at the OpenResty edge and previewed in the browser, plus authz-as-type-inhabitation (a permission *is* a proof). `luajit examples/policy/selftest.lua` | | [`crdt/`](crdt/) | a **CRDT** sync hub: replicas converge via a typed join-semilattice merge whose laws are checked by execution *and* by machine-checked sequent-calculus proof. `luajit examples/crdt/selftest.lua` | -| [`pcr/`](pcr/) | **proof-carrying requests**: the client attaches a proof term, the OpenResty gate *checks* it against `(may subject action resource)` — never searches — and logs the proof as the audit trail; delegation makes proofs compose into justification chains. `luajit examples/pcr/selftest.lua` | +| [`pcr/`](pcr/) | **proof-carrying requests over live facts**: the client attaches a proof term, the OpenResty gate *checks* it — never searches — against a versioned fact store consulted at proof time, so revoking one fact makes the same proof bytes fail on the next request while delegation chains stay composable and every allow logs its full justification. `luajit examples/pcr/selftest.lua` | | [`openresty/`](openresty/) | a complete web app — typed Shen validators + a Shen router on OpenResty (nginx + LuaJIT), with a front end that runs the **same** rules in the browser (Ratatoskr-shaken, ShenScript-compiled). Runs standalone via `luajit examples/openresty/selftest.lua`; see [its README](openresty/README.md) to serve it. | The last three (`configc/`, `policy/`, `crdt/`) are a themed trio: each extracts diff --git a/examples/pcr/README.md b/examples/pcr/README.md index df7e1bf..f13cc36 100644 --- a/examples/pcr/README.md +++ b/examples/pcr/README.md @@ -1,102 +1,159 @@ -# Proof-carrying requests +# Proof-carrying requests, over live facts An authorization gateway where the client **carries the proof** and the edge -only **checks** it. Every request to `/protected/` presents a proof term in -`X-Proof`; the gate builds the judgment `(may SUBJECT ACTION RESOURCE)` from -the request and asks Shen's sequent-calculus typechecker whether the presented -term inhabits it. No proof that checks, no access — and every allowed request -is logged **with its proof**: the audit trail is the justification itself, -machine-checked at the moment of use. +only **checks** it — against the facts current at *this* request. Every +request to `/protected/` presents a proof term in `X-Proof`; the gate builds +the judgment `(may SUBJECT ACTION RESOURCE)` and asks Shen's sequent-calculus +typechecker whether the presented term inhabits it. Fact leaves are discharged +against a **versioned live fact store** at check time, so granting a fact +makes proofs start checking, and revoking it makes the *same proof bytes* +stop checking on the very next request — on every worker. Allowed requests +log the proof, the fact-world version, and the exact fact leaves consumed: + +``` +authorized (may carol write doc1) by [by-delegation [by-owner [fact owns alice doc1] + [fact same-tenant alice doc1]] [fact delegates alice carol]] + (50 inferences, facts v1, leaves (owns alice doc1) (same-tenant alice doc1) (delegates alice carol)) +``` ``` luajit examples/pcr/selftest.lua # everything below, off-nginx +SHEN_TYPECHECK_NATIVE=off luajit examples/pcr/selftest.lua # engine-parity leg mkdir -p examples/pcr/logs # or serve it: openresty -p "$PWD/examples/pcr" -c nginx.conf ``` -## The idea: check, don't search - -[`examples/policy/policy_proof.shen`](../policy/policy_proof.shen) shows -authorization as type inhabitation — a permission *is* a proof, checked -offline when the file loads. This example promotes that from a demonstration -to a **wire protocol**, and the move that makes it affordable at request time -is an asymmetry: +## Check, don't search — and facts are live -* **Searching** for a proof (is `(may S A R)` inhabited at all?) is the - open-ended, expensive direction. -* **Checking** a *given* term against a *given* type is bounded by the size - of the term. +Two asymmetries make this affordable and correct at request time: -So search never runs at request time. The client obtained its proof earlier — -at token issuance, from a policy service, or built from the same rules -client-side (the [`openresty/`](../openresty/) example runs Shen rules in the -browser) — and the gate's entire per-request cost is one bounded check: -the demo's deepest proof (a delegation chain) checks in **50 inferences, -~400 µs warm** on this port, several thousand checks per second per core. -That fits anywhere an LLM call, a database query, or a network hop is already -in the loop — agent/MCP tool gates, internal APIs, admin planes. +* **Checking a given term** against a given type is bounded by the term's + size; *searching* for a proof is the open-ended direction, and it never + runs at request time. The client obtained its proof earlier — the gate's + whole per-request price is one bounded check (~540 µs warm for the + delegation proof, ~1.9k checks/sec/core, parse-dominated). +* **The engine memoizes no answers.** The only caches in either engine hold + translated clause *code*, never derivations, so a fact leaf consults the + store on every check and a revoked fact **cannot** keep proving. Verified: + toggling a fact flips the same proof true/false on every toggle, under + both engines, with identical inference counts. -## Proofs compose: delegation as an audit chain - -The payoff of carrying proofs instead of booleans or bearer scopes is that -proofs **compose**. `rules.shen` has a delegation rule: +Facts stop being axioms in the rules. One rule replaces them all +(`rules.shen`): ``` -P : (may S A R); Q : (delegates S T); -===================================== -[by-delegation P Q] : (may T A R); +if (pcr.fact? Pred S R) +________________________ +[fact Pred S R] : (Pred S R); ``` -so carol's authority to write `doc1` is the *nested* term +The leaf carries its ground triple — `[fact owns alice doc1]` — because a +side condition can only **check** values, never bind them: unification of +the leaf against the client's proof term grounds `Pred`, `S`, `R` before the +guard runs (a bare-token leaf breaks under `by-delegation`, where `S` is not +in the final judgment). It also makes every leaf a self-describing audit +claim. + +## The revoke-then-deny transcript ``` -[by-delegation [by-owner [owns-fact] [alice-tenant]] [deleg-fact]] +# carol acts under alice's delegation — the nested proof is the audit chain: +$ curl -i -H 'X-Subject: carol' -H 'X-Resource: doc1' \ + -H 'X-Proof: [by-delegation [by-owner [fact owns alice doc1] [fact same-tenant alice doc1]] [fact delegates alice carol]]' \ + -X POST localhost:8093/protected/ +HTTP/1.1 200 OK X-Proof-Checked: 50 inferences X-Facts-Version: 1 + +# revoke the delegation (admin, localhost only): +$ curl -X POST localhost:8093/admin/revoke -d '{"pred":"delegates","s":"alice","r":"carol"}' +{"ok":true,"version":2} + +# the IDENTICAL bytes now fail — verified across both nginx workers, +# 30 concurrent requests, zero grace: +$ curl -i ... same request ... +HTTP/1.1 403 Forbidden +{"error":"forbidden","reason":"proof does not establish (may carol write doc1)"} + +# surgical: alice's own ownership proof still passes: +$ curl -i -H 'X-Subject: alice' ... -H 'X-Proof: [by-owner [fact owns alice doc1] [fact same-tenant alice doc1]]' ... +HTTP/1.1 200 OK + +# re-grant, and carol's original curl works again: +$ curl -X POST localhost:8093/admin/grant -d '{"pred":"delegates","s":"alice","r":"carol"}' +{"ok":true,"version":3} ``` -— readable, machine-checked provenance: carol may write **because** alice -delegated to her **and** alice owns it **and** alice is in the resource's -tenant. A bearer token says *that* you may; a proof term says *why*, and the -why is re-verified on every use. Swap the inner proof for bob's read-only one -and the chain no longer connects (`[deleg-fact]` proves `(delegates alice -carol)`, not bob) — the check fails. Run the selftest to see it. +A fact value may also be a **number** — an absolute expiry checked against +the live clock per request. A time-limited grant is then revocation with no +revoke call at all (selftest: "TTL facts"). + +## The staleness contract + +All fact state lives in **one atomically-written blob** — +`{version, synced_at, facts}` in a single `lua_shared_dict` value — decoded +into a per-worker snapshot revalidated on every request (one shm get; decode +only on change). One blob means one epoch: a check can never mix two fact +worlds, an evicted or undecodable blob is a **deny**, and `synced_at` +travels inside the blob so freshness can never be stamped by a failed sync. + +* **Demo (authoritative mode):** `/admin` writes the blob synchronously — + staleness is structurally zero; the next check anywhere sees the new + world. +* **Production (replica mode):** the store mirrors an external DB via a + periodic pull of period `W` (stub in `facts.lua`; `synced_at` is stamped + only inside a *successful* pull). A revoked fact stops authorizing within + `W`. The window is **hard-capped at 3W**: when `now − synced_at > 3W` the + gate denies everything — a partitioned DB, dead timer, or evicted blob + degrades to denial, never to frozen grants (selftest: "replica mode"). + +**New Enemy analysis** (Zanzibar's framing): variant 1 — a check against +pre-revocation facts — is bounded by `W` and cannot be extended by caching +(no derivation memoization exists). Variant 2 — an *old fact world* applied +to *new content* — is **not** closed by default: within `W`, content written +and immediately re-ACLed can be served under facts up to `W` stale relative +to that write. The named path to closing it is zookie-style: content stores +the `facts_version` at write time, and the gate requires the judgment's +version ≥ it — the numeric version already in every audit line makes that +implementable. Archiving `{version, facts}` per bump makes any logged +`(proof, judgment, version)` triple offline-replayable. ## Threat model (the proof is hostile input) -The proof term is attacker-controlled, so the gate treats it accordingly — -each line is a selftest case: - | attack | defense | |---|---| -| present someone else's proof | a proof is bound to the **exact judgment**: alice's ownership proof does not establish `(may bob write doc1)` — denied | -| smuggle a different judgment inside the proof string | `shen.typecheck` reads `"PROOF : TYPE"` as one triple and rejects any other shape — denied as malformed | -| inject syntax through subject/action/resource | judgment atoms pass a bare-symbol whitelist before the reader ever sees them — parens, brackets, colons, whitespace never reach the type | -| unreadable / unbalanced term | reader error is trapped — fail closed | -| adversarially deep term | `*maxinferences*` acts as a **per-check budget** (the helper resets the counter per call) — fail closed, next request unaffected | -| oversized term | byte cap before parsing | -| evaluate something | proofs are **read, never evaluated** — a term is syntax judged by the typechecker | - -What remains trusted: the rules file (loaded under `(tc +)` at worker start), -the ~30-line gate glue, and — for this demo — the headers standing in for an -authenticated subject. In production the subject comes from a verified -JWT/session; the *proof* is exactly where it belongs, presented by the client. - -## The two tiers compose - -This is the runtime half of a staged architecture. For decisions over a -**finite, statically known** domain, compile the policy to a certified -decision procedure at deploy time and pay nanoseconds per request (the -[`policy/`](../policy/) example's `decide` is that tier). Proof-carrying -requests are the tier for what that cannot cover: judgments over **dynamic -data** — delegation chains, per-request facts, open-ended agent tool calls — -where enumeration is impossible but checking a presented justification is -cheap, bounded, and leaves an audit artifact. +| present someone else's proof | bound to the **exact judgment**: alice's proof does not establish `(may bob write doc1)` | +| mint a fact or a grant | fact leaves pass a **predicate allowlist** (`owns`, `same-tenant`, `has-role`, `delegates`) — a leaf can never assert `(may ...)`; and the store, not the proof, decides whether the fact holds | +| smuggle a judgment inside the proof | proof tokenizer rejects unknown tokens (incl. `:`); underneath it, `shen.typecheck` reads one `"PROOF : TYPE"` triple and rejects any other shape | +| forge a store key | guard rejects any atom containing `/` (and all non-`[%w-._]` chars) before the lookup | +| intern-table exhaustion (the symbol table is permanent, ~194 B/symbol) | **nothing reaches the reader un-vetted**: subject/action/resource and every proof token must be static vocabulary or an atom of a seen fact world; a bounded distinct-atom budget backstops even a tokenizer/reader divergence — selftest sends 10k distinct hostile atoms and the heap does not grow | +| unbound-variable leaf `[fact owns X doc1]` | unbound vars reach the guard as non-strings — fail closed | +| adversarially deep / oversized terms | per-check `*maxinferences*` budget + byte cap | +| store outage mid-check | a throwing guard becomes a trapped error — deny, next request unaffected | + +**Engine parity is a tested invariant, not an assumption**: side-condition +rules MUST go through the typed `lua.function` bridge (a raw `P.F` side +condition was observed to pass the native engine and fail CPS for a +byte-identical rule); the parity selftest leg asserts identical verdicts +*and inference counts* under `SHEN_TYPECHECK_NATIVE=off`. + +Two conventions the implementation depends on: the bridge captures the +function **value** at registration, so `pcr.factq` is a stable trampoline +into mutable `facts.lua` state (never reassigned); and fact-base *reloading +as datatypes* is disqualified by measurement (hundreds of ms per reload, a +permanent per-reload leak, and a compiler wall near 200 axioms) — the +datatype compiles once, the *store* is what changes. + +What remains trusted: the rules file, `facts.lua` + the ~40-line gate glue, +and — for the demo — headers standing in for an authenticated subject +(production: a verified JWT/session; the *proof* is exactly where it +belongs, presented by the client). ## Files | file | what it is | |---|---| -| `rules.shen` | the logic: facts, grant rules, delegation — a term of `(may S A R)` is a permission | -| `app.lua` | the gateway: judgment construction, hostile-input handling, the check, the audit log | -| `selftest.lua` | every allow/deny/attack case off-nginx, plus the warm timing loop | -| `nginx.conf` | the OpenResty wiring and curl walkthrough | +| `rules.shen` | the logic: ONE live-fact rule + grant rules (owner, member-read, delegation) | +| `facts.lua` | the versioned fact store: atomic epoch blob, snapshot, TTL facts, the guard, replica-pull stub | +| `app.lua` | the gateway: pre-intern gates, judgment construction, the check, admin endpoints, the audit line | +| `selftest.lua` | allow/deny/revocation-window/TTL/staleness/hostile-input/intern cases + timing, off-nginx | +| `nginx.conf` | two workers sharing one fact blob; the curl walkthrough | diff --git a/examples/pcr/app.lua b/examples/pcr/app.lua index 11fec9e..1f81357 100644 --- a/examples/pcr/app.lua +++ b/examples/pcr/app.lua @@ -1,26 +1,32 @@ --- examples/pcr/app.lua — proof-carrying requests: the gateway CHECKS, never searches. +-- examples/pcr/app.lua — proof-carrying requests over LIVE facts. -- --- The client attaches a proof term (X-Proof) to the request. The gate builds --- the judgment (may SUBJECT ACTION RESOURCE) from the request and asks the --- kernel's sequent-calculus typechecker whether the presented term inhabits --- it. Allowed requests carry their own justification — the proof term IS the --- audit trail, and it is logged with the inference count of its checking. +-- The client attaches a proof term (X-Proof). The gate builds the judgment +-- (may SUBJECT ACTION RESOURCE) from the request and asks the kernel's +-- sequent-calculus typechecker whether the presented term inhabits it. Fact +-- leaves ([fact owns alice doc1]) are discharged against the versioned fact +-- store (facts.lua) AT CHECK TIME, so granting a fact makes proofs start +-- checking and revoking it makes the same proof bytes stop checking on the +-- next request — the engine memoizes no answers. Allowed requests log their +-- proof, the fact-store version it was judged against, and the exact fact +-- leaves consumed: the audit trail is the justification itself. -- --- The proof is UNTRUSTED input. It is read (parsed), never evaluated; the --- judgment is built only from atoms that pass a whitelist, so request data --- cannot smuggle syntax into the type; shen.typecheck reads "PROOF : TYPE" as --- one triple and rejects any other shape, so a proof string cannot smuggle a --- different judgment past the check; and a per-check inference budget makes --- adversarially deep terms fail closed. A proof is bound to the EXACT --- judgment: presenting alice's ownership proof on bob's request checks --- (may bob ...), which that term does not establish. +-- The proof is UNTRUSTED input: judgment atoms and every proof token must +-- pass allowlists BEFORE anything reaches the reader (the symbol table is +-- permanent, so unvetted atoms are a memory leak — a bounded distinct-atom +-- budget backstops even a tokenizer/reader divergence); the typecheck +-- triple shape blocks smuggling a different judgment; reader errors, +-- oversized terms and over-budget terms all fail closed. -- --- Kernel boot + the typed load of rules.shen happen ONCE per worker. +-- Boot order matters: the pcr.fact? bridge is registered BEFORE rules.shen +-- loads under (tc +) — and it is a stable trampoline into facts.lua state, +-- because lua.function captures the function VALUE at registration. local APP_DIR = debug.getinfo(1, "S").source:match("^@(.*)[/\\][^/\\]+$") or "." +package.path = APP_DIR .. "/?.lua;" .. package.path -local shen = require("shen") -local P = shen.prims +local shen = require("shen") +local P = shen.prims +local facts = require("facts") local cjson do @@ -29,37 +35,95 @@ do cjson = ok and m or assert(loadfile(APP_DIR .. "/json_shim.lua"))() end +-- the stable trampoline: registered once, reads live facts.lua state +pcr = { factq = function(pred, s, r) return facts.factq(pred, s, r) end } + shen.boot{quiet = true} +shen.eval('(lua.function pcr.fact? "pcr.factq" [symbol --> symbol --> symbol --> boolean])') shen.eval("(tc +)") P.F["load"](APP_DIR .. "/rules.shen") shen.eval("(tc -)") --- shen.typecheck resets shen.*infs* per call, so *maxinferences* acts as a --- per-check budget: a term needing more than this fails closed. The demo's --- deepest proof (delegation) checks in 50 inferences. +-- per-check inference budget (shen.typecheck resets the counter per call) shen.eval("(set shen.*maxinferences* 10000)") local MAX_PROOF_BYTES = 1024 --- Judgment atoms: bare symbols only. Anything a client could use to alter --- the shape of the type — parens, brackets, whitespace, colon, quotes — --- is refused before the reader ever sees it. +-- the demo fact base; add-if-absent so racing nginx workers seed once +facts.seed{ + ["owns/alice/doc1"] = true, + ["same-tenant/alice/doc1"] = true, + ["has-role/bob/member"] = true, + ["same-tenant/bob/doc1"] = true, + ["delegates/alice/carol"] = true, +} + +-- ---- pre-intern gates --------------------------------------------------------- +-- Nothing reaches the Shen reader unless every atom in it is already known: +-- rule names + predicates + actions (static vocabulary) or an atom of the +-- current fact world. A bounded budget of distinct admitted tokens +-- backstops any gate/reader divergence: exhaust it and the gate denies +-- everything rather than leak interned symbols forever. +local STATIC_VOCAB = { + ["fact"] = true, ["by-owner"] = true, ["by-member-read"] = true, + ["by-delegation"] = true, + ["owns"] = true, ["same-tenant"] = true, ["has-role"] = true, + ["delegates"] = true, + ["read"] = true, ["write"] = true, ["delete"] = true, ["member"] = true, +} + +local ATOM_BUDGET = 4096 +local seen_atoms, seen_count = {}, 0 + +-- The gate is an intern-DoS backstop, not authorization: an atom admitted +-- once is already interned, so admission is MONOTONE — revoking a +-- subject's last fact does not make them "unknown" here; it makes their +-- proofs fail at the type level, with the honest reason. +local function admit(token, snap) + if STATIC_VOCAB[token] or seen_atoms[token] then return true end + if not snap.atoms[token] then return false end + if seen_count >= ATOM_BUDGET then return false end + seen_count = seen_count + 1 + seen_atoms[token] = true + return true +end + local function atom_ok(s) return type(s) == "string" and s ~= "" and s:match("^[%w%-%.%_]+$") ~= nil end --- ---- check one request ------------------------------------------------------ +-- every proof token must be a known word; brackets are structure +local function proof_tokens_ok(proof, snap) + for token in proof:gmatch("[^%s%[%]]+") do + if not admit(token, snap) then return false, token end + end + return true +end + +-- ---- check one request --------------------------------------------------------- -- Returns authorized(bool), reason(string), audit(table|nil). local function check(subject, action, resource, proof) + local snap, why = facts.snapshot() + if not snap then + return false, "fact store unavailable: " .. tostring(why), nil + end if not (atom_ok(subject) and atom_ok(action) and atom_ok(resource)) then return false, "malformed subject/action/resource", nil end + if not (admit(subject, snap) and admit(action, snap) and admit(resource, snap)) then + return false, "unknown subject/action/resource", nil + end if type(proof) ~= "string" or proof == "" then return false, "no proof presented", nil end if #proof > MAX_PROOF_BYTES then return false, "proof too large", nil end + local tok_ok, bad = proof_tokens_ok(proof, snap) + if not tok_ok then + return false, "unknown token in proof: " .. tostring(bad), nil + end local judgment = "(may " .. subject .. " " .. action .. " " .. resource .. ")" + facts.reset_leaves() -- pcall: an unreadable term or a smuggled extra form errors — fail closed local ok, res = pcall(shen.typecheck, proof, judgment) if not ok then @@ -69,25 +133,47 @@ local function check(subject, action, resource, proof) return false, "proof does not establish " .. judgment, nil end return true, "proof checks", { - judgment = judgment, - proof = proof, - infs = shen.value("shen.*infs*"), + judgment = judgment, + proof = proof, + infs = shen.value("shen.*infs*"), + facts_version = snap.version, + sync_age = facts.now() - snap.synced_at, + leaves = facts.leaves(), } end --- ---- request handling (pure; shared with selftest) -------------------------- +-- ---- request handling (pure; shared with selftest) ----------------------------- local function dispatch(method, path, body) if path == "/api/check" and method == "POST" then body = body or {} local authorized, reason, audit = check(body.subject, body.action, body.resource, body.proof) local out = { authorized = authorized, reason = reason } - if audit then out.judgment, out.infs = audit.judgment, audit.infs end + if audit then + out.judgment, out.infs = audit.judgment, audit.infs + out.facts_version, out.leaves = audit.facts_version, audit.leaves + end return 200, out end + if path == "/admin/grant" and method == "POST" then + body = body or {} + if not (atom_ok(body.pred) and atom_ok(body.s) and atom_ok(body.r)) then + return 400, { error = "grant needs pred/s/r atoms" } + end + local v = facts.grant(body.pred, body.s, body.r, tonumber(body.expiry)) + return 200, { ok = true, version = v } + end + if path == "/admin/revoke" and method == "POST" then + body = body or {} + if not (atom_ok(body.pred) and atom_ok(body.s) and atom_ok(body.r)) then + return 400, { error = "revoke needs pred/s/r atoms" } + end + local v = facts.revoke(body.pred, body.s, body.r) + return 200, { ok = true, version = v } + end return 404, { error = "not found" } end -local M = { dispatch = dispatch, check = check, json = cjson } +local M = { dispatch = dispatch, check = check, json = cjson, facts = facts } function M.handle() local method = ngx.req.get_method() @@ -110,10 +196,11 @@ function M.handle() ngx.say(cjson.encode(body)) end --- ---- the enforcement gate (access_by_lua on /protected/) -------------------- +-- ---- the enforcement gate (access_by_lua on /protected/) ----------------------- -- Subject and resource come from headers for the demo; in production the --- subject comes from a verified JWT/session. The PROOF though is exactly --- where it belongs: presented by the client, per request. +-- subject comes from a verified JWT/session. The PROOF is exactly where it +-- belongs: presented by the client, per request, judged against the facts +-- current at THIS moment. function M.gate() local h = ngx.req.get_headers() local action = ngx.req.get_method() == "GET" and "read" or "write" @@ -125,10 +212,13 @@ function M.gate() ngx.say(cjson.encode({ error = "forbidden", reason = reason })) return ngx.exit(403) end - -- the audit line: who did what, justified by which proof, at what cost + -- the audit line: who did what, justified how, against which fact world ngx.log(ngx.INFO, "authorized ", audit.judgment, - " by ", audit.proof, " (", audit.infs, " inferences)") + " by ", audit.proof, + " (", audit.infs, " inferences, facts v", audit.facts_version, + ", leaves ", table.concat(audit.leaves, " "), ")") ngx.header["X-Proof-Checked"] = tostring(audit.infs) .. " inferences" + ngx.header["X-Facts-Version"] = tostring(audit.facts_version) -- fall through to the protected content end diff --git a/examples/pcr/facts.lua b/examples/pcr/facts.lua new file mode 100644 index 0000000..bbcd18a --- /dev/null +++ b/examples/pcr/facts.lua @@ -0,0 +1,183 @@ +-- examples/pcr/facts.lua — the versioned live fact store behind pcr.fact?. +-- +-- All fact state lives in ONE atomically-written blob: +-- { version = N, synced_at = T, facts = { ["owns/alice/doc1"] = true|expiry } } +-- kept in ngx.shared.pcr_facts under a single key (falling back to a plain +-- Lua cell under plain luajit, so the selftest exercises the same code). +-- One blob means one epoch: a per-check snapshot can never mix two fact +-- worlds (no torn reads), a missing/undecodable blob is a deny (no +-- fail-open on shm eviction), and synced_at travels INSIDE the blob so +-- freshness can never be stamped by a failed sync. +-- +-- A fact value of `true` holds until revoked; a NUMBER is an absolute +-- expiry (epoch seconds) checked against the live clock per request — a +-- time-limited grant that needs no revoke call. +-- +-- Modes: "authoritative" (default; the store IS the source of truth — +-- /admin writes land here synchronously, staleness is structurally zero) +-- or "replica" (the store mirrors an external DB via a periodic pull of +-- period W; snapshot() then HARD-DENIES when now - synced_at > 3W, so a +-- dead timer or partitioned DB degrades to denial, never frozen grants). +-- start_sync_timer() is the replica-mode pull stub. + +local M = {} + +local DIR = debug.getinfo(1, "S").source:match("^@(.*)[/\\][^/\\]+$") or "." + +local json +do + local ok, m = pcall(require, "cjson.safe") + if not ok then ok, m = pcall(require, "cjson") end + json = ok and m or assert(loadfile(DIR .. "/json_shim.lua"))() +end + +-- the live clock; selftest overrides M.now to drive TTL/staleness cases +function M.now() + return ngx and ngx.now() or os.time() +end + +M.mode = "authoritative" +M.W = 1 -- replica sync period (seconds); staleness hard cap = 3W + +-- ---- the blob cell ----------------------------------------------------------- +-- One key, whole-blob set/get: atomic under ngx.shared, trivial under the +-- plain-Lua fallback. LuaJIT interns strings, so the per-request "did the +-- blob change" test below is a pointer compare after the get. +local shm = ngx and ngx.shared and ngx.shared.pcr_facts +local cell = { v = nil } -- fallback store + +local function blob_get() + if shm then return shm:get("blob") end + return cell.v +end + +local function blob_set(s) + if shm then return shm:set("blob", s) end + cell.v = s; return true +end + +-- ---- writes (authority side) ------------------------------------------------- +local function decode_blob() + local raw = blob_get() + if not raw then return nil end + local ok, t = pcall(json.decode, raw) + if not ok or type(t) ~= "table" or type(t.facts) ~= "table" then return nil end + return t +end + +local function write(facts, version) + local blob = json.encode{ version = version, synced_at = M.now(), facts = facts } + blob_set(blob) + return version +end + +-- Seed only if no blob exists yet (both nginx workers race at init). +function M.seed(facts) + if blob_get() then return false end + write(facts, 1) + return true +end + +local function mutate(f) + local t = decode_blob() or { version = 0, facts = {} } + f(t.facts) + return write(t.facts, t.version + 1) +end + +function M.grant(pred, s, r, expiry) + return mutate(function(facts) facts[pred .. "/" .. s .. "/" .. r] = expiry or true end) +end + +function M.revoke(pred, s, r) + return mutate(function(facts) facts[pred .. "/" .. s .. "/" .. r] = nil end) +end + +-- ---- the per-check snapshot --------------------------------------------------- +-- snapshot() revalidates the worker-local view against the blob (one shm +-- get + string compare per request; decode only on change) and returns +-- {facts, atoms, version, synced_at} or nil, reason (DENY). The snapshot +-- and the known-atom set derived from it swap together — one epoch for +-- the guard and the request gates. +local SNAP, SNAP_RAW = nil, nil + +local function atoms_of(facts) + local atoms = {} + for key in pairs(facts) do + for part in key:gmatch("[^/]+") do atoms[part] = true end + end + return atoms +end + +function M.snapshot() + local raw = blob_get() + if not raw then return nil, "fact store empty or evicted" end + if raw ~= SNAP_RAW then + local ok, t = pcall(json.decode, raw) + if not ok or type(t) ~= "table" or type(t.facts) ~= "table" + or type(t.version) ~= "number" or type(t.synced_at) ~= "number" then + return nil, "fact store undecodable" + end + SNAP = { facts = t.facts, atoms = atoms_of(t.facts), + version = t.version, synced_at = t.synced_at } + SNAP_RAW = raw + end + if M.mode == "replica" and M.now() - SNAP.synced_at > 3 * M.W then + return nil, "fact store stale (sync older than 3W)" + end + return SNAP +end + +-- ---- the guard ---------------------------------------------------------------- +-- pcr.fact? lands here (via the stable trampoline app.lua registers — the +-- lua.function bridge captures the function VALUE at registration, so all +-- dynamism must live in the state this reads, never in rebinding it). +-- Runs DURING typechecking, so it must fail closed on everything: unbound +-- type variables arrive as tables (not strings), "/" in an atom would +-- forge a different store key, and only fact predicates are consultable — +-- a proof leaf can never assert a grant judgment like (may ...). +local PRED_ALLOW = { ["owns"] = true, ["same-tenant"] = true, + ["has-role"] = true, ["delegates"] = true } + +local LEAVES = {} + +function M.reset_leaves() LEAVES = {} end +function M.leaves() return LEAVES end + +local function atom_ok(x) + return type(x) == "string" and x ~= "" and x:match("^[%w%-%.%_]+$") ~= nil +end + +function M.factq(pred, s, r) + if not (atom_ok(pred) and atom_ok(s) and atom_ok(r)) then return false end + if not PRED_ALLOW[pred] then return false end + local snap = SNAP -- frozen view: check() took the snapshot this request + if not snap then return false end + local v = snap.facts[pred .. "/" .. s .. "/" .. r] + local held + if v == true then held = true + elseif type(v) == "number" then held = v >= M.now() -- TTL fact + else held = false end + LEAVES[#LEAVES + 1] = ("(%s %s %s)%s"):format(pred, s, r, held and "" or "!") + return held +end + +-- ---- replica-mode pull stub ---------------------------------------------------- +-- Production shape: one worker pulls {version, facts} from the source of +-- truth every W seconds and writes the blob (synced_at stamped only inside +-- a SUCCESSFUL pull — a failing pull leaves the old stamp to age toward +-- the 3W deny). `fetch` returns facts-table or nil on failure. +function M.start_sync_timer(fetch) + if not (ngx and ngx.timer) then return false end + local function pull(premature) + if premature then return end + local ok, facts = pcall(fetch) + if ok and type(facts) == "table" then + local t = decode_blob() + write(facts, ((t and t.version) or 0) + 1) + end + end + ngx.timer.every(M.W, pull) + return true +end + +return M diff --git a/examples/pcr/nginx.conf b/examples/pcr/nginx.conf index 5b2d804..aa55de1 100644 --- a/examples/pcr/nginx.conf +++ b/examples/pcr/nginx.conf @@ -1,33 +1,35 @@ -# examples/pcr/nginx.conf — proof-carrying requests on OpenResty. +# examples/pcr/nginx.conf — proof-carrying requests over LIVE facts. # # mkdir -p examples/pcr/logs # openresty -p "$PWD/examples/pcr" -c nginx.conf # -# The client carries the proof; the gate only CHECKS it (never searches). -# -# # allowed — alice owns doc1, and her proof says so: -# curl -i -H 'X-Subject: alice' -H 'X-Resource: doc1' \ -# -H 'X-Proof: [by-owner [owns-fact] [alice-tenant]]' \ -# -X POST localhost:8093/protected/ +# The client carries the proof; the gate CHECKS it against the fact world +# current at this request. Two workers share one versioned fact blob +# (lua_shared_dict), so a revoke through either worker is seen by both. # # # allowed — carol acts under alice's delegation; the nested proof is the # # whole audit chain (carol may write BECAUSE alice delegated AND alice owns): # curl -i -H 'X-Subject: carol' -H 'X-Resource: doc1' \ -# -H 'X-Proof: [by-delegation [by-owner [owns-fact] [alice-tenant]] [deleg-fact]]' \ +# -H 'X-Proof: [by-delegation [by-owner [fact owns alice doc1] [fact same-tenant alice doc1]] [fact delegates alice carol]]' \ # -X POST localhost:8093/protected/ # -# # denied — bob presents ALICE's proof: it does not establish (may bob write doc1): -# curl -i -H 'X-Subject: bob' -H 'X-Resource: doc1' \ -# -H 'X-Proof: [by-owner [owns-fact] [alice-tenant]]' \ +# # revoke the delegation (admin, localhost only): +# curl -X POST localhost:8093/admin/revoke \ +# -d '{"pred":"delegates","s":"alice","r":"carol"}' +# +# # the IDENTICAL proof now fails — on every worker, on the next request: +# # 403 {"error":"forbidden","reason":"proof does not establish (may carol write doc1)"} +# # ...while alice's own ownership proof still passes (surgical revocation): +# curl -i -H 'X-Subject: alice' -H 'X-Resource: doc1' \ +# -H 'X-Proof: [by-owner [fact owns alice doc1] [fact same-tenant alice doc1]]' \ # -X POST localhost:8093/protected/ # -# # denied — bob's member proof grants read, and GET asks read, so this passes: -# curl -i -H 'X-Subject: bob' -H 'X-Resource: doc1' \ -# -H 'X-Proof: [by-member-read [member-fact] [tenant-fact]]' \ -# localhost:8093/protected/ +# # re-grant and carol's original curl works again: +# curl -X POST localhost:8093/admin/grant \ +# -d '{"pred":"delegates","s":"alice","r":"carol"}' daemon off; -worker_processes 1; +worker_processes 2; # exercise cross-worker fact propagation pid logs/nginx.pid; error_log logs/error.log info; # the proof audit lines land here @@ -36,6 +38,8 @@ events { worker_connections 256; } http { access_log logs/access.log; + lua_shared_dict pcr_facts 4m; # the ONE versioned fact blob + types { application/json json; text/plain shen; @@ -47,7 +51,7 @@ http { package.path = prefix .. "../../?.lua;" .. prefix .. "?.lua;" .. package.path } - # boot Shen + typed load once per worker + # boot Shen + typed load + seed the fact blob (add-if-absent) per worker init_worker_by_lua_block { require("app") } server { @@ -58,11 +62,19 @@ http { content_by_lua_block { require("app").handle() } } + # the authority endpoints: grant/revoke facts (demo: localhost only) + location /admin/ { + allow 127.0.0.1; + allow ::1; + deny all; + content_by_lua_block { require("app").handle() } + } + # the enforcement gate: the proof is checked BEFORE the content runs location /protected/ { access_by_lua_block { require("app").gate() } content_by_lua_block { ngx.header.content_type = "application/json" - ngx.say('{"ok":true,"secret":"the protected resource"}') } + ngx.say('{"ok":true,"secret":"the protected resource","worker":' .. ngx.worker.pid() .. '}') } } # serve the logic itself (one source of truth) diff --git a/examples/pcr/rules.shen b/examples/pcr/rules.shen index 1049d50..366f8e3 100644 --- a/examples/pcr/rules.shen +++ b/examples/pcr/rules.shen @@ -3,32 +3,31 @@ \\ A term of type (may S A R) is a PROOF that subject S may perform action A on \\ resource R. The gateway never SEARCHES for such a term — the client carries \\ one with the request (X-Proof), and the gateway merely CHECKS it against the -\\ judgment built from the request. Checking a given term is bounded by the -\\ term's size; search is the expensive, open-ended direction, and it never -\\ runs at request time. +\\ judgment built from the request. \\ -\\ Same logic as examples/policy/policy_proof.shen, promoted from an offline -\\ demonstration to the wire protocol — plus a delegation rule, because the -\\ payoff of carrying PROOFS instead of booleans is that proofs COMPOSE: a -\\ delegated permission is a nested term whose subterms are the entire audit -\\ chain of *why*. +\\ FACTS ARE LIVE. There are no fact axioms in this file: a fact leaf is a +\\ self-describing claim — [fact owns alice doc1] — discharged by the single +\\ side-condition rule below, which consults the gateway's versioned fact +\\ store (facts.lua, via the typed pcr.fact? bridge) AT PROOF-CHECK TIME. +\\ Grant a fact and proofs using it start checking; revoke it and the same +\\ proof bytes stop checking on the very next request — the engine memoizes +\\ no answers, so revocation has zero staleness at the checker. +\\ +\\ The leaf carries its ground triple (Pred S R) because a side condition can +\\ only CHECK values, never BIND them: unification of the leaf against the +\\ client's proof term grounds Pred, S and R before the guard runs, which +\\ keeps rules like by-delegation (where S is not in the final judgment) +\\ working. It also makes every leaf readable in the audit log. +\\ +\\ pcr.fact? must be registered (lua.function, app.lua) BEFORE this file is +\\ loaded under (tc +). The guard allows only the fact predicates below — +\\ a leaf can never assert a grant judgment like (may ...) directly. (datatype authz - \\ -- environment facts (axioms; a directory or DB would supply these) ------ - ______________________________ - [owns-fact] : (owns alice doc1); - - ______________________________________ - [alice-tenant] : (same-tenant alice doc1); - - _________________________________ - [member-fact] : (has-role bob member); - - ____________________________________ - [tenant-fact] : (same-tenant bob doc1); - - ______________________________________ - [deleg-fact] : (delegates alice carol); + \\ -- the ONE fact rule: a leaf is checked against the live store ---------- + if (pcr.fact? Pred S R) + ________________________ + [fact Pred S R] : (Pred S R); \\ -- grant rules (universal in S, A, R, T) --------------------------------- \\ an owner inside the resource's tenant may take ANY action on it diff --git a/examples/pcr/selftest.lua b/examples/pcr/selftest.lua index 7d1148b..64a7e0e 100644 --- a/examples/pcr/selftest.lua +++ b/examples/pcr/selftest.lua @@ -1,66 +1,145 @@ --- examples/pcr/selftest.lua — verify the proof-carrying-request gateway off-nginx. +-- examples/pcr/selftest.lua — verify the live-facts proof-carrying gateway off-nginx. -- --- luajit examples/pcr/selftest.lua (from the repo root) +-- luajit examples/pcr/selftest.lua (native engine) +-- SHEN_TYPECHECK_NATIVE=off luajit examples/pcr/selftest.lua (parity leg) -- --- Drives the SAME check() the edge gate uses: the allow cases (including a --- nested delegation proof), every category of denial — no proof, wrong rule, --- a spoofed proof bound to someone else's judgment, judgment injection, proof --- smuggling, oversized and over-budget terms — and a warm timing loop. --- No nginx, no network. +-- Drives the SAME check() the edge gate uses (pure-Lua fact store fallback): +-- the allow cases, the REVOCATION WINDOW (grant/revoke flips take effect on +-- the immediately-next check, surgically), TTL facts, replica-mode staleness +-- hard cap, every category of hostile-input denial, an intern-growth +-- regression, and a warm timing loop. The parity leg must print IDENTICAL +-- verdicts and inference counts — that is the only guard against +-- side-condition rules silently diverging between the two engines. local root = arg[0]:match("^(.*)/examples/pcr/[^/]+$") or "." package.path = root .. "/?.lua;" .. root .. "/examples/pcr/?.lua;" .. package.path -local app = require("app") -local shen = require("shen") +local app = require("app") +local facts = app.facts +local shen = require("shen") local fail = 0 local function expect(label, want, subject, action, resource, proof) local authorized, reason = app.check(subject, action, resource, proof) - io.write((" %-28s %-5s %s\n"):format(label, authorized and "ALLOW" or "DENY", reason)) + io.write((" %-30s %-5s infs=%-4d %s\n"):format(label, + authorized and "ALLOW" or "DENY", shen.value("shen.*infs*"), reason)) if authorized ~= want then fail = fail + 1; print(" FAIL: expected " .. tostring(want)) end end -local owner_proof = "[by-owner [owns-fact] [alice-tenant]]" -local member_proof = "[by-member-read [member-fact] [tenant-fact]]" -local deleg_proof = "[by-delegation " .. owner_proof .. " [deleg-fact]]" +local owner_proof = "[by-owner [fact owns alice doc1] [fact same-tenant alice doc1]]" +local member_proof = "[by-member-read [fact has-role bob member] [fact same-tenant bob doc1]]" +local deleg_proof = "[by-delegation " .. owner_proof .. " [fact delegates alice carol]]" -print("== proofs that check ==") +print("== proofs that check against the live fact world ==") expect("owner writes", true, "alice", "write", "doc1", owner_proof) expect("same proof, any action", true, "alice", "delete", "doc1", owner_proof) expect("member reads", true, "bob", "read", "doc1", member_proof) expect("delegate writes", true, "carol", "write", "doc1", deleg_proof) +print("\n== the revocation window: identical bytes, next check ==") +for round = 1, 3 do + facts.revoke("delegates", "alice", "carol") + expect("revoked -> deny (round " .. round .. ")", false, "carol", "write", "doc1", deleg_proof) + expect("...surgical: owner unaffected", true, "alice", "write", "doc1", owner_proof) + facts.grant("delegates", "alice", "carol") + expect("re-granted -> allow", true, "carol", "write", "doc1", deleg_proof) +end +facts.revoke("owns", "alice", "doc1") +expect("revoke root fact", false, "alice", "write", "doc1", owner_proof) +expect("...kills chains on it", false, "carol", "write", "doc1", deleg_proof) +facts.grant("owns", "alice", "doc1") +expect("restore root fact", true, "alice", "write", "doc1", owner_proof) + +print("\n== TTL facts: expiry is revocation with no revoke call ==") +local real_now = facts.now +facts.grant("delegates", "alice", "dave", real_now() + 3600) +expect("TTL fact within expiry", true, "dave", "write", "doc1", + "[by-delegation " .. owner_proof .. " [fact delegates alice dave]]") +facts.now = function() return real_now() + 7200 end -- clock passes expiry +expect("TTL fact expired", false, "dave", "write", "doc1", + "[by-delegation " .. owner_proof .. " [fact delegates alice dave]]") +facts.now = real_now +facts.revoke("delegates", "alice", "dave") + +print("\n== replica mode: staleness hard cap fails closed ==") +facts.mode = "replica" +expect("fresh replica allows", true, "alice", "write", "doc1", owner_proof) +facts.now = function() return real_now() + 3 * facts.W + 1 end -- sync ages past 3W +expect("stale replica denies all",false, "alice", "write", "doc1", owner_proof) +facts.now = real_now +expect("recovers when fresh", true, "alice", "write", "doc1", owner_proof) +facts.mode = "authoritative" + print("\n== denials: the proof is bound to the exact judgment ==") expect("read proof, delete asked", false, "bob", "delete", "doc1", member_proof) expect("spoof: alice's proof, bob", false, "bob", "write", "doc1", owner_proof) expect("delegation chain broken", false, "carol", "read", "doc1", - "[by-delegation " .. member_proof .. " [deleg-fact]]") + "[by-delegation " .. member_proof .. " [fact delegates alice carol]]") +expect("leaf asserts a grant", false, "carol", "write", "doc1", + "[fact may carol write doc1]") -- pred allowlist: facts can't mint (may ...) print("\n== denials: hostile input fails closed ==") -expect("no proof", false, "alice", "write", "doc1", nil) -expect("unreadable proof", false, "alice", "write", "doc1", "[by-owner [owns-fact") -expect("smuggled judgment", false, "bob", "delete", "doc1", - member_proof .. " : (may bob read doc1)") -- extra forms: shape check trips -expect("judgment injection", false, "doc1) (may bob delete doc1", "write", "doc1", owner_proof) -expect("oversized proof", false, "alice", "write", "doc1", - "[by-owner " .. string.rep("[owns-fact] ", 200) .. "]") - --- a term needing more inferences than the budget fails closed, and the next --- check recovers (shen.typecheck resets the counter per call) +expect("no proof", false, "alice", "write", "doc1", nil) +expect("unreadable proof", false, "alice", "write", "doc1", "[by-owner [fact owns alice") +expect("smuggled judgment", false, "bob", "delete", "doc1", + member_proof .. " : (may bob read doc1)") +expect("judgment injection", false, "doc1) (may bob delete doc1", "write", "doc1", owner_proof) +expect("unknown subject", false, "mallory", "write", "doc1", owner_proof) +expect("unknown proof token", false, "alice", "write", "doc1", + "[by-owner [fact owns mallory doc1] [fact same-tenant alice doc1]]") +expect("oversized proof", false, "alice", "write", "doc1", + "[by-owner " .. string.rep("[fact owns alice doc1] ", 60) .. "]") +expect("unbound-var leaf", false, "alice", "write", "doc1", + "[by-owner [fact owns X doc1] [fact same-tenant alice doc1]]") + +-- a throwing fact store denies, and the next check recovers +local real_factq = facts.factq +facts.factq = function() error("db down") end +expect("store throws -> deny", false, "alice", "write", "doc1", owner_proof) +facts.factq = real_factq +expect("recovers after throw", true, "alice", "write", "doc1", owner_proof) + +-- a term needing more inferences than the budget fails closed, then recovers local prev_max = shen.value("shen.*maxinferences*") shen.eval("(set shen.*maxinferences* 1)") -expect("over budget", false, "alice", "write", "doc1", owner_proof) +expect("over budget", false, "alice", "write", "doc1", owner_proof) shen.eval("(set shen.*maxinferences* " .. tostring(prev_max) .. ")") -expect("recovers after budget", true, "alice", "write", "doc1", owner_proof) +expect("recovers after budget",true, "alice", "write", "doc1", owner_proof) + +print("\n== the guard itself (defense under the tokenizer) ==") +local function guard(label, want, ...) + local got = facts.factq(...) + io.write((" %-30s %s\n"):format(label, got == want and "ok" or "FAIL")) + if got ~= want then fail = fail + 1 end +end +facts.snapshot() -- ensure the guard's view is current +guard("held fact", true, "owns", "alice", "doc1") +guard("grant pred refused", false, "may", "carol", "doc1") -- PRED_ALLOW +guard("slash injection", false, "owns", "alice/doc1", "x") -- key forgery +guard("non-string (pvar)", false, "owns", {}, "doc1") -- unbound var +guard("empty atom", false, "owns", "", "doc1") + +print("\n== intern regression: distinct hostile atoms stay bounded ==") +collectgarbage("collect"); collectgarbage("collect") +local kb0 = collectgarbage("count") +local denied = 0 +for i = 1, 10000 do + local a = app.check("intruder" .. i, "write", "doc1", owner_proof) + if not a then denied = denied + 1 end +end +collectgarbage("collect"); collectgarbage("collect") +local grew = collectgarbage("count") - kb0 +io.write((" 10k distinct-atom requests: %d denied, heap %+.0f KB\n"):format(denied, grew)) +if denied ~= 10000 then fail = fail + 1; print(" FAIL: hostile atoms must all deny") end +if grew > 512 then fail = fail + 1; print(" FAIL: heap grew > 512 KB — atoms are leaking past the gate") end -print("\n== warm cost of checking (this is the whole per-request price) ==") -for _ = 1, 200 do app.check("carol", "write", "doc1", deleg_proof) end -- warmup +print("\n== warm cost of checking (the whole per-request price) ==") +for _ = 1, 200 do app.check("carol", "write", "doc1", deleg_proof) end local N = 2000 local t0 = os.clock() for _ = 1, N do app.check("carol", "write", "doc1", deleg_proof) end local us = (os.clock() - t0) * 1e6 / N -io.write((" nested delegation proof: %.0f us/check (%d inferences), ~%d checks/sec/core\n") +io.write((" nested delegation vs live facts: %.0f us/check (%d inferences), ~%d checks/sec/core\n") :format(us, shen.value("shen.*infs*"), math.floor(1e6 / us))) if fail == 0 then print("\nOK — all checks passed") From 80f4e3c8285bcaa354655fad6653d86b60be0095 Mon Sep 17 00:00:00 2001 From: Reuben Brooks Date: Mon, 6 Jul 2026 14:43:29 -0500 Subject: [PATCH 4/6] =?UTF-8?q?examples/pcr:=20address=20PR=20review=20?= =?UTF-8?q?=E2=80=94=20variable-injection=20+=20silent=20write=20failures?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two blocking findings from review, both with regression tests: 1. Uppercase atoms parse as Shen TYPE VARIABLES: an uppercase subject/ action/resource admitted through the fact world turned the judgment into a wildcard — (may S write doc1) is universally quantified, so alice's proof authorized it. Atoms are now lowercase-leading (^[a-z][a-z0-9-._]*$) at all three layers: the request gate, the proof-token admit, and the factq guard itself, so an uppercase atom cannot enter the judgment, the proof, or a store lookup even if it is smuggled into the fact world directly. Tests grant uppercase atoms into the store and assert every path still denies. 2. Fact-store writes could fail silently: blob_set ignored the ngx.shared set() result, so a failed revoke under shared-dict pressure reported {ok:true} while the old blob kept authorizing. Write failures now propagate through blob_set -> write -> grant/ revoke/seed and the sync timer (logged), and the admin endpoints return 507 with the reason. Tests simulate write failure and assert: failed revoke keeps the grant effective AND reports failure, failed grant stays absent, the fact version never advances on a failed write, and both paths recover. Also merged origin/main (new openresty-authz example) resolving the .gitignore conflict in favor of the generalized examples/*/logs/ + nginx temp-dir patterns, which subsume main's per-example entries. Selftest green under both engines with byte-identical verdicts and inference counts; make test 471/471. Co-Authored-By: Claude Fable 5 --- examples/pcr/README.md | 14 ++++++---- examples/pcr/app.lua | 19 +++++++++----- examples/pcr/facts.lua | 27 ++++++++++++++----- examples/pcr/selftest.lua | 55 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 97 insertions(+), 18 deletions(-) diff --git a/examples/pcr/README.md b/examples/pcr/README.md index f13cc36..4fb86a7 100644 --- a/examples/pcr/README.md +++ b/examples/pcr/README.md @@ -98,13 +98,16 @@ travels inside the blob so freshness can never be stamped by a failed sync. * **Demo (authoritative mode):** `/admin` writes the blob synchronously — staleness is structurally zero; the next check anywhere sees the new - world. + world. Grant/revoke endpoints return success only after the blob write + succeeds; shared-dict pressure or another persistence failure returns a + non-200 JSON error and leaves the previous fact world in force. * **Production (replica mode):** the store mirrors an external DB via a periodic pull of period `W` (stub in `facts.lua`; `synced_at` is stamped - only inside a *successful* pull). A revoked fact stops authorizing within - `W`. The window is **hard-capped at 3W**: when `now − synced_at > 3W` the - gate denies everything — a partitioned DB, dead timer, or evicted blob - degrades to denial, never to frozen grants (selftest: "replica mode"). + only inside a *successful* pull and successful blob write). A revoked fact + stops authorizing within `W`. The window is **hard-capped at 3W**: when + `now − synced_at > 3W` the gate denies everything — a partitioned DB, dead + timer, failed write, or evicted blob degrades to denial, never to frozen + grants (selftest: "replica mode"). **New Enemy analysis** (Zanzibar's framing): variant 1 — a check against pre-revocation facts — is bounded by `W` and cannot be extended by caching @@ -125,6 +128,7 @@ implementable. Archiving `{version, facts}` per bump makes any logged | mint a fact or a grant | fact leaves pass a **predicate allowlist** (`owns`, `same-tenant`, `has-role`, `delegates`) — a leaf can never assert `(may ...)`; and the store, not the proof, decides whether the fact holds | | smuggle a judgment inside the proof | proof tokenizer rejects unknown tokens (incl. `:`); underneath it, `shen.typecheck` reads one `"PROOF : TYPE"` triple and rejects any other shape | | forge a store key | guard rejects any atom containing `/` (and all non-`[%w-._]` chars) before the lookup | +| smuggle Shen type variables as data | external atoms must be lowercase-starting (`[a-z][a-z0-9-._]*`); uppercase `S`/`A`/`R` are rejected even if they appear in the fact world | | intern-table exhaustion (the symbol table is permanent, ~194 B/symbol) | **nothing reaches the reader un-vetted**: subject/action/resource and every proof token must be static vocabulary or an atom of a seen fact world; a bounded distinct-atom budget backstops even a tokenizer/reader divergence — selftest sends 10k distinct hostile atoms and the heap does not grow | | unbound-variable leaf `[fact owns X doc1]` | unbound vars reach the guard as non-strings — fail closed | | adversarially deep / oversized terms | per-check `*maxinferences*` budget + byte cap | diff --git a/examples/pcr/app.lua b/examples/pcr/app.lua index 1f81357..6805285 100644 --- a/examples/pcr/app.lua +++ b/examples/pcr/app.lua @@ -74,11 +74,16 @@ local STATIC_VOCAB = { local ATOM_BUDGET = 4096 local seen_atoms, seen_count = {}, 0 +local function atom_ok(s) + return type(s) == "string" and s ~= "" and s:match("^[a-z][a-z0-9%-%.%_]*$") ~= nil +end + -- The gate is an intern-DoS backstop, not authorization: an atom admitted -- once is already interned, so admission is MONOTONE — revoking a -- subject's last fact does not make them "unknown" here; it makes their -- proofs fail at the type level, with the honest reason. local function admit(token, snap) + if not atom_ok(token) then return false end if STATIC_VOCAB[token] or seen_atoms[token] then return true end if not snap.atoms[token] then return false end if seen_count >= ATOM_BUDGET then return false end @@ -87,10 +92,6 @@ local function admit(token, snap) return true end -local function atom_ok(s) - return type(s) == "string" and s ~= "" and s:match("^[%w%-%.%_]+$") ~= nil -end - -- every proof token must be a known word; brackets are structure local function proof_tokens_ok(proof, snap) for token in proof:gmatch("[^%s%[%]]+") do @@ -159,7 +160,10 @@ local function dispatch(method, path, body) if not (atom_ok(body.pred) and atom_ok(body.s) and atom_ok(body.r)) then return 400, { error = "grant needs pred/s/r atoms" } end - local v = facts.grant(body.pred, body.s, body.r, tonumber(body.expiry)) + local ok, v, err = facts.grant(body.pred, body.s, body.r, tonumber(body.expiry)) + if not ok then + return 507, { ok = false, error = "grant failed", reason = err } + end return 200, { ok = true, version = v } end if path == "/admin/revoke" and method == "POST" then @@ -167,7 +171,10 @@ local function dispatch(method, path, body) if not (atom_ok(body.pred) and atom_ok(body.s) and atom_ok(body.r)) then return 400, { error = "revoke needs pred/s/r atoms" } end - local v = facts.revoke(body.pred, body.s, body.r) + local ok, v, err = facts.revoke(body.pred, body.s, body.r) + if not ok then + return 507, { ok = false, error = "revoke failed", reason = err } + end return 200, { ok = true, version = v } end return 404, { error = "not found" } diff --git a/examples/pcr/facts.lua b/examples/pcr/facts.lua index bbcd18a..cb71f73 100644 --- a/examples/pcr/facts.lua +++ b/examples/pcr/facts.lua @@ -45,6 +45,7 @@ M.W = 1 -- replica sync period (seconds); staleness hard cap = 3W -- blob change" test below is a pointer compare after the get. local shm = ngx and ngx.shared and ngx.shared.pcr_facts local cell = { v = nil } -- fallback store +M._simulate_write_failure = nil -- selftest hook; normal plain-Lua fallback still succeeds local function blob_get() if shm then return shm:get("blob") end @@ -52,7 +53,12 @@ local function blob_get() end local function blob_set(s) - if shm then return shm:set("blob", s) end + if M._simulate_write_failure then return false, M._simulate_write_failure end + if shm then + local ok, err = shm:set("blob", s) + if not ok then return false, err or "unknown shared-dict set failure" end + return true + end cell.v = s; return true end @@ -67,15 +73,17 @@ end local function write(facts, version) local blob = json.encode{ version = version, synced_at = M.now(), facts = facts } - blob_set(blob) - return version + local ok, err = blob_set(blob) + if not ok then + return false, nil, "fact store write failed: " .. tostring(err) + end + return true, version end -- Seed only if no blob exists yet (both nginx workers race at init). function M.seed(facts) if blob_get() then return false end - write(facts, 1) - return true + return write(facts, 1) end local function mutate(f) @@ -144,7 +152,7 @@ function M.reset_leaves() LEAVES = {} end function M.leaves() return LEAVES end local function atom_ok(x) - return type(x) == "string" and x ~= "" and x:match("^[%w%-%.%_]+$") ~= nil + return type(x) == "string" and x ~= "" and x:match("^[a-z][a-z0-9%-%.%_]*$") ~= nil end function M.factq(pred, s, r) @@ -173,7 +181,12 @@ function M.start_sync_timer(fetch) local ok, facts = pcall(fetch) if ok and type(facts) == "table" then local t = decode_blob() - write(facts, ((t and t.version) or 0) + 1) + local wrote, _, err = write(facts, ((t and t.version) or 0) + 1) + if not wrote then + ngx.log(ngx.ERR, err) + end + elseif not ok then + ngx.log(ngx.ERR, "pcr fact sync fetch failed: ", tostring(facts)) end end ngx.timer.every(M.W, pull) diff --git a/examples/pcr/selftest.lua b/examples/pcr/selftest.lua index 64a7e0e..54ac9bf 100644 --- a/examples/pcr/selftest.lua +++ b/examples/pcr/selftest.lua @@ -26,6 +26,22 @@ local function expect(label, want, subject, action, resource, proof) if authorized ~= want then fail = fail + 1; print(" FAIL: expected " .. tostring(want)) end end +local function expect_admin(label, want_ok, path, body) + local status, out = app.dispatch("POST", path, body) + io.write((" %-30s HTTP %-3d %s\n"):format(label, status, out.reason or out.error or "ok")) + local matched + if want_ok then + matched = status == 200 and out.ok == true + else + matched = status ~= 200 and out.ok == false + end + if not matched then + fail = fail + 1 + print((" FAIL: expected admin ok=%s"):format(tostring(want_ok))) + end + return status, out +end + local owner_proof = "[by-owner [fact owns alice doc1] [fact same-tenant alice doc1]]" local member_proof = "[by-member-read [fact has-role bob member] [fact same-tenant bob doc1]]" local deleg_proof = "[by-delegation " .. owner_proof .. " [fact delegates alice carol]]" @@ -50,6 +66,37 @@ expect("...kills chains on it", false, "carol", "write", "doc1", deleg_proof) facts.grant("owns", "alice", "doc1") expect("restore root fact", true, "alice", "write", "doc1", owner_proof) +print("\n== fact-store write failures fail closed ==") +local before = facts.snapshot() +local before_version = before.version +facts._simulate_write_failure = "simulated shared-dict full" +expect_admin("failed revoke reports", false, "/admin/revoke", + { pred = "delegates", s = "alice", r = "carol" }) +expect("failed revoke keeps grant", true, "carol", "write", "doc1", deleg_proof) +local after = facts.snapshot() +if after.version ~= before_version then + fail = fail + 1 + print(" FAIL: failed revoke advanced fact version") +end + +local erin_proof = "[by-delegation " .. owner_proof .. " [fact delegates alice erin]]" +expect_admin("failed grant reports", false, "/admin/grant", + { pred = "delegates", s = "alice", r = "erin" }) +expect("failed grant stays absent", false, "erin", "write", "doc1", erin_proof) +after = facts.snapshot() +if after.version ~= before_version then + fail = fail + 1 + print(" FAIL: failed grant advanced fact version") +end + +facts._simulate_write_failure = nil +expect_admin("grant recovers", true, "/admin/grant", + { pred = "delegates", s = "alice", r = "erin" }) +expect("recovered grant allows", true, "erin", "write", "doc1", erin_proof) +expect_admin("revoke recovers", true, "/admin/revoke", + { pred = "delegates", s = "alice", r = "erin" }) +expect("recovered revoke denies", false, "erin", "write", "doc1", erin_proof) + print("\n== TTL facts: expiry is revocation with no revoke call ==") local real_now = facts.now facts.grant("delegates", "alice", "dave", real_now() + 3600) @@ -91,6 +138,14 @@ expect("oversized proof", false, "alice", "write", "doc1", "[by-owner " .. string.rep("[fact owns alice doc1] ", 60) .. "]") expect("unbound-var leaf", false, "alice", "write", "doc1", "[by-owner [fact owns X doc1] [fact same-tenant alice doc1]]") +facts.grant("owns", "S", "doc1") -- admit uppercase atoms into the fact world first +facts.grant("owns", "alice", "R") -- the request gate must still reject them +facts.grant("owns", "alice", "A") -- because Shen would read them as type variables +expect("uppercase subject", false, "S", "write", "doc1", owner_proof) +expect("uppercase action", false, "alice", "A", "doc1", owner_proof) +expect("uppercase resource", false, "alice", "write", "R", owner_proof) +expect("uppercase proof atom",false, "alice", "write", "doc1", + "[by-owner [fact owns S doc1] [fact same-tenant alice doc1]]") -- a throwing fact store denies, and the next check recovers local real_factq = facts.factq From 5eefbf8dce98580640514241dab0a0084836b583 Mon Sep 17 00:00:00 2001 From: Reuben Brooks Date: Mon, 6 Jul 2026 17:29:14 -0500 Subject: [PATCH 5/6] examples/pcr: address review findings A & B + header/test-seam hygiene MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A. mutate() no longer heals an undecodable blob into a fresh 1-fact world. decode_blob distinguishes an ABSENT blob (first write, version 1) from a PRESENT-but-undecodable one; the latter is refused and surfaced as a 507 at the admin API, matching snapshot()'s existing deny-on-undecodable. A corrupt blob could otherwise wipe every fact and rewind the monotonic version the audit trail depends on. Regression: corrupt the blob, assert reads deny AND a grant refuses (507) rather than resetting. B. admit() is now stateless: atom_ok and (static vocab or in the current fact world). The old per-worker monotone seen-set capped at 4096 never bounded the attacker (fact-world membership already does — attacker atoms are rejected before read-from-string) but DID false-deny legitimate atoms once a worker had handled >4096 distinct principals, a fail-closed availability bug at scale. A principal with no current facts now denies at the gate; to keep the honest type-layer reason for the demo, carol is seeded a benign same-tenant membership so revoking her delegation denies with "proof does not establish", not "unknown subject". Regression: expect_reason asserts the type-layer reason survives revocation. Minor: the inference-count response header (X-Proof-Checked) is internal detail, now gated behind PCR_DEBUG_HEADERS (env directive added to nginx.conf so it works under OpenResty); X-Facts-Version stays (it is the consistency token clients legitimately use). The write-failure test seam is consolidated under facts._test alongside new corrupt_blob/clear injectors, clearly marked not-public-API. Selftest green under both engines with byte-identical verdicts and infs; make test 471/471; live demo unchanged (honest revocation reason preserved). Co-Authored-By: Claude Fable 5 --- examples/pcr/README.md | 5 +++-- examples/pcr/app.lua | 46 ++++++++++++++++++++++----------------- examples/pcr/facts.lua | 46 ++++++++++++++++++++++++++++++++++----- examples/pcr/nginx.conf | 1 + examples/pcr/selftest.lua | 41 ++++++++++++++++++++++++++++++++-- 5 files changed, 109 insertions(+), 30 deletions(-) diff --git a/examples/pcr/README.md b/examples/pcr/README.md index 4fb86a7..3379c34 100644 --- a/examples/pcr/README.md +++ b/examples/pcr/README.md @@ -62,7 +62,8 @@ claim. $ curl -i -H 'X-Subject: carol' -H 'X-Resource: doc1' \ -H 'X-Proof: [by-delegation [by-owner [fact owns alice doc1] [fact same-tenant alice doc1]] [fact delegates alice carol]]' \ -X POST localhost:8093/protected/ -HTTP/1.1 200 OK X-Proof-Checked: 50 inferences X-Facts-Version: 1 +HTTP/1.1 200 OK X-Facts-Version: 1 +# (start with PCR_DEBUG_HEADERS=1 to also get X-Proof-Checked: 50 inferences) # revoke the delegation (admin, localhost only): $ curl -X POST localhost:8093/admin/revoke -d '{"pred":"delegates","s":"alice","r":"carol"}' @@ -129,7 +130,7 @@ implementable. Archiving `{version, facts}` per bump makes any logged | smuggle a judgment inside the proof | proof tokenizer rejects unknown tokens (incl. `:`); underneath it, `shen.typecheck` reads one `"PROOF : TYPE"` triple and rejects any other shape | | forge a store key | guard rejects any atom containing `/` (and all non-`[%w-._]` chars) before the lookup | | smuggle Shen type variables as data | external atoms must be lowercase-starting (`[a-z][a-z0-9-._]*`); uppercase `S`/`A`/`R` are rejected even if they appear in the fact world | -| intern-table exhaustion (the symbol table is permanent, ~194 B/symbol) | **nothing reaches the reader un-vetted**: subject/action/resource and every proof token must be static vocabulary or an atom of a seen fact world; a bounded distinct-atom budget backstops even a tokenizer/reader divergence — selftest sends 10k distinct hostile atoms and the heap does not grow | +| intern-table exhaustion (the symbol table is permanent, ~194 B/symbol) | **nothing reaches the reader un-vetted**: subject/action/resource and every proof token must be static vocabulary or an atom of the current fact world. The fact world is written only by admin grants, so the admissible-atom set is operator-controlled — an attacker's novel atoms are rejected before `read-from-string`. Selftest sends 10k distinct hostile atoms and the heap does not grow. | | unbound-variable leaf `[fact owns X doc1]` | unbound vars reach the guard as non-strings — fail closed | | adversarially deep / oversized terms | per-check `*maxinferences*` budget + byte cap | | store outage mid-check | a throwing guard becomes a trapped error — deny, next request unaffected | diff --git a/examples/pcr/app.lua b/examples/pcr/app.lua index 6805285..895e091 100644 --- a/examples/pcr/app.lua +++ b/examples/pcr/app.lua @@ -47,22 +47,29 @@ shen.eval("(tc -)") -- per-check inference budget (shen.typecheck resets the counter per call) shen.eval("(set shen.*maxinferences* 10000)") local MAX_PROOF_BYTES = 1024 +local DEBUG_HEADERS = os.getenv("PCR_DEBUG_HEADERS") == "1" --- the demo fact base; add-if-absent so racing nginx workers seed once +-- the demo fact base; add-if-absent so racing nginx workers seed once. +-- carol is a known tenant member (same-tenant) but owns nothing and has no +-- role — her only WRITE capability comes from alice's delegation, so revoking +-- that delegation denies her at the TYPE layer ("proof does not establish"), +-- honestly, while she stays a known atom. facts.seed{ ["owns/alice/doc1"] = true, ["same-tenant/alice/doc1"] = true, ["has-role/bob/member"] = true, ["same-tenant/bob/doc1"] = true, ["delegates/alice/carol"] = true, + ["same-tenant/carol/doc1"] = true, } --- ---- pre-intern gates --------------------------------------------------------- +-- ---- pre-intern gate ---------------------------------------------------------- -- Nothing reaches the Shen reader unless every atom in it is already known: -- rule names + predicates + actions (static vocabulary) or an atom of the --- current fact world. A bounded budget of distinct admitted tokens --- backstops any gate/reader divergence: exhaust it and the gate denies --- everything rather than leak interned symbols forever. +-- CURRENT fact world. That is what bounds the permanent symbol table — the +-- fact world is written only by admin grants (facts.lua validates every +-- pred/s/r), so the set of admissible atoms is operator-controlled and an +-- attacker's novel atoms are rejected here, before read-from-string. local STATIC_VOCAB = { ["fact"] = true, ["by-owner"] = true, ["by-member-read"] = true, ["by-delegation"] = true, @@ -71,25 +78,19 @@ local STATIC_VOCAB = { ["read"] = true, ["write"] = true, ["delete"] = true, ["member"] = true, } -local ATOM_BUDGET = 4096 -local seen_atoms, seen_count = {}, 0 - local function atom_ok(s) return type(s) == "string" and s ~= "" and s:match("^[a-z][a-z0-9%-%.%_]*$") ~= nil end --- The gate is an intern-DoS backstop, not authorization: an atom admitted --- once is already interned, so admission is MONOTONE — revoking a --- subject's last fact does not make them "unknown" here; it makes their --- proofs fail at the type level, with the honest reason. +-- Stateless on purpose. An earlier version kept a per-worker monotone +-- seen-set with a fixed cap; the cap never bounded the attacker (fact-world +-- membership already does) but DID false-deny legitimate atoms once a worker +-- had handled more than the cap's worth of distinct principals. A principal +-- whose facts are all revoked is simply unknown to this fact world and denies +-- here; a production gateway wanting a type-level reason for recently-revoked +-- principals would add an LRU grace set (see the Garmr implementation note). local function admit(token, snap) - if not atom_ok(token) then return false end - if STATIC_VOCAB[token] or seen_atoms[token] then return true end - if not snap.atoms[token] then return false end - if seen_count >= ATOM_BUDGET then return false end - seen_count = seen_count + 1 - seen_atoms[token] = true - return true + return atom_ok(token) and (STATIC_VOCAB[token] == true or snap.atoms[token] == true) end -- every proof token must be a known word; brackets are structure @@ -224,8 +225,13 @@ function M.gate() " by ", audit.proof, " (", audit.infs, " inferences, facts v", audit.facts_version, ", leaves ", table.concat(audit.leaves, " "), ")") - ngx.header["X-Proof-Checked"] = tostring(audit.infs) .. " inferences" + -- X-Facts-Version is a legitimate protocol element (the consistency token a + -- client uses to reason about staleness); the inference count is internal + -- detail, exposed only when PCR_DEBUG_HEADERS=1. ngx.header["X-Facts-Version"] = tostring(audit.facts_version) + if DEBUG_HEADERS then + ngx.header["X-Proof-Checked"] = tostring(audit.infs) .. " inferences" + end -- fall through to the protected content end diff --git a/examples/pcr/facts.lua b/examples/pcr/facts.lua index cb71f73..c660031 100644 --- a/examples/pcr/facts.lua +++ b/examples/pcr/facts.lua @@ -45,7 +45,11 @@ M.W = 1 -- replica sync period (seconds); staleness hard cap = 3W -- blob change" test below is a pointer compare after the get. local shm = ngx and ngx.shared and ngx.shared.pcr_facts local cell = { v = nil } -- fallback store -M._simulate_write_failure = nil -- selftest hook; normal plain-Lua fallback still succeeds + +-- Test-only seam (used by selftest.lua); nil in normal operation. Grouped +-- under one table so it reads as "not the public API." See M._test helpers +-- at the bottom for the corrupt-blob / clear injectors. +M._test = { simulate_write_failure = nil } local function blob_get() if shm then return shm:get("blob") end @@ -53,7 +57,7 @@ local function blob_get() end local function blob_set(s) - if M._simulate_write_failure then return false, M._simulate_write_failure end + if M._test.simulate_write_failure then return false, M._test.simulate_write_failure end if shm then local ok, err = shm:set("blob", s) if not ok then return false, err or "unknown shared-dict set failure" end @@ -63,11 +67,12 @@ local function blob_set(s) end -- ---- writes (authority side) ------------------------------------------------- -local function decode_blob() - local raw = blob_get() +local function decode_blob(raw) + raw = raw or blob_get() if not raw then return nil end local ok, t = pcall(json.decode, raw) - if not ok or type(t) ~= "table" or type(t.facts) ~= "table" then return nil end + if not ok or type(t) ~= "table" or type(t.facts) ~= "table" + or type(t.version) ~= "number" then return nil end return t end @@ -86,8 +91,23 @@ function M.seed(facts) return write(facts, 1) end +-- Apply one grant/revoke. Distinguish an ABSENT blob (first write — start +-- fresh at version 1) from a PRESENT-but-undecodable one: REFUSE the latter +-- rather than silently reset. snapshot() already denies reads on an +-- undecodable blob; a write must not "heal" it into a fresh 1-fact world, +-- which would wipe every fact and rewind the version the audit trail depends +-- on. The refusal propagates through grant/revoke to a 507 at the admin API. local function mutate(f) - local t = decode_blob() or { version = 0, facts = {} } + local raw = blob_get() + local t + if raw then + t = decode_blob(raw) + if not t then + return false, nil, "fact store undecodable; refusing to overwrite" + end + else + t = { version = 0, facts = {} } + end f(t.facts) return write(t.facts, t.version + 1) end @@ -193,4 +213,18 @@ function M.start_sync_timer(fetch) return true end +-- ---- test-only injectors (selftest.lua) ---------------------------------------- +-- Not part of the public API. corrupt_blob() writes an undecodable blob so the +-- selftest can prove reads deny and mutate refuses; clear() empties the store. +function M._test.corrupt_blob() + local garbage = "{not-json" + if shm then shm:set("blob", garbage) else cell.v = garbage end + SNAP, SNAP_RAW = nil, nil +end + +function M._test.clear() + if shm then shm:delete("blob") else cell.v = nil end + SNAP, SNAP_RAW = nil, nil +end + return M diff --git a/examples/pcr/nginx.conf b/examples/pcr/nginx.conf index aa55de1..d99d110 100644 --- a/examples/pcr/nginx.conf +++ b/examples/pcr/nginx.conf @@ -32,6 +32,7 @@ daemon off; worker_processes 2; # exercise cross-worker fact propagation pid logs/nginx.pid; error_log logs/error.log info; # the proof audit lines land here +env PCR_DEBUG_HEADERS; # opt-in: expose the inference count as a response header events { worker_connections 256; } diff --git a/examples/pcr/selftest.lua b/examples/pcr/selftest.lua index 54ac9bf..2a59b9b 100644 --- a/examples/pcr/selftest.lua +++ b/examples/pcr/selftest.lua @@ -26,6 +26,18 @@ local function expect(label, want, subject, action, resource, proof) if authorized ~= want then fail = fail + 1; print(" FAIL: expected " .. tostring(want)) end end +-- assert a DENY whose reason contains a substring — used to prove *which +-- layer* denied (the type checker vs the pre-intern gate). +local function expect_reason(label, want_sub, subject, action, resource, proof) + local authorized, reason = app.check(subject, action, resource, proof) + local ok = (not authorized) and reason:find(want_sub, 1, true) ~= nil + io.write((" %-30s %-5s %s\n"):format(label, authorized and "ALLOW" or "DENY", reason)) + if not ok then + fail = fail + 1 + print(" FAIL: expected deny with reason containing: " .. want_sub) + end +end + local function expect_admin(label, want_ok, path, body) local status, out = app.dispatch("POST", path, body) io.write((" %-30s HTTP %-3d %s\n"):format(label, status, out.reason or out.error or "ok")) @@ -66,10 +78,19 @@ expect("...kills chains on it", false, "carol", "write", "doc1", deleg_proof) facts.grant("owns", "alice", "doc1") expect("restore root fact", true, "alice", "write", "doc1", owner_proof) +-- a known principal (carol is a tenant member) whose delegated capability is +-- revoked must deny at the TYPE layer with the honest reason — not be rejected +-- at the gate as an unknown atom. This locks the admit() rework: fact-world +-- atoms are always admitted, so carol reaches the checker and fails there. +facts.revoke("delegates", "alice", "carol") +expect_reason("de-authorized, still known", "proof does not establish", + "carol", "write", "doc1", deleg_proof) +facts.grant("delegates", "alice", "carol") + print("\n== fact-store write failures fail closed ==") local before = facts.snapshot() local before_version = before.version -facts._simulate_write_failure = "simulated shared-dict full" +facts._test.simulate_write_failure = "simulated shared-dict full" expect_admin("failed revoke reports", false, "/admin/revoke", { pred = "delegates", s = "alice", r = "carol" }) expect("failed revoke keeps grant", true, "carol", "write", "doc1", deleg_proof) @@ -89,7 +110,7 @@ if after.version ~= before_version then print(" FAIL: failed grant advanced fact version") end -facts._simulate_write_failure = nil +facts._test.simulate_write_failure = nil expect_admin("grant recovers", true, "/admin/grant", { pred = "delegates", s = "alice", r = "erin" }) expect("recovered grant allows", true, "erin", "write", "doc1", erin_proof) @@ -197,5 +218,21 @@ local us = (os.clock() - t0) * 1e6 / N io.write((" nested delegation vs live facts: %.0f us/check (%d inferences), ~%d checks/sec/core\n") :format(us, shen.value("shen.*infs*"), math.floor(1e6 / us))) +-- last, because it leaves the store corrupt: an undecodable blob must deny +-- reads AND make a mutation refuse (not silently reset the fact world). +print("\n== undecodable blob: reads deny, mutate refuses (no reset) ==") +facts._test.corrupt_blob() +if facts.snapshot() ~= nil then + fail = fail + 1; print(" FAIL: corrupt blob must make snapshot() deny") +else + print(" corrupt blob -> snapshot denies ok") +end +local st = app.dispatch("POST", "/admin/grant", { pred = "owns", s = "alice", r = "doc9" }) +if st == 200 then + fail = fail + 1; print(" FAIL: mutate over a corrupt blob must refuse, not reset") +else + print((" mutate over corrupt blob -> HTTP %d ok"):format(st)) +end + if fail == 0 then print("\nOK — all checks passed") else print(("\n%d check(s) FAILED"):format(fail)); os.exit(1) end From 0e3b2eae4ea9d876e38998ac3e03e05111133fff Mon Sep 17 00:00:00 2001 From: Reuben Brooks Date: Mon, 6 Jul 2026 17:43:46 -0500 Subject: [PATCH 6/6] examples: add strong-ideas.md; ignore built *.src.rock MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit strong-ideas.md is the vision doc behind this line of work — one typed Shen core projected into every host that owns a boundary (edge, native, ops, browser). The pcr example is its first concrete slice. Co-Authored-By: Claude Fable 5 --- .gitignore | 1 + examples/strong-ideas.md | 72 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 examples/strong-ideas.md diff --git a/.gitignore b/.gitignore index ccbfdd5..44e2624 100644 --- a/.gitignore +++ b/.gitignore @@ -5,6 +5,7 @@ build/shen-bundle.lua .fasl-test/ luacov.stats.out luacov.report.out +*.src.rock examples/*/logs/ examples/*/client_body_temp/ examples/*/fastcgi_temp/ diff --git a/examples/strong-ideas.md b/examples/strong-ideas.md new file mode 100644 index 0000000..f740bbf --- /dev/null +++ b/examples/strong-ideas.md @@ -0,0 +1,72 @@ +# Strong Ideas: Shen at the Edge, in Systems Code, and in Ops + +This repo shows the small version of a larger pattern: put the hard semantic +rules in typed Shen, then run the same rules wherever decisions are made. +`shen-lua` gives LuaJIT/OpenResty deployment, `shen-rust` gives native systems +embedding and verification, `shen-go` gives static operational binaries, and +browser-targeted Shen builds can remove client/server drift. + +## The Shape + +Write one compact Shen core for: + +- domain types and invariants +- request validation and routing contracts +- authorization and policy rules +- state transition laws +- config generation rules +- explanation/proof terms for audit + +Then project that core into the host that owns the boundary: + +- **OpenResty/LuaJIT** for edge enforcement and hot-path request handling. +- **Rust** for native libraries, offline verification, crypto, Cedar + integration, and performance-critical kernels. +- **Go** for CLIs, Kubernetes controllers, admission webhooks, operators, and + CI checks. +- **JavaScript/browser builds** for client validation from the same source of + truth. + +The payoff is that policy, validation, generation, and audit stop being +separate hand-maintained implementations. The Shen file becomes the semantic +artifact; host code becomes glue, I/O, persistence, and acceleration. + +## What Becomes Buildable + +- **Verified API gateways and edge policy engines.** A request reaches a + backend only if route, tenant, JWT claims, resource, action, and backend + destination satisfy one typed policy. +- **Policy compilers with proof backpressure.** Generate Cedar, OpenResty, + Kubernetes, JSON Schema, or other policy/config artifacts from Shen, then + check that generated output still preserves the source invariant. +- **Infrastructure safety controllers.** Use Shen-Go to reject unsafe cluster + changes: public ingress without proof, workloads without limits, secrets in + untrusted namespaces, or tenant routes that break isolation. +- **Financial and ledger cores.** Encode balance conservation, settlement state + machines, idempotency, replay protection, and audit completeness as rules and + types, then serve them from Rust and gate them at the edge. +- **Agent guardrails and tool routers.** Treat every tool call as a typed state + transition with capability policy, input contract, budget accounting, allowed + side effects, and output obligations. + +## A Good Product Slice + +A first serious product would be a typed policy/config compiler: + +```text +policy.shen + -> openresty/policy.lua request-time enforcement + -> policy.cedar authorization engine artifact + -> admission-webhook Go platform safety gate + -> policy-verifier Rust CI/audit verifier + -> client-validator.js browser-side drift prevention +``` + +The demo invariant should be concrete and end-to-end: + +> No request can reach a tenant resource unless the route, credentials, tenant +> binding, resource action, and backend destination all agree on the same tenant +> and permission model. + +That is the useful scary part: one small verified semantic core, enforced at +every boundary where the system can go wrong.