arXiv CSopen access

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

Prezta: Provable Remote Execution of Zero-Trust Authorization using SNARKs Zhongjing Wei* University of Illinois Urbana-Champaign [email protected]

Osaid Muhammad Ameer* University of Illinois Urbana-Champaign [email protected]

Yupeng Zhang University of Illinois Urbana-Champaign [email protected]

Nikita Borisov University of Illinois Urbana-Champaign [email protected]

arXiv:2607.11466v1 [cs.CR] 13 Jul 2026

Abstract Modernizing the security of operational technology systems that control critical infrastructure has become a pressing challenge. Because edge devices have limited capabilities, modernization has relied on application gateways that interface with identity management systems and enforce access policies. These gateways are powerful enough to perform complex authorization decisions and support zero-trust architectures but create major deployment and management burdens: they must be collocated with remote, distributed edge devices, kept up to date with security patches, and managed with minimal downtime. We propose Provable Remote Execution of Zero-Trust Authorization (P REZTA), an architecture that eliminates these gateways by evaluating policies within a zero-knowledge virtual machine (zkVM) running on the client. The zkVM produces a succinct proof of authorization that edge devices can verify efficiently, extending the zero-trust security envelope to the edge. Policies and identity management schemes can evolve without updating edge devices. To demonstrate the feasibility of P REZTA, we implement a prototype, built using the RISC Zero zkVM, that supports XACML 3.0 policies and JWT identity claims. While zkVMs introduce substantial proof overhead, we mitigate this by compiling policies to Rust code and pre-compiling regular expressions. Combined with optimized signature verification and JWT parsing, these measures reduce prover time by more than an order of magnitude. Our compiler correctly implements 83% of the XACML 3.0 conformance suite, with proof generation completing in tens of seconds on a desktop. Verification, by contrast, takes only tens of milliseconds—fast enough for even resource-constrained edge devices.

1

Introduction

Operational technology (OT) networks [49] provide a networked interface to physical devices, such as those used in * * The authors contribute equally to this paper.

manufacturing, energy systems, and various forms of infrastructure, from water treatment to traffic control. Devices in these networks typically have rudimentary built-in security protections, owing to their limited computational capabilities and upgrade cycles that can range to several decades [43]. Yet the security of many of these systems is paramount due to the critical importance of the systems and infrastructure that they monitor and control [32, 34]. This has led to efforts to extend modern security practices and, in particular, zero-trust architectures [45], to OT networks [30, 36, 42]. A key tool in this effort has been the use of application gateways. These gateways implement modern security practices, such as the use of sophisticated role- and attribute-based policies [28, 47], and interfacing with identity management systems that can implement two-factor authentication. These gateways, however, become a critical component, and their failures or compromise can result in a loss of availability or a security breach, respectively. The network linking the gateways to OT devices is implicitly trusted, so in distributed infrastructure, many gateways are needed to collocate them with the OT devices. This creates a significant management problem, where gateways must be kept secured, patched against vulnerabilities, and available. Our Contributions. To mitigate this management problem, we propose an alternate architecture, Provable Remote Execution of Zero-Trust Authorization, or P REZTA1 . Rather than having gateways evaluate complex authorization policies, they are instead executed remotely (typically at the client) inside a zero-knowledge virtual machine (zkVM) [6, 12, 13]. The zkVM produces a succinct proof, also known as a SNARK, that the policy was correctly evaluated and that an access request is correctly authorized, which can be verified at a very low computational cost. This puts policy enforcement within reach of even low-capability OT devices. Moreover, the flexibility of zkVM means that new policies, policy types, and identity management systems, can all be introduced without 1 Our code is available at https://github.com/walotta/ZK_Zero_

Trust and https://github.com/osaidameer/xacml-to-rust

any upgrades to the policy enforcement system. We formalize the algorithms and the security definitions of P REZTA, develop our construction, and prove its security based on the knowledge soundness of the SNARK and the unforgeability of the digital signature. See Section 3 for more details. Note that our architecture only utilizes the soundness and succinctness of SNARK, but not zero-knowledge. In fact, the term “zkVM” refers to a SNARK for a virtual machine not necessarily with zero-knowledge as a convention in the community. To demonstrate the feasibility of P REZTA, we have developed a prototype implementation based on the Risc Zero zkVM [6]. Our prototype supports policies written in XACML [37] and identity claims supported by a JSON Web Token (JWT) [29]. We compile the XACML policies directly to Rust programs that make policy decisions. The programs take as input an access request, a JWT, and context attributes, and produce a decision. The Risc Zero tools then compile and execute the programs inside the zkVM, producing a proof of authorization. The proof can then be used to verify that a request is authorized. The verification confirms that the correct policy program was executed on the correct inputs and produced the correct output. Our compiler supports most of the XACML 3.0 conformance suite [8]. The use of zkVM to execute the policies does introduce significant overhead, and we therefore explored several optimizations in our implementation. We optimize regular expression evaluation by precompiling and serializing the corresponding DFA; we also simplify JWT parsing and use precompiled bigint operations for RSA verifications. Together, these reduce the zkVM execution time, needed to produce a SNARK, from about 20 minutes to under 30 seconds. The cost remains dominated by the RSA verification, so using state-of-the-art RSA verification circuits [50] the policy execution can be lowered to a median of 7 seconds on our test set. Our contributions are summarized below: • We propose a new architecture, P REZTA, for authorizations in OT systems utilizing SNARKs and digital signatures. Our architecture allows OT devices to support complex policies with limited computational resources, and to update policy and identification frameworks without software upgrades on the devices. • We formalize our architecture with security definitions, and prove that our construction is secure based on the security of SNARKs and digital signatures. • We instantiate the SNARK with a zkVM [6], and we build a compiler that automatically compiles policies in XACML to Rust, which is supported by the zkVM. Our compiler is able to support 323 out of 389 test cases in the XACML 3.0 conformance suite. • We propose/integrate several optimizations to improve the prover time of the zkVM for the authorization policies. We

propose a new method to efficiently check regular expressions in zkVM. We also utilize an existing library for JWT parsing, and the precompiled instructions of bigint for RSA signature verification in zkVM. These optimizations improve the prover speed by nearly 50×. • Finally, we fully implement P REZTA and the end-to-end prover time of most policies in the dataset is around 28 seconds. The prover time can be potentially reduced to around 7 seconds with a special proof for RSA signature verification outside zkVM. With ongoing efforts to improve zkVM performance [5], we believe the prover time can become very practical in the near future.

1.1

Related Work

Zero-knowledge proofs have been long used for authentication in the context of anonymous credentials [17, 20]. These systems would allow a client to prove a predicate over attributes in their credential while remaining anonymous. Anonymous credentials have traditionally been implemented using custom zero-knowledge proofs which are relatively expensive to verify and lack the flexibility of our architecture. Several recent papers have used zkSNARKs to bootstrap anonymous credentials from traditional, identityrevealing ones [46], frequently targeting blockchain applications [1, 10, 41]. The focus is largely on identification, and supporting unlinkability, whereas our focus is on supporting flexible and evolvable authorization policies, and not privacy, and our target is OT networks and devices. Another novel aspect of our work is the use of zkVMs for greater policy flexibility and ease of implementation, as compared with circuitbased SNARKs in the previous work. There is some early work on using zkVMs for authorization and authentication; Moser et al. [35] proposed a scheme using zkVM to verify digital signatures to authorize smart contract operations on blockchain, while Bonsai Pay [2] is an application developed by Risc Zero to integrate OpenID with blockchain applications. These systems take a minute or longer to generate their proofs, highlighting the importance of our optimizations. A number of previous systems have proposed using a virtual machine to implement access restrictions [9, 16, 21]; their focus was largely on providing least-privilege in delegation contexts, rather than flexible policy implementation, and they used classic (non-verifiable) VMs, which would need to be run either at the end point or a trusted server, both of which are impractical in OT networks.

2 2.1

Preliminaries Application Gateways

Classically, operational technology (OT) environments relied on network isolation security as the primary security mechanism, with edge devices implementing rudimentary, if any,

Identity Provider

1 Authentication

Application Gateway

Policy Decision Point

2 Auth Token

Subject 3 Request, Auth Token

Policy Enforcement Point

Policy

Implicitly trusted

4 Authorized Request

Policy Authority

Edge Device

Figure 1: Zero Trust architecture security protections. Recent efforts to modernize security practices have included the deployment of zero-trust architectures, with sophisticated identity management and policies, to OT environments, with the help of application gateways. Such gateways bridge the isolated OT network and enterprise networks and/or the Internet. Requests sent from outside the OT network are intercepted by the gateway and checked for correspondence with a policy before being forwarded to the device. The policy can be sophisticated, such as RBAC, ABAC, and NGAC, and requests can be authenticated using sophisticated and modern identity management (IdM) systems, including reliance on an identity provider, the use of two-factor authentication, etc. The gateway thus enables modern zero-trust security practices, but it becomes a new critical component in the OT environment, as all interaction with OT devices must happen via the gateway. As a result, gateways must typically be deployed at every site in an OT environment, both to ensure availability during periods of remote disconnection, and to avoid extending insecure OT networks beyond the premises. At the same time, the gateways are security-critical, since a vulnerability in a gateway allows unrestricted access to the edge devices it protects; e.g., Cesarano and Natella catalog many previously discovered vulnerabilities in application gateways [22]. Thus, application gateways must be carefully managed and kept up-to-date on security patches, while at the same time minimizing downtime due to potential upgrades [44].

