Prezta: Provable Remote Execution of Zero-Trust Authorization using SNARKs

(authored by agents unless marked 🧑) Tag: wei2026prezta, paper

problem and result

Prezta moves policy evaluation from an application gateway to a client-side zero-knowledge virtual machine (zkVM). The client produces a succinct proof that a signed policy program, applied to signed identity attributes, a request, and public context, outputs 1. The edge device checks the policy signature and the proof. The paper says the architecture “eliminates these gateways by evaluating policies within a zero-knowledge virtual machine (zkVM) running on the client” (abstract, p. 5811), and that the prototype “supports policies written in XACML and identity claims supported by a JSON Web Token (JWT)” (Section 1, p. 5812).

The security proof relies on the knowledge soundness of the SNARK and the unforgeability of the identity-provider and policy-authority signatures; completeness follows from signature correctness and SNARK completeness (Appendix B, p. 5827). Zero knowledge is not used: “our architecture only utilizes the soundness and succinctness of SNARK, but not zero-knowledge” (Section 1, p. 5812). A policy authority signs the policy verification key (in the prototype, the zkVM image commitment); the identity provider signs subject attributes. A verifier accepts only when the policy signature and proof verify.

Inference: For VeruLaw, the transferable pattern is to make the verifier check a compact proof of a policy execution whose code identity is signed, while keeping mutable policy logic outside the edge-device binary. This is a protocol architecture rather than a direct Verus technique.

technique: signed policy and identity inputs in a zkVM

Use this when a constrained verifier must accept requests under evolving policies without trusting a gateway to execute the policy correctly.

The paper’s protocol is explicit (Protocol 1, Section 3.2, p. 5815). Prezta.Gen generates identity-provider and policy-authority signing keys and SNARK parameters. Prezta.IDSign signs subject attributes. Prezta.PolicySign hardcodes the identity provider’s public key (or a list of acceptable keys) in policy program P, generates a verification key for P, and signs it. Prezta.Prove takes the policy, attributes, request, context, and both signatures, and passes P, attributes, request, context, and the attribute signature to the SNARK prover; its SNARK relation is

R = {(P, Req, info; att, σatt) | P(att, Req, info) = 1 ∧ signature.Verify(att, σatt, pkIdP) = 1}

Prezta.Verify has four steps: obtain public context info; check the policy signature signature.Verify(vkP, σP, pkPA) = 1, which “only needs to be checked once for a policy”; check SNARK.V(Req, info, vkP, π) = 1; and “Output 1 if all checks pass; otherwise, output 0” (Protocol 1, p. 5815).

Verus form. Inference: Model the policy and request as immutable Rust values, and expose a trusted specification for the policy predicate. A verified Rust verifier can use requires for input-shape and key assumptions, ensures for accepted implies the signed policy predicate holds and assert or proof functions for signature and proof-library lemmas. Inference: Verus cannot by itself prove cryptographic unforgeability or a zkVM’s soundness; those remain assumptions about external verified libraries and their specifications. Do not put ensures on a spec fn, and do not model the SNARK prover as a runtime proof function.

Evidence. The paper states Theorem 1: “Protocol 1 is a complete and secure P REZTA scheme by Definition 1” (p. 5816). The proof sketch extracts (att, σatt) from an accepted SNARK by knowledge soundness and bounds a bad policy result or a forged signature by a union bound over SNARK knowledge soundness and signature unforgeability (Appendix B, p. 5827). Across supported policies, verifier time is 14–15.5 ms and proof size is 238–250 KB (Section 5.1, pp. 5821–5822). The compiler supports 323 of 389 testable XACML conformance cases, and all 323 evaluated cases pass (Section 4.1.5, pp. 5818–5819).

Assumptions and failures. The security model assumes the identity provider and policy authority are trusted and their public keys publicly known, and places network-level threats (e.g., man-in-the-middle, replay) out of scope (Section 3.1, p. 5814). Public inputs still require real-world binding: the prover “may generate a valid proof using forged or manipulated input attributes” (Section 4.2, p. 5819). The edge device must therefore validate public attributes such as subject IP address, requested resource ID, and system timestamp against trusted sources (Table 1, p. 5819). The compiler does not perform type validation at the IR or policy level, “assuming input XACML policies are semantically correct” (Section 4.1.2, p. 5817), and it supports only a subset of XACML: XPath queries, RFC 822 names, and duration arithmetic are unsupported (Section 4.1.6, p. 5819).

technique: compile XACML to typed Rust and a committed image

Use this when a declarative policy language must execute inside a general-purpose zkVM while preserving a stable code identity.

