diff --git a/examples/shen-cedar-authz/examples/equiv.rs b/examples/shen-cedar-authz/examples/equiv.rs new file mode 100644 index 0000000..ef54035 --- /dev/null +++ b/examples/shen-cedar-authz/examples/equiv.rs @@ -0,0 +1,325 @@ +//! Example 4 — **codegen-equivalence gate** (shen-derive, native). +//! +//! `generate.rs` renders Cedar from `spec/authz.shen` and strict-validates the +//! *shape* of the result against the schema. It never checks that the Cedar +//! PolicySet *decides the same way* as the Shen spec it came from. Schema +//! validation catches an ill-typed policy; it does not catch a closure bug, a +//! rendering bug, or a hand-edit that quietly drops a permit. +//! +//! This is the shen-derive move, done natively: the Shen spec is the **oracle** +//! (evaluated in the served VM, `expand-all`), the generated Cedar is the +//! **target**, and the gate enumerates the whole finite request space asserting +//! the two agree on every decision. No Go, no subprocess — the VM and the Cedar +//! `Authorizer` run in one Rust process, exactly as the other examples do. +//! +//! The harness itself is generic over two small traits: +//! +//! * [`Oracle`] — the source-of-truth decision. Today the only impl is +//! [`ShenSpecOracle`], backed by the served Shen VM's `expand-all` permit +//! set. The trait is deliberately narrow (`allows` + `name`) so a *different* +//! oracle — e.g. an out-of-process SBCL evaluation of the same spec — could +//! be dropped in to cross-check the shen-rust VM itself. +//! * [`Target`] — the artifact under test. Today the only impl is +//! [`CedarTarget`], backed by the Cedar `Authorizer` over the generated +//! `PolicySet` + entities. The trait is likewise narrow so a *different* +//! target — e.g. a shengen→Rust compiled guard function — could be checked +//! against the same oracle with no change to the gate loop. +//! +//! Those alternate impls are intentionally **not** provided here; the traits +//! just establish the seam. +//! +//! Pass `--inject-drift` to drop one generated permit before the check, to see +//! the gate flag the now-divergent requests (and exit non-zero). +//! +//! Run: `cargo run -p shen-cedar-authz --example equiv [-- --inject-drift]` + +use std::collections::HashSet; +use std::str::FromStr; + +use cedar_policy::{ + Authorizer, Context, Decision, Entities, EntityUid, PolicySet, Request, Schema, +}; + +use shen_cedar_authz::{entities, read_list, schema, validate_policies, ShenHost}; + +const SPEC_SRC: &str = include_str!("../spec/authz.shen"); + +/// The test fixture: one user per role, so every role's closure is exercised. +/// (user, role) — each user is a direct member of exactly that Role. +const USERS: &[(&str, &str)] = &[ + ("alice", "Analyst"), + ("fred", "Auditor"), + ("dana", "Admin"), + ("erin", "Lead"), +]; + +/// Resources to probe. `io` is granted to no role — both engines must DENY it, +/// so it exercises agreement-on-false, not just agreement-on-true. +const RESOURCES: &[&str] = &["pure", "logs", "io"]; + +/// The source-of-truth decision the gate trusts. +/// +/// `role`/`action`/`resource` are the spec-level coordinates of a request. The +/// only impl today is [`ShenSpecOracle`] (the served Shen VM); the trait exists +/// so a future SBCL evaluation of the same spec could be dropped in to +/// cross-check the shen-rust VM with no change to the gate loop. +trait Oracle { + fn allows(&mut self, role: &str, action: &str, resource: &str) -> bool; + fn name(&self) -> &str; +} + +/// The artifact under test — the thing the oracle is checked against. +/// +/// `user`/`action`/`resource` are the concrete request coordinates (a user, not +/// a role: membership is resolved inside the target). The only impl today is +/// [`CedarTarget`] (the generated Cedar `PolicySet`); the trait exists so a +/// future shengen→Rust compiled guard could be checked against the same oracle +/// with no change to the gate loop. +trait Target { + fn allows(&mut self, user: &str, action: &str, resource: &str) -> bool; + fn name(&self) -> &str; +} + +/// [`Oracle`] backed by the served Shen VM's `expand-all` permit closure, +/// materialised as a set of `(role, action, resource)` triples. +struct ShenSpecOracle { + name: String, + permits: HashSet<(String, String, String)>, +} + +impl Oracle for ShenSpecOracle { + fn allows(&mut self, role: &str, action: &str, resource: &str) -> bool { + self.permits + .contains(&(role.to_string(), action.to_string(), resource.to_string())) + } + fn name(&self) -> &str { + &self.name + } +} + +/// [`Target`] backed by the Cedar `Authorizer` over the generated `PolicySet` +/// and the fixture entities, schema-checked. +struct CedarTarget { + name: String, + authz: Authorizer, + set: PolicySet, + entities: Entities, + schema: Schema, +} + +impl Target for CedarTarget { + fn allows(&mut self, user: &str, action: &str, resource: &str) -> bool { + let req = Request::new( + EntityUid::from_str(&format!("User::{user:?}")).unwrap(), + EntityUid::from_str(&format!("Action::{action:?}")).unwrap(), + EntityUid::from_str(&format!("ShenCap::{resource:?}")).unwrap(), + Context::empty(), + Some(&self.schema), + ) + .expect("request"); + matches!( + self.authz + .is_authorized(&req, &self.set, &self.entities) + .decision(), + Decision::Allow + ) + } + fn name(&self) -> &str { + &self.name + } +} + +fn main() { + let handle = std::thread::Builder::new() + .stack_size(64 * 1024 * 1024) + .spawn(run) + .expect("spawn"); + std::process::exit(handle.join().unwrap_or(2)); +} + +fn run() -> i32 { + let inject_drift = std::env::args().any(|a| a == "--inject-drift"); + + let schema = match schema() { + Ok(s) => s, + Err(e) => { + eprintln!("{e}"); + return 1; + } + }; + + // --- The oracle: evaluate the Shen spec in the served VM. ---------------- + eprint!("booting served Shen VM… "); + let mut host = match ShenHost::new() { + Ok(h) => h, + Err(e) => { + eprintln!("FAILED: {e}"); + return 1; + } + }; + if let Err(e) = host.load_source(SPEC_SRC) { + eprintln!("load spec: {e}"); + return 1; + } + eprintln!("ready (oracle: spec/authz.shen)."); + + let grants_v = match host.call("expand-all", vec![]) { + Ok(v) => v, + Err(e) => { + eprintln!("expand-all: {e}"); + return 1; + } + }; + + // The spec's permit closure as a set of (role, action, resource) triples, + // plus the Cedar rendered from it (the target's source). + let mut spec_permits: HashSet<(String, String, String)> = HashSet::new(); + let mut cedar = String::new(); + let mut rendered: Vec = Vec::new(); + for triple in read_list(&grants_v) { + let parts = read_list(&triple); + if parts.len() != 3 { + continue; + } + let (role, action, res) = ( + host.text(&parts[0]), + host.text(&parts[1]), + host.text(&parts[2]), + ); + spec_permits.insert((role.clone(), action.clone(), res.clone())); + let policy = format!( + "permit(principal in Role::{role:?}, action == Action::{action:?}, resource == ShenCap::{res:?});" + ); + if !rendered.contains(&policy) { + // --- inject a codegen/hand-edit drift: drop Admin·logs --------- + if inject_drift && role == "Admin" && res == "logs" { + eprintln!(" (injected drift: dropping generated permit Admin·logs)"); + continue; + } + rendered.push(policy.clone()); + cedar.push_str(&policy); + cedar.push('\n'); + } + } + + let oracle = ShenSpecOracle { + name: "spec/authz.shen".to_string(), + permits: spec_permits, + }; + + // --- The target: parse + strict-validate the generated Cedar. ----------- + let set = match PolicySet::from_str(&cedar) { + Ok(s) => s, + Err(e) => { + eprintln!("generated Cedar failed to parse: {e}"); + return 1; + } + }; + let errs = validate_policies(&set, &schema); + if !errs.is_empty() { + eprintln!("generated policy FAILED schema validation:"); + for e in errs { + eprintln!(" - {e}"); + } + return 1; + } + + let entities_json = build_entities_json(); + let entities = match entities(&entities_json, &schema) { + Ok(e) => e, + Err(e) => { + eprintln!("{e}"); + return 1; + } + }; + + let target = CedarTarget { + name: "Cedar PolicySet".to_string(), + authz: Authorizer::new(), + set, + entities, + schema: schema.clone(), + }; + + gate(oracle, target) +} + +/// The gate: for every request in the finite space, the oracle and the target +/// must agree. Generic over [`Oracle`]/[`Target`] so the harness is not +/// hard-wired to (shen-rust VM × Cedar). +fn gate(mut oracle: impl Oracle, mut target: impl Target) -> i32 { + println!("\n=== shen-derive: codegen-equivalence gate ==="); + println!("oracle = {} (shen-rust VM: expand-all)", oracle.name()); + println!("target = {} generated from that spec", target.name()); + println!( + "checking {} requests ({} users × {} resources, action Eval)\n", + USERS.len() * RESOURCES.len(), + USERS.len(), + RESOURCES.len() + ); + println!(" request spec cedar"); + println!(" ------------------------------------------"); + + let mut divergences = 0; + for (user, role) in USERS { + for res in RESOURCES { + let spec_allow = oracle.allows(role, "Eval", res); + let cedar_allow = target.allows(user, "Eval", res); + + let agree = spec_allow == cedar_allow; + if !agree { + divergences += 1; + } + let mark = if agree { "✓" } else { "✗ DIVERGENCE" }; + println!( + " {:<20} {:<6} {:<6} {mark}", + format!("{user}({role})·{res}"), + yn(spec_allow), + yn(cedar_allow), + ); + } + } + + let n = USERS.len() * RESOURCES.len(); + println!(); + if divergences == 0 { + println!("{n}/{n} agree — generated Cedar is equivalent to the spec ✓"); + 0 + } else { + println!( + "{divergences}/{n} DIVERGE — generated Cedar does NOT decide like the spec ✗\n\ + the gate would fail the build: the Cedar drifted from spec/authz.shen." + ); + 1 + } +} + +fn yn(b: bool) -> &'static str { + if b { + "ALLOW" + } else { + "DENY" + } +} + +/// Build the entities JSON for the fixture: each user is a member of its Role. +fn build_entities_json() -> String { + let mut roles: Vec<&str> = USERS.iter().map(|(_, r)| *r).collect(); + roles.sort_unstable(); + roles.dedup(); + let users: Vec = USERS + .iter() + .map(|(u, r)| { + format!( + r#"{{ "uid": {{"type":"User","id":"{u}"}}, "attrs": {{}}, "parents": [{{"type":"Role","id":"{r}"}}] }}"# + ) + }) + .collect(); + let role_ents: Vec = roles + .iter() + .map(|r| { + format!(r#"{{ "uid": {{"type":"Role","id":"{r}"}}, "attrs": {{}}, "parents": [] }}"#) + }) + .collect(); + format!("[{}]", [users, role_ents].concat().join(",\n")) +} diff --git a/examples/shen-cedar-authz/examples/reaches_equiv.rs b/examples/shen-cedar-authz/examples/reaches_equiv.rs new file mode 100644 index 0000000..c6fe9c4 --- /dev/null +++ b/examples/shen-cedar-authz/examples/reaches_equiv.rs @@ -0,0 +1,222 @@ +//! Example 5 — **one relation, two evaluations, differentially tested**. +//! +//! Role reachability ("is role A a member of, i.e. does it reach, role B over +//! the role DAG?") is specified *twice* and checked for agreement over the +//! whole finite domain: +//! +//! * **Prolog** — the kernel's REAL built-in Prolog engine. `reaches` is a +//! `defprolog` procedure (reflexivity + parent-transitivity) over `parent` +//! facts for the role DAG. Each `(role, role)` pair is decided by running a +//! ground goal through the engine via `(prolog? (reaches A B))`, which the +//! served VM evaluates to `true`/`false`. +//! +//! * **Functional** — the `reaches` *defun* ported verbatim from `verify.rs`: +//! a `[child parent]` edge-list reachability fold (`reaches` / `reaches-list` +//! / `parents-of`). No unification, no backtracking — a plain recursive +//! membership-closure over the same DAG. +//! +//! Both run in the SAME served Shen VM, in one Rust process. The gate +//! enumerates every ordered pair over the role set, evaluates both relations, +//! prints the truth table, and asserts the two agree on every cell. Exit 0 iff +//! the relations are identical over the domain; exit 1 on any divergence — +//! the same gate style as `equiv.rs`. +//! +//! Run: `cargo run -p shen-cedar-authz --example reaches_equiv` + +use shen_cedar_authz::ShenHost; +use shen_rust::value::Value; + +/// The role set. Every ordered pair (49 of them) is checked. +const ROLES: &[&str] = &[ + "Analyst", "Auditor", "Admin", "Lead", "Staff", "Intern", "Manager", +]; + +/// The role DAG as `child in parent` edges. Shared by both evaluations: +/// * the Prolog side reads it as `parent/2` facts (lower-cased symbols); +/// * the functional side reads it as a `[child parent]` Shen edge list. +/// +/// A small diamond + chain so reflexivity, single-hop, multi-hop and +/// no-reverse-edge cases are all exercised. +const EDGES: &[(&str, &str)] = &[ + ("Analyst", "Staff"), + ("Auditor", "Staff"), + ("Intern", "Staff"), + ("Staff", "Lead"), + ("Lead", "Manager"), + ("Admin", "Manager"), +]; + +/// The FUNCTIONAL `reaches`, ported verbatim from `verify.rs`: a `[child parent]` +/// edge-list reachability fold. `a reaches b` == `a` is-in `b` (a == b, or some +/// parent of a reaches b). +const FUNCTIONAL: &[&str] = &[ + "(defun parents-of (x es) (if (= es []) [] \ + (if (= (hd (hd es)) x) (cons (hd (tl (hd es))) (parents-of x (tl es))) \ + (parents-of x (tl es)))))", + "(defun reaches (a b es) (if (= a b) true (reaches-list (parents-of a es) b es)))", + "(defun reaches-list (ps b es) (if (= ps []) false \ + (if (reaches (hd ps) b es) true (reaches-list (tl ps) b es))))", +]; + +/// The role-reachability relation in the kernel's REAL Prolog engine. +/// +/// `prolog-reaches` is the procedure name (kept distinct from the functional +/// `reaches` defun so both can coexist in one VM). `;` is spaced away from +/// `<--` because the embedding parses these forms with the KL reader, which — +/// unlike Shen's own `.shen` reader — does not split a trailing `<--;` token. +/// +/// `parent/2` carries the same edges as `EDGES`, written as lower-cased +/// symbols (Prolog atoms) and generated below so the two sources cannot drift. +fn prolog_source() -> String { + let mut facts = String::from("(defprolog parent\n"); + for (c, p) in EDGES { + facts.push_str(&format!( + " {} {} <-- ;\n", + c.to_lowercase(), + p.to_lowercase() + )); + } + facts.push_str(")\n"); + // reflexivity + parent-transitivity + facts.push_str( + "(defprolog prolog-reaches\n \ + X X <-- ;\n \ + X Y <-- (parent X Z) (prolog-reaches Z Y) ;)", + ); + facts +} + +fn main() { + let handle = std::thread::Builder::new() + .stack_size(64 * 1024 * 1024) + .spawn(run) + .expect("spawn"); + std::process::exit(handle.join().unwrap_or(2)); +} + +fn run() -> i32 { + eprint!("booting served Shen VM… "); + let mut host = match ShenHost::new() { + Ok(h) => h, + Err(e) => { + eprintln!("FAILED: {e}"); + return 1; + } + }; + + // Load the FUNCTIONAL reaches (defun) ported from verify.rs. + if let Err(e) = host.load_source(&FUNCTIONAL.join("\n")) { + eprintln!("load functional reaches: {e}"); + return 1; + } + // Load the PROLOG reaches (defprolog) into the SAME VM. + if let Err(e) = host.load_source(&prolog_source()) { + eprintln!("load prolog reaches: {e}"); + return 1; + } + eprintln!("ready.\n"); + + // Build the `[child parent]` edge list as Shen data once (functional input). + let edges: Vec = EDGES + .iter() + .map(|(c, p)| host.list([host.string(c), host.string(p)])) + .collect(); + let edges = host.list(edges); + + println!( + "Role reachability — functional (defun) vs Prolog (defprolog), same DAG, same VM.\n\ + Legend per cell: · = neither reaches, T = both true, F = both false (agree),\n\ + X = DISAGREE. Rows = from-role, columns = to-role.\n" + ); + + // Header row. + print!("{:>9} |", "from \\ to"); + for to in ROLES { + print!(" {:>7}", to); + } + println!(); + print!("{:->9}-+", ""); + for _ in ROLES { + print!("{:->8}", ""); + } + println!(); + + let mut disagreements = 0usize; + let mut true_count = 0usize; + for from in ROLES { + print!("{:>9} |", from); + for to in ROLES { + let f = functional_reaches(&mut host, from, to, edges); + let p = prolog_reaches(&mut host, from, to); + let (fv, pv) = match (f, p) { + (Ok(fv), Ok(pv)) => (fv, pv), + (Err(e), _) | (_, Err(e)) => { + println!("\nevaluation error at ({from},{to}): {e}"); + return 1; + } + }; + if fv { + true_count += 1; + } + let cell = if fv != pv { + disagreements += 1; + "X" + } else if fv { + "T" + } else { + "F" + }; + print!(" {:>7}", cell); + } + println!(); + } + + let total = ROLES.len() * ROLES.len(); + println!( + "\nChecked {total} ordered pairs over {} roles ({true_count} reachable, {} not).", + ROLES.len(), + total - true_count + ); + + if disagreements == 0 { + println!( + "Functional `reaches` (defun) and Prolog `prolog-reaches` (defprolog) \ + AGREE on every pair ✓" + ); + 0 + } else { + println!("DIVERGENCE: {disagreements} pair(s) where the two relations disagree (X) ✗"); + 1 + } +} + +/// Decide `from reaches to` with the FUNCTIONAL defun over the `[child parent]` +/// edge list. +fn functional_reaches( + host: &mut ShenHost, + from: &str, + to: &str, + edges: Value, +) -> Result { + let a = host.string(from); + let b = host.string(to); + let v = host + .call("reaches", vec![a, b, edges]) + .map_err(|e| format!("functional reaches: {e}"))?; + Ok(v.as_bool().unwrap_or(false)) +} + +/// Decide `from reaches to` by running a GROUND goal through the kernel's real +/// Prolog engine: `(prolog? (prolog-reaches ))` evaluates to a +/// boolean. Roles are lower-cased to match the `parent/2` atoms. +fn prolog_reaches(host: &mut ShenHost, from: &str, to: &str) -> Result { + let query = format!( + "(prolog? (prolog-reaches {} {}))", + from.to_lowercase(), + to.to_lowercase() + ); + let v = host + .eval(&query) + .map_err(|e| format!("prolog query: {e}"))?; + Ok(v.as_bool().unwrap_or(false)) +} diff --git a/sb.toml b/sb.toml index 947882c..b404594 100644 --- a/sb.toml +++ b/sb.toml @@ -26,6 +26,7 @@ build = "cargo build --workspace" test = "cargo test --workspace" shen = "scripts/shen-check.sh" audit = "scripts/tcb-audit.sh" +equiv = "scripts/shen-cedar-equiv.sh" run_all = "scripts/gates.sh" [tcb] diff --git a/scripts/gates.sh b/scripts/gates.sh index f391522..7b5834c 100755 --- a/scripts/gates.sh +++ b/scripts/gates.sh @@ -27,6 +27,7 @@ run "Gate 4: shen-check" scripts/shen-check.sh run "Gate 5: tcb-audit" scripts/tcb-audit.sh run "Gate 6: kernel-aot-audit" scripts/kernel-aot-audit.sh run "Gate 7: kernel-tests" scripts/kernel-tests.sh +run "Gate 8: cedar-equiv" scripts/shen-cedar-equiv.sh echo if [ ${#fail[@]} -eq 0 ]; then diff --git a/scripts/shen-cedar-equiv.sh b/scripts/shen-cedar-equiv.sh new file mode 100755 index 0000000..51cf829 --- /dev/null +++ b/scripts/shen-cedar-equiv.sh @@ -0,0 +1,20 @@ +#!/bin/bash +# Gate 8: codegen-equivalence examples for shen-cedar-authz. +# +# Runs the `equiv` example, and the `reaches_equiv` example if present, +# under shen-cedar-authz. Exits non-zero if any invoked example fails. +set -euo pipefail + +cd "$(dirname "$0")/.." + +echo "shen-cedar-equiv: running equiv example" +cargo run -q -p shen-cedar-authz --example equiv + +if [ -f examples/shen-cedar-authz/examples/reaches_equiv.rs ]; then + echo "shen-cedar-equiv: running reaches_equiv example" + cargo run -q -p shen-cedar-authz --example reaches_equiv +else + echo "shen-cedar-equiv: reaches_equiv example not present, skipping" +fi + +echo "RESULT: PASS"