2.2

Zero-Trust Authorization Flow

To discuss the authorization flow, we will be using the following terms. Most of these are adapted from the Zero-Trust Architecture specification [45], but slightly adapted for presentation in our system.

device by sending it requests, such as a maintenance technician, or a monitoring service. We will typically assume that the subject is using a COTS computer system to initiate its requests. • An Identity Provider (IdP) authenticates subjects and assigns them identities, roles, or group membership, that can be used for authorization. The IdP issues the subject with an authentication token that can be used to prove their identity. • A Policy Authority (PA) sets an authorization policy for the system and makes updates to it as needed. • A Policy Decision Point (PDP) decides whether a request from a subject is authorized to perform a request. • A Policy Enforcement Point (PEP) interacts with the PDP to determine whether a request from a subject is properly authorized and takes action to either permit the request to reach the edge device, or block it. We describe the authorization flow in an application gateway, as shown in Figure 1. The PA specifies a policy and deploys it on the PDP, running inside the application gateway. The subject authenticates with the IdP and obtains a token, which is forwarded along with the request to the gateway. The PEP, also inside the gateway, communicates with the PDP and, based on the decision, either forwards the request through to the edge device or denies it. Note that beyond the PEP, no further authentication or authorizations are made, and the communication from the gateway is implicitly trusted by the edge device. Denied requests (or all requests) can be sent to an audit log (not shown); we discuss audit in Section 6.3. The PDP makes use of the following information when making a decision:

• An Edge Device is an OT component that performs or monitors a physical action. This could be a relay in an electric substation, a PLC controller for a manufacturing device, or a traffic sensor.

• Subject attributes, e.g., usernames, email addresses, roles, etc., as authenticated by the identity provider

• A Subject is an entity that needs to interact with the edge

• Edge device attributes, e.g., device type, location, or label

• Request attributes, e.g., requested operation, and parameters

• Context, e.g., the current date and time, or the IP address of the requester In some enterprise deployments of ZTA, the IdP and PDP are combined into a single identity and access manager (IAM) which issues an authorization token for a particular request. Involving an IAM at every request, however, is not appropriate for OT environments where delays and availability issues associated with IAM may prevent critical operation. Even the IdP need not be contacted with every request, as authentication tokens can be reused until their expiry. The expiration times are typically minutes to hours, but can be tuned to trade off the performance, availability, and security risks. JWT. In this paper, we use the JSON Web Tokens (JWT) as the authentication token, but our scheme can be generalized to other formats. A JWT consists of three fields: <Header>, <Payload>, <Signature>. The header includes the algorithm of the digital signature (e.g. RSA-SHA256) and other meta-data. The payload includes the subject’s role, user-group, issued timestamp and expiration timestamp. The signature is a digital signature signing both the header and the payload in base64. We use RSA-2048 and SHA-256 in this paper. An example of JWT is provided in Section 4.2.2.

2.3

Cryptographic Primitives

Digital signature. A digital signature scheme consists of the following algorithms: Gen(1λ ) → (sk, pk), Sign(m, sk) → σ, Verify(m, σ, pk) → {0, 1}. A signature scheme is correct if for all (sk, pk) ← Gen(1λ ), all σ ← Sign(m, sk), Verify(m, σ, pk) = 1. It is unforgeable if for all PPT adversary A , (sk, pk) ← Gen(1λ ), (m∗ , σ∗ ) ← A Sign(·) (pk), Pr[Verify(m∗ , σ∗ , pk) = 1 ∧ m∗ ∈ / Q] ≤ negl(λ), where Q is the set of messages queried to the signing oracle Sign(·). SNARK. A Succinct non-interactive argument of knowledge (SNARK) allows a prover to convince a verifier that a statement is true. It consists of three algorithms (G , P , V ), and satisfies completeness and soundness. See Appendix A for the formal definitions. In our construction, we instantiate the SNARK with a zkVM, which represents the relation by a program P. The statement is y = P(x, w), denoting the output of running the program on the input and the witness. zkVM also supports the generation of vkP for a program, and we abuse the notation to denote it as vkP ← G (1λ , P). In our construction, we use the zkVM of RISC Zero [6], the backend of which is STARK [11] with a transparent setup. Therefore, pk simply consists of a hash function and some public parameters that do not depend on P.

3

Architecture Design

In this section, we present the security definitions and the architecture of our new design, P REZTA. We also provide a generic construction using SNARKs and digital signatures.

3.1

Security Model

Security Model. We assume that the subject is untrusted and may be compromised by an adversary to make unauthorized access to the device. Both the IdP and the PA are assumed to be trusted and their public keys are publicly known. We do not consider adversaries that compromise the network communications. Network-level threats (e.g., man-in-the-middle, replay attacks) are defended against with orthogonal mechanisms and are out of the scope of this paper. Informally speaking, our P REZTA architecture guarantees that the subject is granted the access of the device if and only if the subject possesses a valid token issued by the IdP, and the subject’s attributes satisfy the policy authorized by the PA. We formally define P REZTA below: Definition 1. A P REZTA scheme is a tuple of algorithms: • Prezta.Gen(1λ ) → (skIdP , pkIdP , skPA , pkPA , pkSNARK ): the algorithm takes the security parameter as input, and outputs the pairs of secret key and public key of IdP and PA, as well as the public parameters of the SNARK. They can be generated separately, but we combine their generations into one algorithm for simplicity. • Prezta.IDSign(skIdP , att) → σatt : the algorithm is executed by the IdP. It takes the secret key of IdP and the attributes of the subject and outputs an authorization token. • Prezta.PolicySign(skPA , P) → (vkP , σP ): the algorithm is executed by the PA. It signs the access control policy of the edge device and outputs the verification key and the signature of the policy P. • Prezta.Prove(P, att, Req, info, σP , σatt , pkSNARK ) → π: the algorithm is executed by the subject. For a request Req to access the edge device, the algorithm takes as input the policy, the subject’s attributes, the subject’s token, the signature of the policy and other public information, and computes a proof. Here info denotes device attributes (e.g., type, location) and context (e.g., date, IP address). • Prezta.Verify(π, Req, info, vkP , σP , pkPA ) → {0, 1}: upon receiving a request together with a proof, the system runs this verification algorithm and outputs 0 or 1. Completeness. A P REZTA scheme is complete if for all (skIdP , pkIdP , skPA , pkPA , pkSNARK ) ← Prezta.Gen(1λ ), σatt ← Prezta.IDSign(skIdP , att), (vkP , σP ) ← Prezta.PolicySign(skPA , P):   P(att, Req, info) = 1∧  π ← Prezta.Prove(P, att, Req, info,   = 1, Pr    σP , σatt , pkSNARK ) : Prezta.Verify(π, Req, info, vkP , σP , pkPA ) = 1 where P(att, Req, info) denotes the output of the policy on the request, the subject’s attributes and the public information.

Identity Provider

Policy Authority

1 Authentication 2 Auth Token 3 Signed Policy

zkVM

6 Verification

PDP 4 zkSNARK Generation

PEP 5 Request, Context, Proof

Subject

Edge Device

Figure 2: Our new P REZTA architecture Security. A P REZTA scheme is secure if for any PPT adversary A , for any (skIdP , pkIdP , skPA , pkPA , pkSNARK ) ← Prezta.Gen(1λ ). the following probability is ≤ negl(λ):   (Req, att, σatt , π, P, vkP , σP ) ← A IDSign(·),PolicySign(·) (  pkIdP , pkPA , pkSNARK ),     : (Prezta.Verify(π, Req, info, vkP , σP , pk ) = 1  PA   Pr   and P(att, Req, info) = ̸ 1)    ∨(Verify(att, σatt , pkIdP ) = 1 and att ∈  / Qatt ) ∨(Verify(vkP , σP , pkPA ) = 1 and vkP ∈ / QP ). where Qatt is the set of messages queried to the signing oracle IDSign(·), and QP is the set of messages queried to PolicySign(·). Unlinkability. An additional property that can be achieved by our design is the unlinkability of the access requests. This can be enabled by the zero-knowledge property of the zkSNARK, and by changing the algorithms to hide some information in Req and info such as the IP address of the subject. We primarily focus on the security of the P REZTA scheme and leave the formal definition and construction of unlinkability as a future work.

3.2

Our P REZTA System

Our new P REZTA architecture is presented in Figure 2, and the generic protocol of our scheme is presented in Protocol 1. It utilizes the SNARK scheme and the digital signature scheme as defined in Section 2. As shown in the figure, we completely remove the gateway from the architecture, and utilize SNARK to enforce the policy. The overhead of policy evaluation and proof generation is shifted to the subject, thus addressing the update and maintenance issues of gateways and edge devices in the existing zero trust architecture (Figure 1). In the protocol, we hardcode pkIdP , or a list of acceptable public keys of IdPs, in the policy, which is signed by the PA. We can also make pkIdP as a public input known by the edge device, and there is no essential difference between the two choices.

