diff --git a/.gitignore b/.gitignore index 22aae81..44e2624 100644 --- a/.gitignore +++ b/.gitignore @@ -5,5 +5,10 @@ build/shen-bundle.lua .fasl-test/ luacov.stats.out luacov.report.out -examples/openresty/logs/ -examples/openresty-authz/logs/ +*.src.rock +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 bcf6143..e0cead2 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 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. | | [`openresty-authz/`](openresty-authz/) | durable multi-tenant **authorization**: the policy as a Prolog proof chain (`token → user → tenant → resource`), a typed `decision` witness that gates every response, and an event-sourced store (file + `lua-resty-lmdb`) whose append-only log makes decisions durable and auditable. Runs standalone via `luajit examples/openresty-authz/selftest.lua`; see [its README](openresty-authz/README.md). | diff --git a/examples/pcr/README.md b/examples/pcr/README.md new file mode 100644 index 0000000..3379c34 --- /dev/null +++ b/examples/pcr/README.md @@ -0,0 +1,164 @@ +# Proof-carrying requests, over live facts + +An authorization gateway where the client **carries the proof** and the edge +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 +``` + +## Check, don't search — and facts are live + +Two asymmetries make this affordable and correct at request time: + +* **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. + +Facts stop being axioms in the rules. One rule replaces them all +(`rules.shen`): + +``` +if (pcr.fact? Pred S R) +________________________ +[fact Pred S R] : (Pred S R); +``` + +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 + +``` +# 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-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"}' +{"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} +``` + +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. 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 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 +(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) + +| attack | defense | +|---|---| +| 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 | +| 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 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 | + +**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: 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 new file mode 100644 index 0000000..895e091 --- /dev/null +++ b/examples/pcr/app.lua @@ -0,0 +1,238 @@ +-- examples/pcr/app.lua — proof-carrying requests over LIVE facts. +-- +-- 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: 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. +-- +-- 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 facts = require("facts") + +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 + +-- 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 -)") + +-- 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. +-- 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 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. 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, + ["owns"] = true, ["same-tenant"] = true, ["has-role"] = true, + ["delegates"] = true, + ["read"] = true, ["write"] = true, ["delete"] = true, ["member"] = true, +} + +local function atom_ok(s) + return type(s) == "string" and s ~= "" and s:match("^[a-z][a-z0-9%-%.%_]*$") ~= nil +end + +-- 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) + 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 +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 + 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*"), + facts_version = snap.version, + sync_age = facts.now() - snap.synced_at, + leaves = facts.leaves(), + } +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 + 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 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 + 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 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" } +end + +local M = { dispatch = dispatch, check = check, json = cjson, facts = facts } + +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 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" + 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 how, against which fact world + ngx.log(ngx.INFO, "authorized ", audit.judgment, + " by ", audit.proof, + " (", audit.infs, " inferences, facts v", audit.facts_version, + ", leaves ", table.concat(audit.leaves, " "), ")") + -- 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 + +return M diff --git a/examples/pcr/facts.lua b/examples/pcr/facts.lua new file mode 100644 index 0000000..c660031 --- /dev/null +++ b/examples/pcr/facts.lua @@ -0,0 +1,230 @@ +-- 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 + +-- 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 + return cell.v +end + +local function blob_set(s) + 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 + return true + end + cell.v = s; return true +end + +-- ---- writes (authority side) ------------------------------------------------- +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" + or type(t.version) ~= "number" then return nil end + return t +end + +local function write(facts, version) + local blob = json.encode{ version = version, synced_at = M.now(), facts = facts } + 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 + 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 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 + +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("^[a-z][a-z0-9%-%.%_]*$") ~= 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() + 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) + 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/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..d99d110 --- /dev/null +++ b/examples/pcr/nginx.conf @@ -0,0 +1,84 @@ +# 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 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 [fact owns alice doc1] [fact same-tenant alice doc1]] [fact delegates alice carol]]' \ +# -X POST localhost:8093/protected/ +# +# # 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/ +# +# # 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 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; } + +http { + access_log logs/access.log; + + lua_shared_dict pcr_facts 4m; # the ONE versioned fact blob + + 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 + seed the fact blob (add-if-absent) 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 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","worker":' .. ngx.worker.pid() .. '}') } + } + + # 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..366f8e3 --- /dev/null +++ b/examples/pcr/rules.shen @@ -0,0 +1,47 @@ +\\ 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. +\\ +\\ 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 + \\ -- 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 + 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..2a59b9b --- /dev/null +++ b/examples/pcr/selftest.lua @@ -0,0 +1,238 @@ +-- examples/pcr/selftest.lua — verify the live-facts proof-carrying gateway off-nginx. +-- +-- 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 (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 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((" %-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 + +-- 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")) + 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]]" + +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) + +-- 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._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) +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._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) +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) +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 .. " [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 [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]]") +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 +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) +shen.eval("(set shen.*maxinferences* " .. tostring(prev_max) .. ")") +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 (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 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 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. 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.