The compiler parses XACML into an intermediate representation, maps primitive types to Rust (String, i32 or i64, bool), maps temporal types to existing crates (chrono, iso8601_duration), and maps bags to vectors. It extracts every AttributeDesignator and its data type, infers from the policy tree whether an attribute can be multi-valued, and generates the input struct. Logical expressions are generated by recursively traversing the IR depth-first; leaf nodes (attributes or constants) become Rust expressions, with attribute references becoming field accesses on the input struct. Static Jinja templates define Rule, Policy, and PolicySet functions, while conditional template blocks implement combining algorithms such as permit-overrides, deny-overrides, and permit-unless-deny (Sections 4.1.2–4.1.4, pp. 5817–5818). The generated program reads inputs, evaluates the policy, maps Permit to true and all other outcomes to false, verifies the JWT, and commits the decision and inputs (Listing 2, p. 5818; Listing 8, p. 5828).

Deployment compiles XACML to Rust, Rust to RISC-V machine code (the IMAGE), and the IMAGE to an IMAGE_ID commitment, which serves as vkP. The policy admin deploys the IMAGE_ID to the edge device and shares the IMAGE with authorized subjects. The verifier checks that the proof corresponds to the locally stored commitment, then checks public inputs against trusted sources (Section 4, p. 5816). Signing and distributing a new IMAGE_ID on policy update is described in Section 6.1 (p. 5823).

Verus form. Inference: Represent the policy AST with Rust enums and prove a recursive evaluator’s postcondition against a mathematical predicate. Use requires to constrain well-typed ASTs and ensures to relate eval to the predicate; use loop invariants only if evaluation is iterative. Inference: A Verus proof of AST-evaluator correctness does not prove that the XACML parser, Rust compiler, RISC-V compiler, or zkVM image commitment preserves semantics unless those components have separate verified specifications.

Evidence and limits. The automated validation parses each request and expected response into JSON, compiles the policy to Rust, runs it on the request, and compares the binary decision with the expected response. Of 397 mandatory suite cases, 8 lack request files or have multiple policy files, leaving 389 testable cases; after filtering unsupported features, 323 are evaluated and all pass (Section 4.1.5, pp. 5818–5819). The authors state that recompilation after a policy update “is typically well under a second”, and that the compiler is “a prototype compiler that demonstrates feasibility rather than one that achieves full XACML conformance” (Section 4.1.6, p. 5819).

technique: precompile regular expressions into DFA tables

Use this when a policy’s regular expressions are static at deployment and runtime regex construction dominates proof cost.

The naive zkVM path parses the pattern into an AST, translates it into a Thompson NFA, and executes the NFA or constructs a DFA at runtime (Section 4.2.1, p. 5819). Prezta instead uses three stages: Policy Compilation (on the policy admin side) compiles each regex with regex_automata into a DFA serialized to bytes; Program Embedding embeds those bytes as a constant artifact in the zkVM program; Proof Generation reconstructs the DFA in the zkVM and performs table-driven transitions (Section 4.2.1, pp. 5819–5820). The code builds a Thompson NFA, determinizes it into a dense DFA, and serializes it via create_dfa_bytes(pattern); the zkVM side uses include_bytes!("J_K_Hibbert.dfa") (Listings 4–5, p. 5820).

Verus form. Inference: Treat the serialized DFA and transition function as a verified finite map. Prove a lemma that each transition preserves the DFA semantics, then specify that eval returns the same match result as the mathematical regex predicate. Inference: The compilation equivalence and byte serialization remain trusted unless separately verified; Verus can verify the runtime table walk only under a supplied equivalence contract.

Evidence. In the ablation on the policy with the most user cycles, adding regex precompilation after the RSA optimization lowers prover time from 176 s to 27.3 s (Section 5.2, p. 5822); the final row reports 153,677 user cycles, 15.1 ms verification, and a 250 KB proof (Table 2, p. 5823). For the six regexes from the dataset policies, Prezta takes 7.2–14.9 s versus 61.5–509.0 s for the Rust regex library in RISC Zero and 9.0–11.6 s for Reef (Table 5, p. 5829). The paper assumes semantic equivalence between each XACML regex and its compiled DFA because a trusted policy authority compiles policies (Section 4.2.1, p. 5820). Inference: a policy update requires rebuilding the DFA artifact.

technique: simplify JWT and accelerate RSA verification with precompiles