Protocol 1 (P REZTA scheme). • Prezta.Gen(1λ ) → (skIdP , pkIdP , skPA , pkPA , pkSNARK ) 1. (skIdP , pkIdP ) ← signature.Gen(1λ ) 2. (skPA , pkPA ) ← signature.Gen(1λ ) 3. pkSNARK ← SNARK.G (1λ ) • Prezta.IDSign(skIdP , att) → σatt 1. σatt ← Sign(att, skIdP ) • Prezta.PolicySign(skPA , P) → (vkP , σP ) 1. P hardcodes pkIdP , or a list of acceptable public keys of IdPs. 2. vkP ← SNARK.G (1λ , P) 3. σP ← Sign(vkP , skPA ) • Prezta.Prove(P, att, Req, info, σP , σatt , pkSNARK ) → π 1. π ← P (P, att, Req, info, σatt , pkSNARK ) where the statement of the SNARK is R = {(P, Req, info; att, σatt )|P(att, Req, info) = 1 ∧ signature.Verify(att, σatt , pkIdP ) = 1}. • Prezta.Verify(π, Req, info, vkP , σP , pkPA ) → {0, 1} 1. Obtain info 2. Check if signature.Verify(vkP , σP , pkPA ) = 1. This only needs to be checked once for a policy. 3. Check if SNARK.V (Req, info, vkP , π) = 1 4. Output 1 if all checks pass; otherwise, output 0.

In Appendix B, we provide a proof sketch for the following theorem:

Theorem 1. Protocol 1 is a complete and secure P REZTA scheme by Definition 1.

4

System Design

Following the generic construction in the previous section, we further present the detailed design of P REZTA to make it concretely efficient in practice. We instantiate the zkSNARK with a zkVM. The primary motivation for adopting a zkVM rather than designing custom circuits is that the authorization logic involves several components with high implementation complexity, including regular-expression based string matching, JSON Web Token (JWT) parsing, and RSA signature verification. Constructing hand-optimized circuits for such components is cumbersome, error-prone, and expensive to maintain, especially when policy rules evolve frequently. A zkVM allows us to directly reuse well-engineered library implementations of these components in Rust, maintaining high code readability, auditability, and testability. At the same time, with targeted optimizations on these components (detailed in Section 4.2), the zkVM proving overhead is significantly reduced, making its proving cost comparable to that of tailored circuits for our authorization workloads. This design enables both practical deployment and security soundness without sacrificing performance. Due to the use of zkVM, in particular RISC Zero [6], the policy will be compiled to a Rust code at the first step; then the Rust code will be converted to machine code (RISC-V in our case. This machine code is called the IMAGE) and the zkVM module will also output a commitment of machine code (this commitment is called the IMAGE_ID). The commitment serves as vkP defined previously, and when performing the verification, the verifier will check if the proof is aligned with the commitment of machine code. This technology can ensure the code in zkVM is identical to the trusted policy logic approved by the policy authority, thus the subject cannot change the policy. The P REZTA system works in three main stages: 1. Policy Deployment: The policy admin compiles the authorization policy in XACML format into Rust code, which is further compiled into RISC-V machine code (IMAGE). A commitment to this machine code (IMAGE_ID) is generated for later verification. Then the policy admin deploys the IMAGE_ID to the edge device, which stores it for future access requests. Also the policy admin will share the policy code (IMAGE) with authorized subjects who may request access to resources protected by this policy. 2. Proof Generation: When a subject requests access to a resource, they provide their attributes (e.g., JWT token, source IP address), environment attributes (e.g., current Unix timestamp) and request context (e.g., requested resource ID and request operation) to the zkVM along with

the compiled policy IMAGE. The zkVM executes the policy logic using these attributes and generates a zeroknowledge proof attesting that the access decision is computed correctly according to the policy. Then the subject sends the access request and the generated proof to the edge device for verification. 3. Proof Verification: The edge device receives the subject’s access request and the generated proof. It first verifies that the proof corresponds to the committed machine code (IMAGE_ID) ) stored locally during policy deployment. Then, it checks the authenticity of all public input attributes against trusted sources before accepting the proof and making the final access decision. These checks include consistency tests between subject-provided values and verifier-observable data when applicable.

4.1

Policy Compiler

To enable verifiable evaluation of XACML policies in constrained OT environments, we developed a policy compiler that translates XACML policies directly into Rust. The resulting programs take the request and context as input and output whether the source XACML policy would have permitted or denied access. The programs can then be compiled into RISC-V code that can produce a verifiable execution in the Risc Zero virtual machine. The entire flow is illustrated in Figure 3. 4.1.1

XACML Background

Before diving into the compiler and its design, we first provide some background on XACML itself. The eXtensible Access Control Markup Language (XACML), is an OASIS standard which is designed to express fine-grained, attribute-based access control policies. XACML enables the combination of role-based permissions with attribute-based evaluation of requests, for example, characteristics of the subject (e.g. role, department), the resource (e.g file type, sensitivity level), the action (e.g. read, write) and the environment (e.g. time of day, network location). At a high level, XACML policies consist of the following elements: • PolicySet: A container that groups policies or other policy sets, defining how their decisions are combined. • Policy: A container that groups rules and defines the overall structure of the authorization logic. • Rule: This is the smallest unit of decision-making in a policy. It typically consists of an effect (e.g. Permit or Deny) and logic determining when that effect applies. • Target: This is a filtering mechanism inside a rule or policy that defines to which request a policy or rule applies. This enables quick filtering of applicable policies/rules.

• Condition: A boolean expression that evaluates to true for a rule to apply.

XACML

• Combining Algorithm: These are strategies for resolving conflicts when multiple rules, policies, or policy sets apply; e.g., deny-overrides or permit-overrides.

Intermediate Representation Rust Code

Together, these components enable XACML to express complex authorization logic while remaining structured and declarative. Listing 1 shows a simplified XACML policy that permits physicians to read a specific patient record, demonstrating how targets and rules are structured in practice.2 Listing 1 ALFA version of an XACML Policy namespace example.policies { policy A001_policy { apply deny-overrides; rule IIA003_rule permit { target subject.bogus == "Physician" and resource.resource_id == "http://medico.com/record/pati ⌋ ,→ ent/BartSimpson" and (action.action_id == "read" or ,→ action.action_id == "write"); } } // Attribute definitions // ... }

RISC-V Binary JWT Req. Attributes

Type System and Mapping

XACML’s type system includes primitives (string, integer, boolean, double), temporal types (date, time, dateTime), durations (dayTimeDuration, yearMonthDuration) and other specialized types. Our compiler maps these to appropriate Rust types: strings map to String, integers to i32 or i64, booleans to bool, and temporal types leverage existing crates (chrono for date/time types, iso8601_duration for duration parsing). Multi-valued attributes (known as bags in XACML terminology) are represented as Rust vectors (e.g. Vec<String>, Vec<i32>). The Input struct is generated dynamically based on all attributes referenced in the policy, with fields strongly typed according to their declared XACML data type. Type safety is currently enforced at compile time, where the Rust compiler validates that all comparisons and operations are type-correct, catching any inconsistencies introduced during code generation. At runtime, the host program is responsible for providing 2 Our compiler works directly with XACML policies, but for ease of readability, we show policies using the ALFA syntax [18], which is much more compact than XACML. ALFA can be compiled directly to XACML using existing tools.

Decision Req. Attributes

zkVM Environment

Figure 3: End-to-end pipeline from XACML policy to verifiable execution in zkVM. Compilation stages (blue) transform the policy into executable code, while runtime stages (green) execute within the zkVM environment with request attributes and JWT (yellow) as inputs, with the decision and respective request attributes (orange) as output.

the correctly-typed inputs matching the policy’s expectations. Since proof generation requires valid execution, malformed or mistyped inputs will simply fail to produce a valid proof. We do not currently perform type validation at the IR or policy level, assuming input XACML policies are semantically correct. 4.1.3

4.1.2

Guest Program Execution

Expression and Code Generation

Logical expressions, including conditions and targets, are generated by recursively traversing the IR. Each operator is mapped to a handler that emits typed Rust code, with handlers recursively processing child nodes in a depth-first manner. This approach naturally mirrors the tree structure of logical expressions in XACML. Leaf nodes—attributes or constants—are converted into Rust expressions with appropriate type handling. Attribute references are transformed into field accesses on the input structure, with insertion of parsing logic where required for complex data types (e.g. temporal, durations). Static Jinja templates define the structure of Rule, Policy, and PolicySet functions. Using templates is a design choice that follows the natural structure and hierarchical nature of operations in XACML, resulting in verifiable, deterministic, and human-readable code. These templates function as boilerplate structures of XACML policies, while the expressions inside these structures are dynamically generated, dependent on the logic enclosed in the particular policy. Combining-algorithm logic is also embedded within these templates through conditional blocks. The Compiler supports all standard XACML 3.0 combining algorithms, such as permit-overrides, in which a single Permit decision over-

rides the results of all sibling policies or rules; its counterpart, deny-overrides, where a single Deny decision takes precedence; and permit-unless-deny, which yields an overall Permit decision unless any child element evaluates to Deny. These implementations follow advice from the XACML 3.0 specification document [37], and exist as distinct code paths within the template, selected dynamically based on the policy’s specified combining algorithm. The same template structure applies to both policy-level rule combination and policyset-level policy combination, with the exception of the only-one-applicable combining algorithm which only applies to PolicySets. Listing 2 shows the Rust code generated from the sample policy in Listing 1, illustrating how the hierarchical policy structure is translated into a series of evaluation functions. The complete code and policy are provided in Appendix D. Listing 2 Rust code generated from policy defined in Listing 1, illustrating rule evaluation. Combining logic and auxiliary functions are omitted for brevity, complete code and policy are included in Appendix D // {omitted imports and jwt functions} fn evaluate_rule_target(inp: &Inputs) -> bool { (("Physician" == inp.access_subject_bogus) && ("http://medico.com/record/patient/Bart ⌋ ,→ Simpson" == inp.resource_resource_id) && (("read" == inp.action_action_id) || ,→ ("write" == inp.action_action_id))) } fn evaluate_rule(inp: &Inputs) -> Result { if !evaluate_rule_target(inp) { return Result::NotApplicable; } return Result::Permit; } fn evaluate_policy(inp: &Inputs) -> Result { // {omitted target evaluation + combining ,→ algorithm logic} } fn main() { let inp: Inputs = env::read(); let mut decision = match evaluate_policy(&inp) ,→ { Result::Permit => true, _ => false, }; // {omitted jwt verification} env::commit(&decision); env::commit(&inp); }

4.1.4

Input/Output

XACML policies, while defining static values to be used in comparisons, also strictly define what fields and their respec-

tive data types are expected in the access request. The Compiler leverages this to dynamically define an input structure for each policy. This is accomplished by parsing the policy file, extracting all the AttributeDesignator elements (which specifies which attributes the policy expects to be present in a request) and their data types. The structure of the policy tree is analyzed to determine whether an attribute could be multivalued (a bag in XACML terminology), in which case it is defined as a vector in the generated Rust code. This approach ensures that the input structure precisely matches the policy’s requirements, allowing a request to be read by a host program and passed directly as input to the guest policy code. Alongside establishing the request structure, the policy evaluator must also validate that the request originates from an authenticated source. Since our architecture removes traditional components such as the Policy Enforcement Point or Application Gateways, we must supplement our policy evaluator with request-validation capabilities. Each policy program accepts a JWT (our chosen authentication token), which acts as the source of subject attributes as defined in Section 2.2, decodes the contents, verifies its signature, and ensures that the subject from the token matches the subject of the request. In our current prototype, the public key of the Identity Provider, used for JWT verification, is embedded into the policy program at compile time. The decision output is simplified to a binary outcome, where a regular Permit maps to true, while NotApplicable, Deny, and Indeterminate map to false. This simplification is intentional, as our architecture is primarily concerned with whether requests are correctly authorized or denied according to the policy. While NotApplicable and Indeterminate represent aspects of policy evaluation logic rather than explicit access outcomes, their distinction is less critical to our binary authorization model. Nevertheless, the compiler does retain support for XACML’s extended result functionality should more granular decision information be needed in future work, and to support the correct implementation of combining algorithms. 4.1.5

Validation

We validate our compiler using the XACML 3.0 conformance test suite [8], which contains 397 mandatory test cases. Each test case in the suite contains three files: policy.xml, request.xml, and response.xml (with a few exceptions). From these 397, 8 lack associated request files or have multiple policy files (linked through PolicyIdReference or PolicySetIdReference, an unsupported feature), leaving 389 testable cases. After filtering for unsupported features, we evaluate our Compiler on 323 policies. Since the test suite contains the appropriate responses for the specific request input, we can sufficiently validate our compiler implementation. Our validation process is fully automated, for each test case, both the request and expected response are parsed into JSON,

Table 1: Example attribute visibility and trusted binding source Attribute

Visibility

Binding Source

JWT JWT public key subject IP address Requested resource ID System timestamp

Private Public Public Public Public

-1 Committed with zkVM code Network stack Request context System clock

1 Private attributes are validated implicitly inside the zkVM (e.g., JWT claims

verified using signature).

the policy is compiled to Rust, which is finally executed with the test request as input and the resulting decision is compared against the expected response. We pre-process the the policy results to map to the true and false binary output we expect, as mentioned in Section 4.1.4. All 323 evaluated test cases pass successfully, demonstrating that the compiler correctly implements XACML semantics for the supported feature set.

4.1.6

Limitations and Scope

Our compiler implements most XACML functions—numeric, logical, string, set operations, and regular expressions. We did not implement certain functionality, such as XPath queries, RFC 822 names, or duration arithmetic, since our goal was a prototype compiler that demonstrates feasibility rather than one that achieves full XACML conformance. Nevertheless, the compiler supports a large majority of the conformance suite. A full list of unsupported XACML functions is provided in Appendix C for reference. 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.

4.2

zkVM and optimizations

We present the zkVM design and optimizations to make P REZTA efficient in this section. In P REZTA, the edge device cannot rely solely on a valid SNARK proof for authorization. The prover (i.e., the subject) may generate a valid proof using forged or manipulated input attributes. Therefore, the edge device must validate the authenticity of all public inputs before accepting the proof. To illustrate how different input attributes are treated in the P REZTA system, we classify them based on their visibility and required real-world binding, as summarized in Table 1. As we will demonstrate in the experiments, naively implementing the policies in zkVM would introduce a high overhead on the prover time. We introduce several optimizations to reduce the overhead significantly.

4.2.1

Regex

The first type of function with a high overhead is regular expressions. It appears in some of the policies to perform string match on the username. Listing 3 shows an example from case IIC057 in the XACML 3.0 conformance test suite to check the regular expression of J.* K.* Hibbert. The code was compiled naively into Rust using the Regex library. It executes the full regex engine to parse and match this pattern at the runtime. Listing 3 Default regex matching in Rust use regex::Regex; let is_match = Regex::new(r"J.* K.* Hibbert") .unwrap() .is_match("Julius K. Hibbert");

Running a generic Rust regex engine inside a zkVM significantly increases the prover time due to the heavy Nondeterministic/Deterministic Finite Automaton (NFA/DFA) construction and state transitions performed at runtime. In particular, the dynamic compilation of arbitrary user-provided patterns results in a substantial growth of the number of CPU cycles because the entire automaton evaluation logic must be represented in the zkVM. In particular, when running the example in Listing 3, the naive approach performs the following steps at runtime: 1. Parse the user-supplied regular expression into an abstract syntax tree (AST); 2. Translate the AST into an intermediate automaton representation (typically a Thompson NFA); 3. Execute the NFA (or construct a DFA) dynamically during pattern matching. When executed inside a zkVM, this entire workflow is recorded in the execution trace, including parsing, automaton construction, and state transitions. Since every step must be represented by arithmetic constraints in the proof system, dynamic pattern compilation leads to substantial constraint growth and proving overhead. Our approach. In P REZTA, the policy is statically known at the time of deployment. Therefore, regexes can be precompiled into deterministic finite automata (DFA), and the resulting transition tables can be embedded directly into the zkVM program as serialized binary artifacts. During proof generation, the zkVM performs only table-driven state transitions, eliminating both pattern parsing and automaton construction overhead. In particular, the workflow consists of three stages: 1. Policy Compilation (on policy admin side): Each regex pattern appearing in the XACML policy (e.g., J.* K.* Hibbert) is compiled into a deterministic finite automaton (DFA) using the regex_automata library. The DFA is then serialized into a compact byte array.

2. Program Embedding: The serialized DFA byte sequence is embedded as a constant artifact within the zkVM program (e.g., linked as a static data segment). No regex parsing or automaton construction is needed during execution. 3. Proof Generation (in zkVM): During execution, the zkVM simply reconstructs the DFA from the serialized bytes and performs table-driven transitions over the input string. Pattern parsing and NFA/DFA construction are eliminated.

Listing 5 Table-driven DFA evaluation inside zkVM use regex_automata::dfa::dense::DFA; // Statically embedded DFA artifact static DFA_BYTES: &[u8] = include_bytes!("J_K_Hibbert.dfa"); pub fn eval_name_attr(input: &str) -> bool { // Reconstruct DFA from bytes, no parsing let dfa = DFA::from_bytes(DFA_BYTES) .unwrap(); // Table-driven pattern matching return dfa.try_search_fwd(&input); }

Listing 4 DFA precompilation using regex_automata use regex_automata::{ dfa::dense::DFA, nfa::thompson, }; pub fn create_dfa_bytes(pattern: &str) -> Result<Vec<u8>, Box<dyn std::error::Error>> { // 1. Build Thompson NFA let nfa = thompson::NFA::compiler() .build(pattern)?; // 2. Determinize to a dense DFA let dfa = DFA::builder() .build_from_nfa(&nfa)?; // 3. Serialize DFA to a little-endian byte #[cfg(target_endian = "little")] let (bytes, pad) = dfa.to_bytes_little_endian(); assert_eq!(pad, 0); Ok(bytes.to_vec()) }

with input length and is decoupled from the complexity of the regular expression, significantly reducing the overhead. • Clear trust and correctness boundaries: Since the policies are compiled by a trusted policy authority, we assume semantic equivalence between the regular expression in the original XACML and its compiled DFA. The zkVM only needs to prove correct evaluation over a known DFA, not correctness of the compilation itself. This optimization reduces the number of executed RISC-V instructions and minimizes the volume of committed memory reads. As a result, it leads to fewer constraints and faster prover time, while retaining full correctness guarantees for regex-based attribute validation. 4.2.2

Implementation of DFA precompilation. We use the regex_automata library’s Thompson compiler and dense DFA builder to generate precompiled transition tables. The core Rust code is shown in Listing 4. During policy deployment, each regex pattern is passed to create_dfa_bytes, and the resulting byte vector is stored as a binary artifact (e.g., a .dfa file). For the pattern J.* K.* Hibbert, the deployed policy includes a serialized DFA encoding equivalent semantics. DFA reconstruction and evaluation in zkVM. Inside the zkVM, the DFA is reconstructed from its serialized form and used for deterministic, table-driven evaluation. Listing 5 illustrates this process. Compared to the naive implementation in Listing 3, this design achieves: • No runtime parsing or construction overhead: All regex parsing, AST construction, and DFA determinization occur in the trusted pre-deployment phase. The zkVM only executes deterministic transitions. • Reduced trace and constraint complexity: Matching becomes a fixed table lookup operation. The number of RISCV instructions and committed memory reads scales linearly

JWT Parsing

Another common gadget in the policies is the JWT parsing. Listing 6 shows an example of JWT. Listing 6 Example JWT used in P REZTA. header = { "alg": "RS256", "typ": "JWT", "kid": key_id, } payload = { "iss": "https://login.example.com/", "subject_id": "Julius Hibbert", "aud": "api://payments-service", "exp": "<current_time> + 3600", "iat": "<current_time>", "auth_time": "<current_time> - 100", "email": "[email protected]", "nonce": "3e4f0f67-bc5a-413d-b528-93fd1c71fd4e", "roles": "admin", }

Unlike prior works, such as zkLogin [10], that develop special protocols verifying the JWT parsing with auxiliary input provided by the prover, we directly use the serde_json

library in Rust. This is because we observe that implementing the special protocol in zkVM incurs a similar overhead to using the serde_json library, for common JWT tokens with no more than 10 fields in the payload. Moreover, directly using the serde_json library avoids the vulnerability of the prover lying about the structure of the JWT token by injecting special characters in some fields of the payload. 4.2.3

RSA Verification

Finally, another major overhead comes from the signature verification of the JWT. The RSA verification involves the SHA2 hashing of the header || ’.’ || payload string and modular exponentiations over the large RSA group. Naively implementing them in zkVM would result in the prover time of more than 1,000 seconds. In P REZTA, we utilize the pre-compiled system calls in the RISC Zero zkVM, including SHA-256 and big-integer modular arithmetic (sha2 and rsa in [4]), to improve the efficiency. These pre-compiled modules are verified and committed implementations of cryptographic primitives that are included in the zkVM’s instruction set. Their correctness can be verified publicly by the PA, and thus using these pre-compiled instructions do not alter the soundness of the proof. Additionally, we avoid the dynamic construction of RSA public key parameters. Instead of decoding the base64-encoded modulus and exponent in zkVM, the public key is hardcoded in the policy as a static field in the program’s read-only memory. This removes expensive operations and big-integer initializations. As we will show in the experiments, although this optimization improves the prover time of RSA verification by one to two orders of magnitude, its overhead is still quite high in practice and is the bottleneck of the prover. In the literature, there are optimized circuits/R1CS constraints [3, 31] and special protocols [50] for RSA verification. It merely takes around 2 seconds to generate a proof using Groth16 [27], and the prover time would be another order of magnitude faster using the SNARK backend of RISC Zero. In principle, we could utilize them through a pre-compiled instruction, or through a proof composition using recursive SNARKs to combine the proof for RSA verification with the zkVM proof. Unfortunately, we were not able to integrate them to RISC Zero. We believe this is only a gap of the implementation, but not any fundamental issue of our scheme.

5

Experiments

We have fully implemented P REZTA, and we report the empirical evaluations in this section. Settings. We tested the prover and the verifier on an AWS c7i.4xlarge instance with 16 vCPUs of Intel Xeon Scalable and 32 GB of memory. The prover and the verifier are both implemented in Rust and compiled with cargo using the -release flag to enable optimizations. We use the RISC

Zero zkVM v3.0.3 [6] to instantiate our SNARK. It has a transparent setup, and the security relies on collision-resistant hash functions and the Fiat-Shamir transformation.

5.1

End-to-end Performance

Dataset, compilation and verification key generation. As presented in Section 4.1.5, we test P REZTA on the XACML 3.0 conformance test suite [8], and our compiler supports 323 out of 389 testable policies. On average, it takes around 0.24 seconds to compile a policy from XACML to Rust, while it takes 1.73s to compile the policy from Rust to RISC-V and also generate the verification key of the policy in zkVM. This part is done only once for each policy by the PA, and thus the overhead is very small in practice. Prover time. The prover time of every policy P REZTA supports is presented in Figure 4. As shown in the figure, the prover time is either around 14 seconds or around 28 seconds. This is due to the padding of RISC Zero zkVM. To provide a better understanding, we also plot the number of total cycles before padding for each policy reported by RISC Zero, and the figure is sorted by total cycles. The total cycles consist of user cycles (the number of cycles executed by the main Rust code), and additional instructions inserted by RISC Zero that are required for the zkVM. The total number of cycles is then padded to the nearest power of 2. Therefore, for those policies with fewer than 130K total cycles before padding, they are padded to 217 = 131, 072 cycles, while others are padded to 218 = 262, 144 cycles. The same number of cycles after padding does not result in exactly the same prover time because of different instructions used in different policies, but they are highly correlated. We also tested an empty Rust code in RISC Zero, and it results in 215 = 32, 768 cycles after padding with the prover time of 3.8 seconds. There are around 20K paging cycles and 9K reserved cycles in the padding for initializing the memory and setting up the zkVM. To demonstrate the potential of P REZTA, we remove the RSA verification module from the zkVM and report the prover time in Figure 5. This is because as explained in Section 4.2.3, we envision that optimized circuits or special protocols for RSA verification should be integrated in the future, eliminating the overhead of this module in zkVM. As shown in the figure, the prover time for 88.6% of the policies drops to only 7 seconds. It shows that the main bottleneck of the end-to-end prover time in P REZTA comes from the RSA verification and the padding of RISC Zero. In fact, the number of user cycles for the majority of policies is less than 20K, which is even smaller than the additional padded cycles of RISC Zero for initialiation. With the recent improvement of zkVMs [5] with hardware accelerations, our scheme can be made practical in the near future. We further investigated the cases with more than 100K user cycles in Appendix E. Proof size and verifier time. The proof size of all policies

·105 3

30

20

User Cycles Page Cycles Padding Cycles Prover time

2.5 2

15

1.5

10

1

5

0.5

0

Cycles

Prover time (s)

25

0

Policy # (sorted by total cycles before padding)

Figure 4: Prover time and cycles of all policies. ·105 3

30

20

User Cycles Page Cycles Padding Cycles Prover time

2.5 2

15

1.5

10

1

5

0.5

0

Cycles

Prover time (s)

25

0

Policy # (sorted by total cycles before padding)

Figure 5: Prover time and cycles of all policies. (without RSA verification) are between 238KB to 250KB, and the verifier time are between 14 and 15.5 milliseconds. The verifier time is very practical for edge devices in practice. The proof size can be further compressed to 256 bytes via recursive SNARKs (e.g., Groth16 [27]), with an additional overhead on the prover time.

5.2

Ablation Study and Micro-benchmarks

To better understand the improvement of P REZTA over naive approaches, we present an ablation study and microbenchmarks in this section. We take the policy with the largest number of user cycles, implement it in RISC Zero naively without any optimizations, and then add each of our optimizations one by one cumulatively. Table 2 shows the ablation study. It would take 1,301.7

seconds to generate a proof in the naive approach without any optimizations, while it only takes 27.3 seconds in P REZTA, which is 47.7× faster. The largest improvement comes from the RSA verification, which can be further improved by a dedicated circuit/R1CS outside zkVM, or by special protocols such as [50]. Moreover, the regex optimization targets a major source of user cycles, significantly reducing user cycles and lowering prover time from 176s to 27.3s. In Table 3, we also provide a breakdown of P REZTA for the same policy in terms of user cycles. As shown in the table, the RSA verification contributes to 45% of the user cycles and our optimized Regex contributes to 47%3 . 3 The sum of cycles does not equal to the last row of Table 2 because RISC Zero also inserts different number of user cycles when we implement each module individually.

Table 2: Ablation study of Prezta optimizations. Each row denotes adding the optimization in Column 1 cumulatively. Optimization None RSA Regex

User cycles

Prover time (s)

Verifier time (ms)

Proof size (KB)

10,521,257 805,388 153,677

1301.7 176 27.3

196.9 32.8 15.1

3236 536 250

Table 3: Breakdown of user cycles by major functions.

User cycles

Others

Regex

RSA

13,508

71,429

68,598

Comparison to Reef [7]. In Appendix E.1, we further compare the performance of our regex-focused optimizations with Reef [7], a SNARK system tailored for regular expressions.

6

Discussion

We now address the practical considerations that arise when deploying P REZTA, including update mechanics, proof generation models, and auditability.

6.1

Updates

One important feature of the architecture is the ease of updates. To update a policy, the policy authority needs to compile it from XACML to Rust and then use RISC Zero to obtain a new IMAGE_ID. This ID is then signed and distributed to edge devices (perhaps piggybacked on the requests). To ensure the most recent policy is used, the signed IMAGE_IDs should be accompanied by an expiration time; more speedy revocation could be supported by using a protocol similar to OCSP [48] to certify that a policy is still in effect. Specifically, a revocation service tracks whether a policy has been revoked and, when queried by a client, signs a status message indicating that status. The client includes this status message as another input to the policy evaluation program, much like the JWT from the IdP. The program then checks the signature, revocation status, and freshness against the current timestamp (Table 1). The edge device remains agnostic to revocation checks. As with OCSP, the policy authority may operate the revocation service directly or delegate it to another server trusted only to track status. Because these checks are embedded in the PA-signed policy, P REZTA can vary parameters such as freshness requirements, potentially conditioned on other attributes such as request sensitivity. We note that some of the logic of verifying update signatures, expirations, and revocation status, could itself be encoded into a separate (long-lived) zkSNARK or zkVM program to allow updates without any specific code on the edge

device. Due to the flexibility of the zkVM, more significant changes are possible, all without device upgrades. For example, to support a new policy language, such as Rego [39] or NGAC [24], it would be necessary to build a new compiler that translates such policies into Rust, but from the point of view of the edge device, the new programs would be equivalent to a policy update. One could also switch identity management systems, e.g., from JWT to SAML [38], or from RSA signatures on tokens used in our prototype to ECDSA or others. Again, since the edge device does not interact with authentication tokens, it would remain agnostic to this change. (Unless new precompiles were necessary to efficiently verify the signature, in which case the verifier would need to be updated.) In fact, it would be possible to create a post-quantum secure version of P REZTA. The proof algorithm used by RISC Zero [14] (see [19] for details) is hash-based and thus not vulnerable to quantum attacks. To render the entire system post-quantum secure, it would be necessary to use a postquantum signature algorithm for the signing of policy IMAGE_IDs and the credentials (JWTs) in the identity system. The latter signature must be verified inside the zkVM, so a version of SPHINCS+ [15] instantiated with Poseidon [26] would be a good candidate. Verifier upgrades would be needed for any updates to the zkVM verifier, and these would become critical if these addressed a soundness error in the proof system. The field of zkVMs is rapidly maturing and we expect that a robust, production-ready zkVM will be available in the near future.

6.2

Proof Outsourcing and Composition

The resources needed to create a proof may be prohibitive for low-power devices, such as phones or monitoring terminals. In such cases, proof generation can be outsourced to either a local server or a cloud service; this is a strategy adopted by, e.g., zkLogin [10]. Importantly, this service would not be a trusted component—its compromise would at worst obtain a log of attempted accesses, but would not enable unauthorized access, due to the soundness of zkSNARKs.4 Full access privacy could be achieved by using a committee of servers using recent collaborative zkSNARKs [25, 40]. A powerful cloud proving server with GPUs could also significantly reduce the proving latency. RISC Zero supports proof composition, where one zkVM program can verify another’s execution. This could be used to support modular policy programs, with parts of the policy delegated to other programs (or even other administrators), and would create potential reuse of proof components to optimize 4 One has to be somewhat careful with supplying JWTs to an outsourced prover, as they serve as bearer certificates and could therefore be abused by an outsourced prover. Again, following a strategy from zkLogin, we can bind the JWT by having it including a hash of the request in the nonce, which could then be verified by the zkSNARK.

performance. We leave a full exploration of proof composition in this context to future work.

6.3

Auditing

To support audits, policies could require subjects to register a log record at a logging server and supply a proof of inclusion with the access request, which would be verified by the policy program. The log server could be made transparent and append-only by using techniques from certiicate transparency [33]; the log entries could also be encrypted using techniques similar to Larch [23].

Open Science The artifact is permanently archived at https://doi. org/10.5281/zenodo.20303462 (CC BY 4.0). It includes: (1) the Prezta prototype (RISC Zero zkVM v3.0.3) and (2) the XACML-to-Rust policy compiler. Source repositories: https://github.com/walotta/ZK_ Zero_Trust and https://github.com/osaidameer/ xacml-to-rust. The implementation is unaudited research code.

References https://aptos.dev/build/ [1] Aptos keyless. guides/aptos-keyless. Accessed: 2025-11-10.

Acknowledgments This material is based upon work supported by the National Science Foundation (NSF) under Grant No. 2113819 and No. 2401481. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of these institutes.

Ethical Considerations Prezta is a proposed architecture for OT security, and this paper is a first step toward possible future production systems based on that architecture. Any eventual deployment could affect OT operators, administrators, other parties interacting with edge devices, and indirectly the public who rely on critical infrastructure. We believe Prezta has the potential to improve security and reduce management burden in OT environments. However, deployment of new technology in such environments also introduces risks, including implementation flaws, misconfiguration, new attack surfaces, and possible availability impacts. These tradeoffs are highly deployment-specific, so a full cost-benefit-risk analysis is beyond the scope of this paper. We judge the risks from publication of this work and code to be minimal. The work proposes a defensive architecture and our implementation is a research prototype rather than a production-ready system. For clarity, we will explicitly label the implementation as unaudited research code. Like many defensive security technologies, a system that strengthens OT authorization could also make some forms of access or exploitation more difficult for a range of actors, including sophisticated state-backed actors. We nevertheless view improved security and resilience for OT and critical infrastructure as a net benefit, given the broad set of stakeholders who depend on these systems.

[2] Bonsai pay. https://risczero.com/blog/ bonsai-pay. Accessed: 2025-11-10. [3] Circom RSA verification. https://github.com/ zkp-application/circom-rsa-verify. Accessed: 2025-11-07. [4] Cryptography precompiles. https://dev.risczero. com/api/zkvm/precompiles. Accessed: 2025-1112. [5] Ethereum real-time proving. https://ethproofs. org/. Accessed: 2025-11-12. [6] RISC Zero – risc zero zkvm: Scalable, transparent arguments of risc-v integrity. https://github.com/ risc0/risc0. Accessed: 2025-11-12. [7] S. Angel, E. Ioannidis, E. Margolin, S. Setty, and J. Woods. Reef: Fast succinct Non-Interactive ZeroKnowledge regex proofs. In 33rd USENIX Security Symposium (USENIX Security 24), pages 3801–3818, 2024. [8] AuthzForce Core. PDP test utilities. https: //github.com/authzforce/core/tree/ develop/pdp-testutils/src/test/resources/ conformance/xacml-3.0-from-2.0-ct. Accessed: 2025-11-12. [9] F. Bakir, C. Krintz, and R. Wolski. Caplets: Resource aware, capability-based access control for iot. In 2021 IEEE/ACM Symposium on Edge Computing (SEC), pages 106–120. IEEE, 2021. [10] F. Baldimtsi, K. K. Chalkias, Y. Ji, J. Lindstrøm, D. Maram, B. Riva, A. Roy, M. Sedaghat, and J. Wang. zklogin: Privacy-preserving blockchain authentication with existing credentials. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, pages 3182–3196, 2024.

[11] E. Ben-Sasson, I. Bentov, Y. Horesh, and M. Riabzev. Scalable, transparent, and post-quantum secure computational integrity. In Advances in Cryptology – CRYPTO, 2019. [12] E. Ben-Sasson, A. Chiesa, D. Genkin, E. Tromer, and M. Virza. SNARKs for C: Verifying program executions succinctly and in zero knowledge. In CRYPTO 2013. [13] E. Ben-Sasson, A. Chiesa, E. Tromer, and M. Virza. Scalable zero knowledge via cycles of elliptic curves. In CRYPTO 2014, pages 276–294. 2014. [14] E. Ben-Sasson, L. Goldberg, S. Kopparty, and S. Saraf. DEEP-FRI: Sampling Outside the Box Improves Soundness. In T. Vidick, editor, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020), Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1–5:32, Dagstuhl, Germany, 2020. Schloss Dagstuhl Leibniz-Zentrum für Informatik. [15] D. J. Bernstein, A. Hülsing, S. Kölbl, R. Niederhagen, J. Rijneveld, and P. Schwabe. The sphincs+ signature framework. ACM Transactions on Information and System Security, 2019. [16] N. Borisov and E. Brewer. Active certificates: A framework for delegation. In Network and Distributed Systems Security Symposium, 2002. [17] S. A. Brands. Rethinking public key infrastructures and digital certificates: building in privacy. MIT Press, 2000. [18] D. Brossard, A. Clymer, and T. Dimitrakos. ALFA 2.0 the Abbreviated Language for Authorization. InternetDraft draft-brossard-alfa-authz-00, Internet Engineering Task Force, July 2024. Work in Progress. [19] J. Bruestle, P. Gafni, and the RISC Zero Team. Risc zero zkvm: Scalable, transparent arguments of risc-v integrity. Technical report, RISC Zero, August 11 2023. Draft technical report. [20] J. Camenisch and A. Lysyanskaya. An efficient system for non-transferable anonymous credentials with optional anonymity revocation. In International conference on the theory and applications of cryptographic techniques, pages 93–118. Springer, 2001.

[23] E. Dauterman, D. Lin, H. Corrigan-Gibbs, and D. Mazières. Accountable authentication with privacy protection: The larch system for universal login. In 17th USENIX Symposium on Operating Systems Design and Implementation (OSDI 23), pages 81–98, Boston, MA, July 2023. USENIX Association. [24] D. Ferraiolo, L. Feldman, and G. Witte. Exploring the next generation of access control methodologies, Nov. 2016. [25] S. Garg, A. Goel, A. Jain, G.-V. Policharla, and S. Sekar. zkSaaS:Zero-Knowledge SNARKs as a service. In 32nd USENIX Security Symposium (USENIX Security 23), pages 4427–4444, 2023. [26] L. Grassi, D. Khovratovich, C. Rechberger, A. Roy, and M. Schofnegger. Poseidon: A new hash function for Zero-Knowledge proof systems. In 30th USENIX Security Symposium (USENIX Security 21), pages 519–535, 2021. [27] J. Groth. On the size of pairing-based non-interactive arguments. In Advances in Cryptology – EUROCRYPT 2016, pages 305–326, 2016. [28] V. Hu, D. Ferraiolo, R. Kuhn, A. Schnitzer, K. Sandlin, R. Miller, and K. Scarfone. Guide to attribute based access control (abac) definition and considerations. Technical Report NIST Special Publication 800-162, National Institute of Standards and Technology (NIST), 2014. [29] M. B. Jones, J. Bradley, and N. Sakimura. JSON web token (JWT). Technical Report 7519, IETF, 2015. [30] A. Kim and K. Lawson-Jenkins. Zero trust architectures for operational technology at nuclear facilities. Technical Report TLR-RES-DE-2024-001, U.S. Nuclear Regulatory Commission, Washington, DC, November 2023. Prepared under the Future Focused Research Initiative. [31] A. Kosba, C. Papamanthou, and E. Shi. xjsnark: A framework for efficient verifiable computation. In 2018 IEEE Symposium on Security and Privacy (SP), pages 944–961. IEEE, 2018. [32] R. Langner. Stuxnet: Dissecting a cyberwarfare weapon. IEEE Security and Privacy, 9(3):49–51, 2011.

[21] L. Cao, L. Meng, D. Stefan, and E. Fernandes. Stateful least privilege authorization for the cloud. In 33rd USENIX Security Symposium (USENIX Security 24), pages 3477–3494, 2024.

[33] B. Laurie, A. Langley, and E. Kasper. Certificate transparency. RFC RFC 6962, Google Inc. and Internet Engineering Task Force (IETF), Dec. 2013.

[22] C. Cesarano and R. Natella. Securing an application layer gateway: An industrial case study. In 2024 19th European Dependable Computing Conference (EDCC), pages 75–80, 2024.

[34] R. M. Lee, M. J. Assante, and T. Conway. Analysis of the cyber attack on the ukrainian power grid. Technical report, E-ISAC and SANS Industrial Control Systems, March 2016. Technical report.

[35] P. Moser, M. Esposito, F. Bruschi, and D. Sciuto. Privacy-preserving eidas compliance in blockchain wallets via zkvm. In 2025 IEEE International Conference on Pervasive Computing and Communications Workshops and other Affiliated Events (PerCom Workshops), pages 31–37. IEEE Computer Society, 2025.

[45] S. W. Rose, O. Borchert, S. Mitchell, and S. Connelly. Zero trust architecture. NIST Special Publication 800-207 800-207, National Institute of Standards and Technology (NIST), August 2020. https://csrc.nist.gov/publications/detail/sp/800207/final.

[36] North American Electric Reliability Corporation. Zero trust security for electric operations technology. White paper, NERC, June 2023. Accessed November 2025.

[46] M. Rosenberg, J. White, C. Garman, and I. Miers. zkcreds: Flexible anonymous credentials from zksnarks and existing identity infrastructure. In 2023 IEEE Symposium on Security and Privacy (SP), pages 790–808. IEEE, 2023.

[37] OASIS. extensible access control markup language (xacml) version 3.0 core specification. Standard OASIS Standard, OASIS, 2013. [38] OASIS Security Services Technical Committee. Security assertion markup language (saml) v2.0 technical overview. Technical report, OASIS, 2005. Available at: http://docs.oasis-open.org/security/saml/v2.0/samlcore-2.0-os.pdf. [39] Open Policy Agent Authors. Rego - policy language for open policy agent. https: //www.openpolicyagent.org/docs/latest/ policy-language/, 2025. Accessed: 2025-11-13. [40] A. Ozdemir and D. Boneh. Experimenting with collaborative zk-SNARKs:Zero-Knowledge proofs for distributed secrets. In 31st USENIX Security Symposium (USENIX Security 22), pages 4291–4308, 2022. [41] S. Park, J. Lee, S. Lee, J. H. Chun, H. Cho, M. Kim, H. K. Cho, and S.-M. Moon. Beyond the blockchain address: Zero-knowledge address abstraction. In Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing, pages 366–374, 2025. [42] E. Peterson. Achieving visibility and control in ot systems: Remote maintenance, securing remote access, and the zero-trust approach. Technical report, Cybercore Integration Center, Idaho National Laboratory, May 2023. Published by CISA.

[47] R. S. Sandhu, E. J. Coyne, H. L. Feinstein, and C. E. Youman. Role-based access control models. IEEE Computer, 29(2):38–47, 1996. [48] S. Santesson, M. Myers, R. Ankney, A. Malpani, S. Galperin, and D. C. Adams. X.509 Internet Public Key Infrastructure Online Certificate Status Protocol - OCSP. RFC 6960, June 2013. [49] K. Stouffer, M. P. J. Falco, and K. Scarfone. Guide to operational technology (ot) security. NIST Special Publication 800-82 Revision 3, National Institute of Standards and Technology, September 2023. [50] A. P. Woo, A. Ozdemir, C. Sharp, T. Pornin, and P. Grubbs. Efficient proofs of possession for legacy signatures. In 2025 IEEE Symposium on Security and Privacy (SP), pages 3291–3308. IEEE, 2025.

A

Additional Preliminaries

A.1

SNARK

Definition 2 (Succinct non-interactive argument of knowledge (SNARK)). Let R be a relation with public instance x and private witnesses w, a SNARK for R consists of PPT algorithms (G , P , V ) with the following properties: • Completeness. For any instance (x, w) ∈ R 

[43] President’s National Security Telecommunications Advisory Committee (NSTAC). Draft NSTAC IT-OT convergence report. Technical report, Cybersecurity and Infrastructure Security Agency (CISA), August 2022. Working Draft. [44] P. H. N. Rajput, C. Doumanidis, and M. Maniatakos. ICSPatch: Automated vulnerability localization and NonIntrusive hotpatching in industrial control systems using data dependence graphs. In 32nd USENIX Security Symposium (USENIX Security 23), pages 6861–6876, Anaheim, CA, Aug. 2023. USENIX Association.

Pr

V (x, vk, π) = 1

(pk, vk) ← G (1λ ), π ← P (x, w, pk),

 =1

• Knowledge Soundness: for any PPT adversary A , there exists an expected PPT knowledge extractor EA such that the following probability is ≤ negl(λ):  Pr

V (x, vk, π∗ ) = 1 ∧(x, w) ∈ /R

(pk, vk) ← G (1λ ), ∗ (π ; w) ← (A ||EA )(x, pk)

 .

• Succinctness. The proof size |π| is sublinear in the size of the relation R and the witness |w|.

In addition to these properties, a zero-knowledge SNARK further satisfies zero-knowledge, which informally says that the proof leaks no information about the witness beyond the fact that the instance is in R . We only use the soundness and the succinctness of a SNARK in this paper and omit the formal definition of zero-knowledge.

B

Table 4: Unsupported XACML Elements, Functions and Features Name x500-* base64Binary-* hexBinary-* rfc822Name-* dnsName-* ipAddress-* *-add-yearMonthDuration *-subtract-yearMonthDuration *-add-dayTimeDuration *-subtract-dayTimeDuration double-*{set functions} any-of all-of any-of-any any-of-all all-of-any all-of-all map AttributeSelector PolicyIdReference PolicysetIdReference Obligations Advice

Proof Sketch of Theorem 1

The completeness is implied by the correctness of the digital signature scheme and the completeness of the SNARK on the relation R checking P(att, Req, info) = 1 and signature.Verify(att, σatt , pkIdP ) = 1. For security, when Prezta.Verify(π, Req, info, vkP , σP , pkPA ) = 1, by the knowledge soundness of SNARK (Definition 2), there exists an extractor that can extract w = (att, σatt ) such that P(att, Req, info) ̸= 1 or signature.Verify(att, σatt , pkIdP ) ̸= 1 only with negligible probability. Then by the unforgeability of the digital signature, when signature.Verify(att, σatt , pkIdP ) = 1, the probability that att ∈ / Qatt is negligible. Moreover, by Step 2 of Prezta.Verify, signature.Verify(vkP , σP , pkPA ) = 1, the probability that vkP ∈ / QP is negligible. The by the union bound, the probability that Prezta.Verify(π, Req, info, vkP , σP , pkPA ) = 1 and P(att, Req, info) ̸= 1, or Verify(att, σatt , pkIdP ) = 1 and att ∈ / Qatt , or Verify(vkP , σP , pkPA ) = 1 and vkP ∈ / QP is negligible, completing the proof of security.

C

Unsupported XACML Functions

D

Full Policy vs Generated Code

E

Additional Experimental Results

number of user cycles and thus characterizing these cases as representative high-load scenarios in the policy evaluation workload.

E.1

Policies with large number of user cycles. We further investigated the cases with more than 100K user cycles in Figure 4. The large number of user cycles are primarily due to their intensive computational patterns during the policy evaluation. Specifically, cases IIC150–IIC156 and IIC340–IIC349 repeatedly invoke IsoDuration::parse or DateTime parsing functions for each attribute or bag element, resulting in frequent ISO-8601 duration and timestamp conversions. Cases IIC201–IIC205 additionally construct and manipulate HashSet objects to perform intersection, union, subset, and equality operations, which significantly increase the number of cycles. The most computationally demanding cases, IIC056 and IIC057, involve loading and executing dual DFA-based regular expressions in conjunction with JWT field validation, producing extensive state transitions and branching. Overall, these patterns combine repeated parsing, string processing, and complex set operations, leading to a substantially higher

Type Functions Functions Functions Functions Functions Functions Functions Functions Functions Functions Functions Function Function Function Function Function Function Function Element Element Element Feature Feature

Comparison with Reef

To quantify the improvement of our regex-focused optimizations, we evaluate the six representative regular expressions in the policies from the dataset and compare them with Reef [7], a SNARK system tailored for regular expressions. Table 5 (top) reports the prover time for each regular expression. As shown in the table, even for short strings and simple regular expressions, the naive Regex library in zkVM leads to a significant overhead on the prover time. Our optimization improves the efficiency by one to two orders of magnitude. Compared to Reef, our protocol is even slightly faster for some of the cases, while slightly slower for others. Due to the limited number of examples from the XACML policy datasets, we also create synthetic regex expressions that may occur in authorization policies, such as checks on email, IP address and JWT. See the full expressions in Table 6. The performance is reported in Table 5 (bottom) as well, and we observe similar comparisons with the naive approach and Reef. The full regular expressions and inputs corresponding to the names used in Table 5 are shown in Table 6.

Listing 8 Rust code generated from policy in Listing 7

Listing 7 Simplified Sample XACML Policy <Policy PolicyId="policy" ,→ RuleCombiningAlgId="deny-overrides"> <Target/> <Rule Effect="Permit" RuleId="rule"> <Target> <AnyOf> <AllOf> <Match MatchId="string-equal"> <AttributeValue DataType="#string">Julius ,→ Hibbert</AttributeValue> <AttributeDesignator ,→ AttributeId="subject-id" ,→ Category="access-subject" ,→ DataType="#string"/> </Match> </AllOf> </AnyOf> <AnyOf> <AllOf> <Match MatchId="anyURI-equal"> <AttributeValue DataType="#anyURI">http://m ⌋ ,→ edico.com/record/patient/BartSimpson</A ⌋ ,→ ttributeValue> <AttributeDesignator ,→ AttributeId="resource-id" ,→ Category="resource" DataType="#anyURI"/> </Match> </AllOf> </AnyOf> <AnyOf> <AllOf> <Match MatchId="string-equal"> <AttributeValue ,→ DataType="#string">read</AttributeValue> <AttributeDesignator AttributeId="action-id" ,→ Category="action" DataType="#string"/> </Match> </AllOf> <AllOf> <Match MatchId="string-equal"> <AttributeValue DataType="#string">write</A ⌋ ,→ ttributeValue> <AttributeDesignator AttributeId="action-id" ,→ Category="action" DataType="#string"/> </Match> </AllOf> </AnyOf> </Target> </Rule> </Policy>

// imports // jwt verification functions #[derive(Debug, PartialEq)] enum Result { Permit, Deny, NotApplicable, } fn evaluate_target_rule(inp: &Inputs) -> bool { (("Julius Hibbert" == ,→ inp.access_subject_subject_id) && ("http:/ ⌋ ,→ /medico.com/record/patient/BartSimpson" == ,→ inp.resource_resource_id) && (("read" == ,→ inp.action_action_id) || ("write" == ,→ inp.action_action_id))) } fn evaluate_rule(inp: &Inputs) -> Result { if !evaluate_target_rule(inp) { return Result::NotApplicable; } return Result::Permit; } fn evaluate_target_policy(inp: &Inputs) -> bool { true // empty target, match all } fn evaluate_policy(inp: &Inputs) -> Result { if !evaluate_target_policy(inp) { return Result::NotApplicable; } let results = vec![evaluate_rule(inp)]; //deny-overrides let mut atleast_one_permit = false; for res in &results { if *res == Result::Deny { return Result::Deny; } else if *res == Result::Permit { atleast_one_permit = true; } } if atleast_one_permit { return Result::Permit; } return Result::NotApplicable; } fn main() { let inp: Inputs = env::read(); let mut decision = match evaluate_policy(&inp) ,→ { Result::Permit => true, _ => false, }; let jwt: String = env::read(); let jwt_positions: Vec<usize> = env::read(); if !extract_jwt(&jwt, &jwt_positions, &inp) { decision = false; } env::commit(&decision); env::commit(&inp); }

Table 5: Per-policy prover time (in seconds) for regex workloads. Short names are used in the table; the full regex patterns and inputs are listed in Table 6. Short

RISC0 (Regex lib)

Prezta

Reef

RW_READ RW_DELETE J_HIBBERT B_SIMPSON J_K_HIBBERT B_O_SIMPSON

61.5 61.6 314.4 509.0 127.3 128.2

7.2 7.3 14.8 14.9 14.7 14.8

9.0 10.8 9.4 11.3 11.6 11.6

EMAIL_SIMPLE EMAIL_COMPLEX IPV4 IPV6 JWT_LIKE OAUTH_PATH ISO8601

315.0 127.3 126.8 61.3 129.7 54.1 111.8

7.4 7.5 14.9 7.5 7.4 7.4 7.4

11.3 12.3 13.4 13.5 11.4 11.1 12.4

RW_READ RW_DELETE J_HIBBERT B_SIMPSON J_K_HIBBERT B_O_SIMPSON EMAIL_SIMPLE EMAIL_COMPLEX IPV4 IPV6 JWT_LIKE OAUTH_PATH ISO8601

pattern: read | write; input: read pattern: read | write; input: delete pattern: J .* Hibbert; input: Julius Hibbert pattern: B.* Simpson; input: Julius Hibbert pattern: J .* K.* Hibbert; input: Julius Hibbert pattern: B.* O.* Simpson; input: Julius Hibbert pattern: ^[a−zA−Z0−9._%+−]+@[a−zA−Z0−9.−]+ .[ a−zA−Z]{2,}$; input: [email protected] pattern: ^[a−zA−Z0−9._%+−]+@[a−zA−Z0−9.−]+ \\.[ a−zA−Z]{2,}$; input: very . unusual [email protected]−[email protected] pattern: ^((25[0−5]|2[0−4][0−9]|[01]?[0−9][0−9]?).){3} (25[0−5]|2[0−4][0−9]|[01]?[0−9][0−9]?) $; input: 192.168.1.1 pattern: ^(?:[0−9a−fA−F]{1,4}:){7}[0−9a−fA−F]{1,4}$ |^::1 $ |^:: $; input: 2001::1 pattern: ^ey[A−Za−z0−9+/=]+\.[ey][A−Za−z0−9+/=]+ \.[ A−Za−z0−9+/=]*$; input: not . a . jwt . token pattern: ^/oauth /( authorize | token | revoke)$; input: /oauth/ authorize pattern: ^([0−9]{4})−([0−9]{2})−([0−9]{2})T ([0−9]{2}):([0−9]{2}) :([0−9]{2})(.[0−9]+)?( Z |([+−][0−9]{2}):([0−9]{2}))\ $; input: 2025−04−05T10:15:30.123+05:30

Table 6: Full regex patterns and inputs.