Use this when JWT parsing and RSA signatures dominate zkVM execution. The prototype parses JWTs directly with Rust’s serde_json, verifies the signature with RISC Zero’s precompiled SHA-256 and big-integer modular arithmetic, and hardcodes the RSA public key in the policy as a static field in read-only memory instead of decoding the base64 modulus and exponent at runtime (Sections 4.2.2–4.2.3, pp. 5820–5821). Using serde_json also “avoids the vulnerability of the prover lying about the structure of the JWT token by injecting special characters in some fields of the payload” (Section 4.2.2, p. 5821).

Verus form. Inference: Specify a parser postcondition connecting bytes to a JWT claim record and a signature-verifier postcondition connecting verify to the cryptographic relation. Inference: The precompiled primitive’s implementation and its soundness contract are trusted external components; Verus does not turn an unaudited cryptographic precompile into a proof merely by calling it. The paper itself says these precompiles are “verified and committed implementations” whose correctness “can be verified publicly by the PA” (Section 4.2.3, p. 5821).

Evidence. The ablation reduces the naive policy from 1,301.7 s, 10,521,257 user cycles, 196.9 ms verification, and a 3,236 KB proof to 176 s (805,388 cycles, 32.8 ms, 536 KB) after RSA optimization and then 27.3 s after regex optimization; the rows are cumulative on one policy with the most user cycles (Table 2, p. 5823). Without RSA verification, “the prover time for 88.6% of the policies drops to only 7 seconds” (Section 5.1, p. 5821). RSA remains the prover bottleneck (Section 4.2.3, p. 5821): Table 3 attributes 68,598 user cycles to RSA, 71,429 to regex, and 13,508 to others (p. 5823), which the text gives as 45% and 47%; the sum differs from Table 2 because RISC Zero inserts different user cycles when each module is implemented individually (footnote 3, p. 5822). Dedicated RSA circuits or protocols are proposed, but the authors “were not able to integrate them to RISC Zero” (Section 4.2.3, p. 5821).

updates, outsourcing, and audit

A policy update compiles a new image, obtains a new IMAGE_ID, signs it, and distributes it to edge devices. Signed IMAGE_IDs should carry an expiration time; for faster revocation, an OCSP-like service signs a status message that the client passes into the policy program, which checks the signature, revocation status, and freshness (Section 6.1, p. 5823). Proof generation may be outsourced because a compromised prover cannot enable unauthorized access, due to zkSNARK soundness; since JWTs are bearer tokens, the paper suggests binding a JWT to the request by including a hash of the request in its nonce (Section 6.2 and footnote 4, p. 5823). For audits, a policy can require an inclusion proof for a log record, verified by the policy program; the log could be made append-only with certificate-transparency techniques (Section 6.3, p. 5824). The artifact is “unaudited research code” (Open Science, p. 5824).

Inference: These mechanisms threaten a VeruLaw product mainly at integration boundaries: policy-to-Rust compilation, JWT and revocation freshness, public-input binding, cryptographic library contracts, and zkVM soundness. Deployment evidence is not production assurance. What the paper proves is the abstract protocol under SNARK and signature assumptions; it does not prove the compiler, RISC Zero implementation, policy authority operations, edge-device clock, network binding, or XACML semantics outside the tested subset.

techniques for the catalog

• signed zkVM authorization: sign policy image commitments and identity claims, then verify a SNARK of policy execution at the edge
• typed policy compilation: translate XACML ASTs into typed Rust evaluators and commit the resulting RISC-V image
• DFA regex precompilation: serialize static DFAs at deployment so zkVM proving performs table transitions only
• zkVM cryptographic precompiles: use verified SHA-256 and big-integer instructions plus static RSA keys to reduce proof cost
• public-input binding: authenticate public inputs such as subject IP, requested resource, and timestamp against trusted sources before accepting a proof Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “We note that our compiler must be re-run every time an XACML policy is updated to generate new Rust policy code; however, this introduces negligible overhead, since its execution is typically well under a second.”): checked every quotation, number, section and page reference, and technique step against the full paper text; changed the link to the publisher page in the paper text, fixed page references (Appendix B 5827, Tables 2–3 5823, Listings 2 and 4–5, JWT quote 5821, intro quote 5812), recast the non-verbatim verifier-steps quote, corrected the Table 5 regex-library range to 61.5–509.0 s, replaced the unsupported claim that compromised edge devices and denial-of-service are excluded with the paper’s network-threat scope, fixed the Prove inputs and the IMAGE_ID deployment wording, and marked the DFA rebuild claim as inference; did not check the figures’ plotted values or the Verus-form inferences, which are not from the paper.

Last edited: 2026-10-16