arXiv CSopen access

SafeNom: Data-Aware Microservice Policies

SafeNom: Data-Aware Microservice Policies

arXiv:2609.30394v1 [cs.PL] 24 Sep 2026

KARUNA GREWAL, Cornell University, USA P. BRIGHTEN GODFREY, University of Illinois Urbana-Champaign, USA JUSTIN HSU, Cornell University, USA Many cloud-based applications are organized as loosely coupled microservices, where invoking a service’s API triggers a cascade of APIs across many services and leads to inter-service exchange of API parameters and output responses. Current tools for monitoring microservice safety properties have limited expressiveness for properties that describe the flow of data through API calls. To this end, we present SafeNom, a specification and monitoring framework for microservices based on nominal languages. SafeNom policies can express both the desired order of API calls and how the data carried in requests and responses should or should not flow between the APIs. Policies are enforced using a nominal automaton-based distributed runtime monitor which can be applied in a blackbox and non-invasive manner, without access to the service implementation and without making changes to the service implementation. Our experiments show that our monitor can efficiently enforce rich data-aware properties while incurring minimal latency overhead, on the order of a few milliseconds.

1 Introduction A popular paradigm for implementing a modern-day cloud application is to decompose it into loosely coupled self-contained microservices that expose their functionality through APIs, which can be accessed using protocols like HTTP or gRPC. In such an application, a single user request can trigger a cascade of downstream API calls and responses, resulting in a tree-shaped execution. Each call or response may carry data as parameters or results. For instance, these data include region identifiers, access tokens, confidential data, encryption keys, or trace IDs. Correct handling of this data is crucial to application correctness, and verifying that it is handled properly can provide assurance to various teams: compliance, development, and deployment. Since data moves between services, handling it correctly is an application-wide concern rather than the responsibility of any single service. A service may correctly process its local input and invoke the correct sequence of APIs, yet the overall execution can still be unsafe if a later service receives or uses the wrong value. For instance, a database write may occur after an encryption API to ensure compliant storage of personally identifiable information, but the execution may be unsafe if the value written to the database is the original raw data rather than the encrypted result. Thus, many policies must specify not only which services should be called and in what order, but also how the values carried by those calls relate to one another. Violations of such policies can cause data leaks, broken auditability, regulatory penalties, and loss of client trust, even when each individual service appears to satisfy its local API contract. Enforcement of such data-aware policies is complicated by the distributed design and deployment of microservice applications. The services in a microservice application are often not controlled by a single team. They may be developed by independent teams that do not have access to each other’s implementations, deployed by another team, and audited by a separate security or compliance team. Consequently, the team tasked with certifying an application may not have access to all service implementations and even when it does, requiring global changes to all services may be impractical. Thus, an enforcement mechanism should treat the application as a blackbox. Interservice communication provides a natural boundary for teams to specify and enforce fine-grained aspects of the application behavior without peeking into service code. Authors’ Contact Information: Karuna Grewal, [email protected], Cornell University, USA; P. Brighten Godfrey, University of Illinois Urbana-Champaign, USA, [email protected]; Justin Hsu, Cornell University, USA, [email protected].

2

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

Existing work and limitations. Existing deployment infrastructure and runtime monitors for microservices can enforce constraints on which APIs may communicate and in what order, but they remain unable to enforce properties that relate data values across an execution. For example, Kubernetes, a container network orchestration tool, allows a user to coarsely restrict or allow all access to services. Meanwhile, service mesh [Istio 2024b], a recent networking layer, offers finer-grained enforcement of inter-service communication policies, but its policies are single hop, meaning they can only specify whether a pair of endpoints is allowed to communicate through API calls. Recent runtime monitoring frameworks [Grewal et al. 2025, 2023] for microservice applications move beyond single-hop checks by enforcing multi-hop policies over the execution’s tree structure. The work by Grewal et al. [2023] introduces regular expression-style policies over the order of API calls, while SafeTree [Grewal et al. 2025] adds declarative constructs for specifying valid parentchild structure in the API call tree. Both systems are implemented as distributed monitors at the service mesh networking layer, using finite-state and visibly pushdown automata, respectively. This mirrors the distributed deployment structure of a microservice application. Each service’s incoming/outgoing traffic is locally monitored without a centralized monitor. The monitors are also blackbox and non-invasive, meaning they require no access to, or modifications of, the service implementation. However, neither framework can enforce properties that depend on the values carried by API calls or responses. This limitation rules out many natural microservice properties, like: (1) A compliance team may want the raw data to be encrypted before the encrypted result (different from the raw data) is stored in a database. (2) A development team may want that in a multi-party co-signature protocol, within a session the APIs called by each party use the same key, while different sessions may use distinct keys. (3) A deployment team may want all requests in an execution trace to carry the same trace ID parameter. These examples share a common form: they require reasoning about equality and inequality patterns among data carried by API calls/responses, not just the order of API calls. We call such properties data-aware, and in this work we consider how to specify and monitor these properties. We target a setting where teams that specify properties do not have access to the service implementation, and must treat the application as a blackbox. Thus, we consider the following question: “How can we specify and enforce data-aware microservice policies in a blackbox and noninvasive manner, i.e., without access to the service implementation and without invasive changes to the service code?” Addressing this question requires solving the following three challenges. Challenge 1: Policies should depend on (in)equality patterns and not concrete values. A common theme across our data-aware policies is that they specify an equality or inequality relation on the values of certain parameters across several API calls, but the concrete value of the parameter in the trace is insignificant. For instance, the trace-ID policy (3) above should accept any execution in which all API calls share the same trace ID, whether that ID is 10 or 20. Similarly, the (1) encryption policy above should accept any execution based on whether certain data values are (in)equal. Thus, the policies should be invariant under consistent renaming of values: two executions that differ only by replacing concrete values while preserving the same equality and inequality patterns should either both satisfy the property or violate it. This rules out treating values as elements of a fixed finite alphabet because the policy should not enumerate all possible values that may appear at runtime. Therefore, a suitable specification language should treat traces that preserve the (in)equality patterns modulo the concrete parameter/result values.

3

Challenge 2: (In)equality constraints are scoped. (In)equality relationships in microservice executions are not always global. Some values must remain consistent across an entire execution, while others may be relevant only within a smaller session, or a protocol phase, or a child call. For instance, the (3) trace ID policy above imposes a constraint that the trace ID remain fixed across the entire execution. In contrast, the (2) co-signature policy establishes the key equality constraint per-child session. After a session returns, the next session’s keys can be different. The policy author should have the flexibility to define the beginning and end of the scope of a data-dependency obligation. Thus, scoping is a semantic requirement of the policy language. Challenge 3: Efficient enforcement over a large value domain. Parameter and return values in a microservice trace range over a large domain—a monitor cannot use one automaton state per possible value. Moreover, in our blackbox microservice setting, the monitor must simulate an automaton in a distributed manner and carry the relevant monitoring metadata in HTTP headers. To fit this monitoring metadata into the limited header space, the monitor should track only values that are currently in scope and needed for a later comparison, while dropping values when they go out of scope. Thus, the underlying automaton needs a disciplined strategy to decide when to start tracking a value, how long to retain it for later comparisons, and when to discard it once policy checking no longer requires it. Our approach To address these challenges, we propose SafeNom, a specification language and monitoring framework for data-aware microservice policies. Nominal words as the semantic foundation. We use nominal words and nominal languages to make invariance under value renaming an intrinsic property of the policy semantics. Intuitively, a nominal word is a sequence of ordinary symbols, like API call and return events, augmented with special symbols called names, which correspond to data values in our setting. Then, a nominal language is a set of nominal words such that freely replacing a name keeps the word in the language. This makes nominal languages a suitable interpretation for our data-aware properties, which should only depend on repetition patterns of (in)equal values rather than concrete values. Lazy binders for scoping. We develop the SafeNom policy language for expressing scoped data-dependencies over microservice traces. Our policies can declare when the tracking of a value begins and ends for a data-dependency constraint. Our starting point is the nominal regular expressions with binders (NREs) introduced by Kurz et al. [2012b], whose binders provide a declarative mechanism to introduce names for values and delimit the part of the trace over which they can be referenced. However, Kurz et al.’s NRE eager binders are too restrictive for modeling microservice traces because they require the value associated with a data-dependency constraint to appear exactly where the constraint’s scope begins. However, in microservice executions, the scope of a datadependency may begin before the relevant value appears in an API event. SafeNom addresses this mismatch with lazy binders. A lazy binder opens the scope of a name without immediately assigning it a value. The name is initialized at the point of its first observation. Once initialized, it can be used for future comparison. Thus, lazy binders let the policy specify the scope of a constraint while deferring the value’s binding to the point where it is observed in the trace. SafeNom further extends NREs with semantics for inequality checks because NREs are designed around equality checks on names, whereas many interesting properties in the microservice setting also require checking for inequality between certain data.

4

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

Nominal automaton-based monitoring. To enforce SafeNom policies, we compile them into a nominal automaton model inspired by Kurz et al. [2012b], extended to support SafeNom’s lazy binding and inequality semantics. Building on SafeTree’s automaton-based distributed monitoring setup, we implement the compiled nominal automaton as a runtime monitor that simulates the automaton’s transitions on the execution trace of HTTP messages in a microservice application. Since a nominal automaton is finite-state regardless of the size of the value domain, and it tracks only the names currently in scope, the monitoring metadata stays within the HTTP header budget. By implementing our monitor atop the service mesh [Istio 2024a] networking layer, it runs outside the service containers and does not require any visibility or invasive changes to the service implementation. Contributions. We make the following technical contributions: (1) an extension of nominal words and nominal regular expressions supporting lazy binding (section 3), (2) the syntax and semantics of our SafeNom language for specifying data-aware microservice policies (section 4), (3) case studies that demonstrate SafeNom’s expressiveness (section 5), (4) a method to soundly compile SafeNom policies to a novel notion of nominal automata (section 6), and (5) a service mesh-based implementation of a runtime monitor for SafeNom policies (section 7) and an evaluation of its performance (section 8). 2

A Tour of SafeNom Policies

This section motivates SafeNom through a multi-factor authentication application. The goal is to illustrate why data-aware policies require more than checking which APIs are called, or in which order they are called. Many safety properties for microservice applications are about the flow of values through API parameters and responses: a value received by one service should be forwarded unchanged to another service, a transformed value should be used instead of the raw value, or two values should be provably different. SafeNom provides a policy language and runtime monitor for such properties. 2.1

Example: login with multi-factor authentication

Consider an authentication service that implements login with multi-factor authentication (MFA). The application exposes a login API that takes in a password as its parameter. After checking the input password, the login service calls the mfa API to perform one round of multi-factor authentication. Each mfa call carries a challenge code as its input. This is the code that will be shown to the user through an authenticator application. The corresponding mfa response carries the code confirmed by the user. In high-risk login settings, the application may issue multiple MFA challenges for additional verification. For simplicity, we assume that the application uses two MFA challenges. Safety property. A security team may require the following data-flow property: (1) login execution should include two calls to mfa APIs. (2) Each MFA response must return the same challenge code that was passed to its corresponding MFA call. (3) The MFA challenge code must be distinct from the enclosing login password. This is because the password and the one-time challenge codes serve different roles in the login process. This property constrains both the order of API calls and returns and the values they carry.

5 ≠✓

call-login 1234

accepted

(i)

call-mfa

200

ret-mfa

200

call-mfa

100

=✓

ret-mfa

100

ret-login

✓

200

ret-login

✓

100

ret-login

✗

200

ret-login

✗

=✓ may coincide

≠✓

(ii)

call-login 1234

call-mfa

200

ret-mfa

200

call-mfa

200

=✓

ret-mfa =✓

≠✓

call-login 1234

rejected

(iii)

call-mfa

200

ret-mfa

150

call-mfa

100

=✗

ret-mfa =✓

≠✗

(iv)

call-login 1234

call-mfa 1234

ret-mfa 1234 =✓

call-mfa

200

ret-mfa =✓

Fig. 1. Example login traces. Each API event is marked in gray; values in boxes following API events are their respective parameters and responses. Blue boxes mark login passwords, yellow boxes mark the first mfa codes, green boxes mark the second mfa codes, and red boxes mark values that are the source of the property’s violation. Traces annotated with a green check satisfy the property, while crossed traces are invalid. Edges annotated with green checks ✓ and red crosses ✗ denote whether the corresponding equality or inequality constraint is satisfied.

(c) login scope

For example, the first HTTP trace (𝑖) in fig. 1 is valid. We write call-login and ret-login for call and return events of the login API, and call-mfa and ret-mfa for call and return events of mfa API. The trace begins with a call to login with password 1234. In this execution, login service initiates the first MFA challenge by calling mfa API with challenge code 200. This MFA challenge’s response carries the same value, meaning that the challenge was successful. Then login service initiates a second MFA challenge, but this time with a different code 100. Once again, this MFA challenge also succeeds with the response carrying 100. Thus, this trace satisfies the correct API event order and also the requirement that the two mfa codes should be different from the password of the enclosing login request, and that the call and return corresponding to a given mfa request should carry the same code. Our policy does not require the two MFA challenge codes to be different from each other. For example, the trace (𝑖𝑖) is also accepted. Meanwhile, trace (𝑖𝑖𝑖) is rejected because the input code 200 to the first call-mfa does not match its response 150. Similarly, trace (𝑖𝑣) is rejected because the first mfa challenge reuses the login password 1234. The SafeNom policy for the set of traces satisfying the above property is:  𝜈 n . call-login n       𝜈 𝑚 . call-mfa 𝑚 ret-mfa m } (a) independent MFA scopes   𝜈 𝑚 . call-mfa 𝑚 ret-mfa m } (b) 𝜈𝑚: fresh with respect to 𝜈𝑛    ret-login 

The correct sequence of HTTP requests/responses is marked in gray. The names n , m are used as logical identifiers for the API input and output parameters. The outer binder 𝜈 n introduces a (fresh identifier) name for the login password. Its scope extends over the entire login execution spanning from call-login to its corresponding ret-login. In a concrete trace, each binder is associated with the introduction of a fresh concrete value. Inside the login scope, each MFA challenge introduces its own local name m for its respective code for the duration of its own execution. The policy

6

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

has three crucial aspects: (a) the values of parameters marked by yellow m within the first mfa challenge should be equal, (b) the values of parameters marked by green m within the second mfa challenge should be equal, (c) (nested) 𝜈 n and 𝜈 m implicitly specify that the values of parameters at positions marked with n and m should be distinct, but values of parameters in disjoint mfa scopes need not be equal. Besides this, the policy should be agnostic to the actual value passed to all the parameters labeled by m (and similarly by n ). 2.2

Traces as words with binders

A concrete microservice execution trace records the API events and the values that appear in their parameters and responses. For example, in trace (ii), the parameters/responses of both mfa calls are 100. But these values are indistinguishable and we cannot observe that these correspond to different binders. However, the policy needs to distinguish them. By inspecting the trace, one should be able to decipher that the first two 100s belong to the first mfa; and the last two belong to the second mfa. Also, the trace does not record any information about the scopes in which the relevance of a value lasts for some (in)equality constraint. This is crucial for identifying that the first and second mfa codes are not required to be equal. To express these aspects, we add names n and binders « n . · » to raw microservice traces. A name identifies which occurrences of concrete values in the trace are meant to be equal. A binder « n . ·» marks where the name n is introduced and its associated concrete value’s lifetime. Repeated occurrences of the name within its lifetime should have the same concrete value. For example, the MFA trace (ii) will be represented as:  « 𝑛 . call-login (n, 1234)      login « 𝑚1 . call-mfa (m1, 100) ret-mfa (m1, 100) » mfa  binder « 𝑚2 . call-mfa (m2, 200) ret-mfa (m2, 200) » binders     ret-login »  Here, n is the name identifier for the login password, and m1 and m2 are the name identifiers for the first and the second mfa codes. The two occurrences of m1 must carry the same value (m1 , 100) . Similarly, the two occurrences of m2 should carry the same value (m2 , 200) . Since m1 and m2 are introduced by distinct binders with disjoint scopes, they can carry the same concrete values. However, m1 and n should carry distinct mfa code and login passwords as their binders are nested. The binders and the names record the structure needed by the policy: (a) where a value is introduced, (b) where it should be reused or not, (c) when the constraints around it should stop being relevant. This trace model buys us a notion of renaming concrete values while preserving the freshness and equality constraints on certain values. This is crucial for our policy’s semantics which should only depend on equality and inequality repetition patterns instead of concrete values. Therefore, SafeNom uses nominal words with binders as its trace model. The SafeNom policies are then interpreted over these nominal words with binders, rather than over flat sequences of concrete values. 2.3

SafeNom policy enforcement

A SafeNom policy is enforced using a nominal automaton-based runtime monitor. Binders in traces offer a syntax-directed way to enforce the property. When the monitor sees a binder, it records the fresh value at that position under the bound name. When it later sees the same name again, it checks that the value matches the recorded one. When a new binder is introduced inside the scope of another name, the monitor checks that the new value is fresh with respect to the currently

7

stored values. When the binder scope ends, the monitor can forget the value. Thus, the automaton does not need an ad-hoc implementation for each policy describing which values to remember, check, or drop. The monitor simulating the nominal automaton, first, converts the raw microservice trace with flat API events and concrete values into a nominal word by using symbolic finite transducer [Veanes et al. 2012].1 Then the nominal word output of the transducer is processed by the NA that recognizes the given policy. If the NA accepts the nominal word, then the corresponding raw microservice trace satisfies the property. 3

Nominal Languages for Data-Aware Properties

To understand the interpretation of a data-aware property as a nominal language, we present a refresher on nominal languages followed by our nominal languages extension motivated by the microservice setting. 3.1 Refresher: Nominal Languages with Binders Nominal languages [Kurz et al. 2012b] define sets of nominal words over a large (possibly infinite) domain of names N and a finite set of letters C, where the names can be tested for equality. This is useful in applications, like microservices, where a possibly large set of parameter values, session tokens, etc., can be viewed as N and the set of function or API names can be viewed as C. Nominal words [Kurz et al. 2012b] are given by the following grammar, where c ∈ C and n ∈ N : Nominal words 𝑤 ::= 𝜖 | c | n | 𝑤 · 𝑤 | «n.𝑤»

(1)

The first four cases describe the ordinary trace structure: an empty trace, an event from the finite alphabet, a data value from the large name domain, and sequential composition. The binder case «n.𝑤» is the key structure provided by nominal words. It introduces a scope for the name n in the word 𝑤. The occurrences of n inside this scope (i.e., inside the word 𝑤) are treated as occurrences of the same logical value (or name). To illustrate a nominal word, suppose that a successful file write requires a write call to occur between an open and a close call, where open and close should be passed the same session ID. We instantiate the grammar with session IDs as names N = N and session actions as a finite set of symbols C = {open, close, write}. A flat trace without any binder can only record the concrete session events and values: open 100 write close 100. This trace only describes that the concrete value 100 appears after both open and close. However, it does not record that the value after the open and close events are supposed to be occurrences of the same logical value of session ID and that only the 100s between open and close events are to be treated as session ID. We can express this using nominal words with binders as the following trace: «100. open 100 write close 100». Here, the binder « 100._» introduces a bound name 100 ∈ N . Within this scope, all occurrences of 100 are treated as uses of the same logical value, i.e., session ID. Meanwhile, «100. open 100 write close 200» is a nominal word of an invalid trace, where open and close are called with different session IDs. Thus, nominal words with binders offer a promising foundation to record the three structural aspects of data-aware traces that are required to check the properties in our microservice settings: 1 The SafeNom policy to transducer compilation is detailed in Appendix .

8

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

order of API events, the data values along with their positions, and the scope over which certain values are treated as the same logical value. The scoping aspect is a key tool for choosing nominal words with binders for interpreting our target properties that simply care about repetition of (in)equality patterns instead of concrete values in a run. A binder does not care about the concrete name it introduces. It only records the equality pattern among the occurrences of values in its scope. Therefore, the bound name is like a placeholder and replacing it consistently by another name gives an equivalent trace. For instance, «200. open 200 write close 200» represents the same pattern as the above trace, but with a different session ID 200. With respect to the above property, both are equivalent valid traces because the values used at close is the same as that introduced at open. This consistent renaming of bound names in a nominal word is called 𝛼-renaming. However, not every replacement of a bound name is valid. 𝛼-renaming of nominal words. To precisely state 𝛼-renaming, we first distinguish bound and free occurrences of names in a nominal word. An occurrence of a name is bound if it lies inside the scope of a binder that introduced the given name; otherwise it is free. For example, in 𝑤 1 = «n. n n m», the two occurrences of n are bound by the initial binder, while m is free as no binder binds it. Similarly, in the nominal word 𝑤 2 = «n. n n» n, the two occurrences of n inside the binder delimiters are bound, but the final n is free as it is outside the binder’s scope. 𝛼-renaming changes the name introduced by a binder together with its occurrences bound by that binder. For instance, in 𝑤 1 , we may rename the bound name n to p as: «n. n n m»

≡𝛼

«p. p p m».

These traces are said to be 𝛼-equivalent as the equality structure is unchanged: the first two names are bound occurrences of the same name and m remains free. The replacement name must not capture a freely occurring name. Thus, renaming n to m in 𝑤 1 is invalid: «n. n n m» .𝛼 «m. m m m». Here, the last occurrence of m was free in the original word, but it becomes bound in the renamed word. This changed the trace structure by adding an equality that was initially not present. Renaming does not affect occurrences of names outside the binder’s scope. For instance, if we rename n to p in 𝑤 2 , the last n remains unchanged: «n. n n» n

≡𝛼

«p. p p» n.

Nominal Regular Expressions. We can express the set of valid nominal words using a nominal regular expression (NRE) [Kurz et al. 2012b] given by the following grammar, where c ∈ C and n ∈ N: 𝑛𝑒 ::= 1 | 0 | c | n | 𝑛𝑒 + 𝑛𝑒 | 𝑛𝑒 · 𝑛𝑒 | 𝑛𝑒 ∗ | 𝜈 n.𝑛𝑒

(2)

Here, 1 matches the empty word 𝜖, 0 matches no word, c matches the same letter, and n matches the same name. NREs also support the usual union, concatenation, and Kleene star. A binder expression 𝜈 n.𝑛𝑒 matches words of the form «n.𝑤», where 𝑤 is matched by 𝑛𝑒. This binder expression also matches the 𝛼-renamings of «n.𝑤». Example 1. Consider using the binder expression 𝜈 100.open 100 write close 100 to specify the file write property. This NRE matches «100. open 100 write close 100». Although the NRE includes 100, it does not require that all the matching nominal words should have session ID set to 100. The session ID 100 in the above word could have been renamed to other names in N .

9

The key point is that the parameter values following open and close should be equal. For instance, «200. open 200 write close 200» is also accepted by the policy. We could have written this policy using the NRE 𝜈 200.open 200 write close 200 and yet it would have accepted the same set of valid traces. This invariance of the nominal language of an NRE under renaming of bound names is formally stated as the closure of nominal languages under 𝛼-renaming. Our extension. The nominal word accepted by the above NRE specification modeled the setting where the parameter value of open and close is observable at the binder, like “«100.”, before the actual call. However, in reality, a function or API call’s parameters are visible only after seeing the operation or API’s identifier. The nominal words model by Kurz et al. cannot express variants such as «_. open 100 write close 100», where the session ID 100 is unknown at the binder. This motivates our new notion of a lazy binder for modeling a microservice application’s execution trace as a nominal word. 3.2

Our Lazy Binding Extension

To support lazy binding, we extend Kurz et al.’s alphabet (comprising N and C) with a set N⊥ of partial names and a partial name map 𝜂 : N → N⊥ . Intuitively, a partial name is a logical identifier for a parameter, while a name corresponds to the actual value of a parameter. Below, we denote a partial name as n⊥ . We make two changes to the nominal words grammar in eq. (1): (a) add partial names n⊥ ∈ N⊥ , and (b) use partial names in binders, like « n⊥ ._» instead of a name n. Lazy nominal words 𝑤 ::= 𝜖 | c | n | n⊥ | 𝑤 · 𝑤 | « n⊥ .𝑤»

(3)

A name in the word between the binder delimiters is said to be bound and corresponding to n⊥ if the name is the first occurrence of a name that is mapped to n⊥ by 𝜂. For example, if 𝜂 (n1 ) = n⊥ , then in 𝑤 = « n⊥ .n1 »n2 , the name n1 is the bound name corresponding to n⊥ . We note that the nominal word representation of real-world execution traces (in §5) will not have free partial names, i.e., partial names appearing standalone without a binder « symbol. But our extended nominal words grammar allows free partial names as a technical device to define the semantics of our lazy NREs. We also make changes to the standard NRE grammar in eq. (2) and replace occurrences of names n ∈ N with partial names n⊥ ∈ N⊥ : Lazy NRE 𝑛𝑒 ::= 1 | 0 | c | n⊥ | 𝑛𝑒 + 𝑛𝑒 | 𝑛𝑒 · 𝑛𝑒 | 𝑛𝑒 ∗ | 𝜈 n⊥ .𝑛𝑒

(4)

The (lazy) binder expression in our grammar, 𝜈 n⊥ .𝑛𝑒, specifies a partial name n⊥ and occurrences of n⊥ in 𝑛𝑒 mark the positions in a word 𝑤 matched by 𝑛𝑒, where the name corresponding to n⊥ should appear. The formal semantics of our lazy NREs is as follows: Definition 2. The set of nominal words accepted by a lazy NRE 𝑛𝑒 is given by: 𝐿(1) ≜ {𝜖},

𝐿(0) ≜ ∅,

𝐿(c) ≜ {c},

𝐿( n⊥ ) ≜ { n⊥ },

𝐿(𝑛𝑒 1 + 𝑛𝑒 2 ) ≜ 𝐿(𝑛𝑒 1 ) ∪ 𝐿(𝑛𝑒 2 )

𝐿(𝑛𝑒 1 · 𝑛𝑒 2 ) ≜ 𝐿(𝑛𝑒 1 ) · 𝐿(𝑛𝑒 2 ) = {𝑤 · 𝑣 | 𝑤 ∈ 𝐿(𝑛𝑒 1 ), 𝑣 ∈ 𝐿(𝑛𝑒 2 )} Ø 𝐿(𝑛𝑒 ∗ ) = 𝐿(𝑛𝑒) 𝑗 , where 𝐿(𝑛𝑒)𝑖+1 = 𝐿(𝑛𝑒) · 𝐿(𝑛𝑒)𝑖 , and 𝐿(𝑛𝑒) 0 = {𝜖} 𝑗 ∈N

 𝐿(𝜈 n⊥ .𝑛𝑒) ≜

« m⊥ .𝑤»

𝑤 ′ ∈ 𝐿(𝑛𝑒), m⊥ ∈ { n⊥ } ∪ ( N⊥ \ 𝐹𝑉 (𝑤 ′ )), 𝑤 = 𝑤 ′ [ n⊥ ↦→ m], 𝜂 (m) = m⊥

 where

10

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

𝐹𝑉 (𝑤 ′ ) is the set of free partial names in 𝑤 ′ and the capture-avoiding substitution 𝑤 [ n⊥ ↦→ m] is defined as follows:  𝑤, if 𝑤 ∈ {𝜖, c, n}      m, if 𝑤 = n⊥       k⊥ ,  if 𝑤 = k⊥ and k⊥ ≠ n⊥ 𝑤 [ n⊥ ↦→ m] =  𝑤 1 [ n⊥ ↦→ m] · 𝑤 2 [ n⊥ ↦→ m], if 𝑤 = 𝑤 1 · 𝑤 2       « n⊥ .𝑤 ′ », if 𝑤 = « n⊥ .𝑤 ′ »      « k⊥ .𝑤 ′ [ n⊥ ↦→ m]», if 𝑤 = « k⊥ .𝑤 ′ » and k⊥ ≠ n⊥ .  Our semantics of the lazy binder expression differs from Kurz et al.’s semantics. We allow the partial name n⊥ to be renamed to any partial name m⊥ not appearing freely, i.e., without a binder in a word 𝑤 ′ ∈ 𝐿(𝑛𝑒) matched by the inner 𝑛𝑒. The word 𝑤 ′ will have free occurrences of n⊥ because it is not bound. Binding n⊥ substitutes all free n⊥ by a name m such that 𝜂 (m) = m⊥ . Example 3. Consider the lazy NRE 𝑛𝑒 = 𝜈 n⊥ . n⊥ n⊥ . The binder marks that the first and second symbols in the word between « n⊥ ._» should be some name n such that 𝜂 (n) = n⊥ . For example, 𝑛𝑒 matches 𝑤 = « n⊥ .nn». Similar to the NREs (in eq. (2)), our lazy NRE also accepts the renamed word 𝑤 ′ = « n′ ⊥ . n′ n′ », where n′ ⊥ = 𝜂 (n′ ). Example 4. Consider 𝑛𝑒 = (𝜈 n⊥ . n⊥ ) ∗ and names n and m, where 𝜂 (n) = n⊥ and 𝜂 (m) = m⊥ . This NRE matches words with repetition, like « n⊥ .n», « n⊥ .n»« m⊥ .m», « m⊥ .m»« m⊥ .m». Example 5. Consider 𝑛𝑒 = 𝜈 n⊥ .𝜈 m⊥ . m⊥ n⊥ and names n and m, where 𝜂 (n) = n⊥ and 𝜂 (m) = m⊥ . This NRE matches « n⊥ .« m⊥ .mn»». Permuting n⊥ and m⊥ gives another acceptable word « m⊥ .« n⊥ .nm»». Notice that NREs accept a language of closed nominal words where every name n in a word has a corresponding bound partial name 𝜂 (n). In the rest of the paper, by nominal words, we mean closed nominal words. 4

SafeNom: Nominal Language-based Policy Language

Now, we turn to instantiating the general constructs of lazy NRE and nominal words to the microservice setting. We let N = S × N, so names are pairs of a register 𝑛 ∈ S and a value 𝑢 ∈ N. Intuitively, 𝑢 is the concrete value of an API parameter or output, while the register 𝑛 is a logical identifier describing the binder in the policy that 𝑢 corresponds to. We let the set of partial names be N⊥ = {(𝑛, ⊥) | 𝑛 ∈ S} and the partial name map be 𝜂 ((𝑛, 𝑢)) = (𝑛, ⊥). The set of symbols C contains API names prefixed with call and ret, to denote API HTTP requests and responses. However, we need one refinement to support inequality constraints in SafeNom. According to the lazy NRE semantics (in theorem 2), a nested binder policy, like 𝜈 (𝑛, ⊥).𝜈 (𝑚, ⊥).(𝑛, ⊥) (𝑚, ⊥) will accept both «(𝑛, ⊥).«(𝑚, ⊥).(𝑛, 100) (𝑚, 200)»» and «(𝑛, ⊥).«(𝑚, ⊥).(𝑛, 100) (𝑚, 100)»». However, for a SafeNom policy, we want to enforce inequality between the value part of the names corresponding to the (nested) bound partial names, meaning «(𝑛, ⊥).«(𝑚, ⊥).(𝑛, 100) (𝑚, 100)»» should be rejected under the SafeNom semantics. We show that we can capture inequality relations by restricting the semantics of SafeNom to a class of well-formed words. As a further benefit, our SafeNom semantics satisfies a notion of 𝛼-equivalence.

11

4.1

SafeNom Semantics

Intuitively, a well-formed word for SafeNom should satisfy two constraints. Firstly, each bound partial name must be associated with only one (register, value) pair in the word. Secondly, to capture inequality, nested partial names must be associated with distinct values. To formally define these constraints, we introduce a few notations. Consider a nominal word with nested binders, like «(𝑛, ⊥).(𝑛, 1)«(𝑚, ⊥).(𝑚, 2)»«(𝑟, ⊥).(𝑟, 2)»». We call the set of partial names bound by nested binders between the outermost and some innermost binder as a binder path, and we let 𝑃𝑎𝑡ℎ𝑠 (𝑤) be the set of all paths in a word 𝑤. For instance, in the above word the set of all paths is {{(𝑛, ⊥), (𝑚, ⊥)}, {(𝑛, ⊥), (𝑟, ⊥)}}. For simplicity of presentation, we assume the bound partial names in SafeNom policies are all distinct; any SafeNom policy can be rewritten to bring it to this form. We can now define well-formed words: Definition 6. A nominal word 𝑤 is well-formed if, for every path 𝑝 ∈ 𝑃𝑎𝑡ℎ𝑠 (𝑤) the following conditions hold. (1) a unique name for any bound partial name: for any (𝑛 1, 𝑢 1 ), (𝑛 2, 𝑢 2 ) ∈ 𝑤, if 𝜂 ((𝑛 2, 𝑢 2 )) = 𝜂 ((𝑛 1, 𝑢 1 )) = (𝑛 1, ⊥) then 𝑛 1 = 𝑛 2 and 𝑢 1 = 𝑢 2 . (2) fresh nested names: the value parts (or the second projection) of the names corresponding to the bound partial names along the path 𝑝 are distinct. Example 7. The word «(𝑛, ⊥).(𝑛, 1)«(𝑚, ⊥).(𝑚, 2)»«(𝑟, ⊥).(𝑟, 2)»» is well-formed as all names of the form (𝑛, _) have value 1 and the value part of names (𝑛, 1), (𝑚, 2) bound by the partial names along the path {(𝑛, ⊥), (𝑚, ⊥)} are distinct. Similarly, along the other path, the names have distinct values 1 and 2. Finally, we are ready to define the SafeNom semantics: Definition 8. The set of nominal words accepted by a SafeNom policy 𝑛𝑒 is defined as SNomJ𝑛𝑒K = 𝐿(𝑛𝑒) ∩ WellForm, where WellForm is the set of well-formed nominal words. 4.2

Alpha-renaming in SafeNom

Consider a SafeNom policy that checks for equality between the first parameter of API calls to A and B: 𝜈 (𝑛, ⊥).callA (𝑛, ⊥) retA callB (𝑛, ⊥) retB. The acceptance of a word should only depend on the equality of parameter values at certain positions, rather than the specific values. We show this property holds for SafeNom by proving that SafeNom languages (like other nominal languages) are closed under a suitable notion of 𝛼-renaming. We define 𝛼-renaming of a well-formed nominal word as the application of a permutation (a bijection on N ), as usual: Definition 9 (Permutation Operation). Applying a (bijective) permutation 𝜋 : N → N to a lazy nominal word 𝑤 is defined as: 𝜋 (𝜖) ≜ 𝜖,

𝜋 (c) ≜ c,

𝜋 ( n⊥ ) ≜ n⊥ ,

𝜋 (n) ≜ m, where n ↦→ m ∈ 𝜋

𝜋 (𝑤 1 · 𝑤 2 ) ≜ 𝜋 (𝑤 1 ) · 𝜋 (𝑤 2 ) ( « m⊥ .𝜋 (𝑤)», if ∃n ∈ 𝑤 s.t. 𝜂 (n) = n⊥ and 𝜂 (𝜋 (n)) = m⊥ 𝜋 (« n⊥ .𝑤») ≜ « n⊥ .𝜋 (𝑤)», otherwise Example 10. Consider the well-formed word «(𝑛, ⊥).«(𝑚, ⊥).call-A (𝑛, 100) call-B (𝑚, 200)»» capturing that API A is called with parameter value 100 and B is called with parameter value 200. When permuted using 𝜋, where 𝜋 (𝑛, 100) = (𝑚, 200) and 𝜋 (𝑚, 200) = (𝑛, 100), we get «(𝑚, ⊥).«(𝑛, ⊥).call-A (𝑚, 200) call-B (𝑛, 100)»». This denotes another execution trace where A was called with value 200 and B was called with 100.

12

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

In the above example, applying a permutation to a well-formed word produces another wellformed word. However, applying the permutation with 𝜋 (𝑛, 100) = (𝑛, 200) above gives: «(𝑚, ⊥).«(𝑛, ⊥).call-A (𝑚, 200) call-B (𝑛, 200)»», which is not well-formed. Thus, to establish 𝛼-equivalence, we must work with a restricted set of permutations. To define these permutations, we introduce some notation. We let reg : S × N → S and val : S × N → N denote the first and second projections. We define the restricted domain of a path 𝑝 (the set of names corresponding to the partial names along the path) to be 𝐷 𝑝 = {(𝑛, 𝑢) ∈ 𝑤 | (𝑛, ⊥) ∈ 𝑝 and 𝜂 ((𝑛, 𝑢)) = (𝑛, ⊥)}, and we let val(𝐷 𝑝 ) ≜ {𝑢 | (𝑛, 𝑢) ∈ 𝐷 𝑝 }. Definition 11 (Valid SafeNom Permutation). Consider a well-formed nominal word 𝑤. Let the restricted permutation for any 𝑝 ∈ 𝑃𝑎𝑡ℎ𝑠 (𝑤) be 𝜋 ↾𝐷𝑝 : 𝐷 𝑝 → 𝜋 (𝐷 𝑝 ), the restricted value and name projection functions be val ↾𝐷𝑝 : 𝐷 𝑝 → val(𝐷 𝑝 ) and reg ↾𝐷𝑝 : 𝐷 𝑝 → reg(𝐷 𝑝 ), respectively. A permutation 𝜋 is valid for 𝑤 if for any path 𝑝 ∈ 𝑃𝑎𝑡ℎ𝑠 (𝑤): (1) the value transposition 𝑉𝑝 : val(𝐷 𝑝 ) → val(𝜋 (𝐷 𝑝 )) is a bijection: 𝑉𝑝 (𝑢) = val ↾𝐷𝑝 (𝜋 ↾𝐷𝑝 (val ↾𝐷−1𝑝 (𝑢))), (2) the register transposition 𝑅𝑝 : reg(𝐷 𝑝 ) → reg(𝜋 (𝐷 𝑝 )) is a bijection: 𝑅𝑝 (𝑢) = reg ↾𝐷𝑝 (𝜋 ↾𝐷𝑝 (reg ↾𝐷−1𝑝 (𝑢))). Note that the set of valid permutations depends on the word 𝑤. However, the sets of valid permutations are closely related: there is a bijection that maps every valid permutation for a well-formed word to a unique permutation that is valid for the 𝛼-renamed permuted word. Theorem 12. Let 𝑤 1 be a well-formed word with some valid permutation 𝜋 ∈ 𝑆 (𝑤 1 ), which permutes 𝑤 1 to 𝑤 2 = 𝜋 (𝑤 1 ). The function 𝑃𝑒𝑟𝑚 : 𝑆 (𝑤 1 ) → 𝑆 (𝑤 2 ) defined as 𝑃𝑒𝑟𝑚(𝜋1 ) = 𝜋 2 , where 𝜋 2 (𝑥) = 𝜋 1 (𝜋 −1 (𝑥)) is a bijection. We defer the proofs of this section’s theorems to Appendix . Applying a valid permutation to a word gives an 𝛼-equivalent word: Definition 13. Well-formed words 𝑤 1 and 𝑤 2 are said to be 𝛼-equivalent, i.e., 𝑤 1 ≡𝛼 𝑤 2 if there exists a valid permutation 𝜋 for 𝑤 1 such that 𝑤 2 = 𝜋 (𝑤 1 ). As expected, ≡𝛼 is an equivalence relation: Theorem 14. The ≡𝛼 relation is symmetric, reflexive and transitive. Finally, we can show that SafeNom policies are closed under 𝛼-equivalence. Theorem 15. Let 𝑛𝑒 be a SafeNom policy and 𝑤 1, 𝑤 2 be two well-formed nominal words such that 𝑤 1 ≡𝛼 𝑤 2 . If 𝑤 1 ∈ L (𝑛𝑒) then 𝑤 2 ∈ L (𝑛𝑒).

13

Thus, SafeNom policies do not depend on specific parameter values of API calls and returns, but only on the (in)equality relation across parameter values. 5

Case Studies

In this section, we highlight the expressiveness of SafeNom features using realistic case studies. Below, the API names are prefixed with call and ret to denote the API’s request and response, respectively. We write 𝑆, where 𝑆 = {𝑠 1, . . . , 𝑠𝑛 }, as the shorthand for the regular expression (𝑠 1 + · · · + 𝑠𝑛 ) and !𝑆 for (C − 𝑆) ∗ . Static data/configuration. SafeNom can express properties where the exact values that appear at certain positions is statically known, like a Boolean error code, region identifiers, etc., using regular expression patterns over constants C. For instance, consider a GDPR compliance regulation that mandates that the data of user in the EU region should not be stored in a US region’s database to avoid violating data storage guidelines. Consider the following two APIs in the database-backed application: API User, which takes the region of the user as its parameter, and API DB that takes in the region of the database to which it writes. The GDPR policy can be stated as: after a call to call-User with EU ∈ C, any call to call-DB should be passed EU to avoid cross-region writes. This is specified as follows: call-User EU ( !{call-DB} + call-DB EU ) ∗, where !{call-DB} allows any other APIs to be invoked without any restrictions. This policy accepts the following trace: call-User EU call-DB EU ret-DB call-DB EU ret-DB ret-User, but rejects the trace call-User EU call-DB US ret-DB call-DB ret-DB call-DB ret-DB ret-User because the first DB is writing to the US region and additionally the second DB write did not carry the region identifier. This class is useful when a policy depends on simple tags or flags. For example, a deployment team may use version tags for A/B testing to ensure that an end-to-end request is served by the same API version; a security team may use traffic origin tags to prevent external requests from reaching confidential internal services; and a development team may route paid and unpaid users to different feature APIs based on some account-tier tags. Equality check. Unlike the above policy over the constant region identifier, some properties require two or more API events to carry the same (runtime) parameters or responses. We express such properties using SafeNom’s binder construct. Such policies arise when services must agree on dynamic values, like request identifiers, session tokens, transaction IDs, etc. For example, a tracing policy may require all downstream APIs to use the same trace ID (which will be assigned at runtime); an authorization policy may require all the database accesses to use the same session ID. As a representative example, consider the following APIs in a CI/CD build pipeline: a build API Build that takes in an identifier for the build session it starts; and a container creation API Container that takes the identifier to tag the container’s image. To avoid wastage of resources, a deployment team requires that exactly one container image tagged with the same identifier as the build session should be created. In the following SafeNom policy, id⊥ represents any identifier

14

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

and all instances of id⊥ are required to have the same identifier: 𝜈 id⊥ . call-Build id⊥ !{call-Container, ret-Container, call-Build, ret-Build} call-Container id⊥ ret-Container !{call-Container, ret-Container, call-Build, ret-Build} ret-Build The pattern between call-Build and ret-Build disallows more than one occurrence of call-Container, and requires that occurrence to carry the same id bound at Build. The following two traces illustrate an accepted run (left) and a rejected run (right), where the Container call either repeats or carries a mismatched value: « (𝑖𝑑, ⊥) . call-Build (𝑖𝑑, 100) call-Container (𝑖𝑑, 100) ret-Container ret-Build» ✓ accepted

« (𝑖𝑑, ⊥) . call-Build (𝑖𝑑, 100) call-Container (𝑖𝑑, 200) ret-Container call-Container (𝑖𝑑, 100) ret-Container ret-Build» ✗ rejected

✗ extra

Inequality check. Developers often want to check that an API generates fresh data, transforms an input before forwarding it, or returns multiple distinct values. Such requirements appear when raw input to an encryption service should be different from its encrypted response, a backup copy should be stored in a different region than the primary region, or a user may create a new sub-task with a different session ID. Such properties can be stated as an inequality between nested bound names. As a representative example, consider the following APIs that implement a secure handshake protocol: a frontend API frontend that initiates the handshake, a key generation API KeyGen that responds with a public key followed by a private key, an API Client that takes in a key as a parameter and publishes its input to the client, and a similar API Server that takes a key and publishes it to the server. Suppose the protocol requires that the public and private keys generated by KeyGen should be unique and the client should publish the public key, while the server should publish the private key. This can be specified as the following policy, where the pattern of pub⊥ marks that the ret-KeyGen’s public key response should be equal to the key published to the client, and the pattern of pvt⊥ marks that the ret-KeyGen’s private key response should be equal to the key published to the server: 𝜈 pub⊥ . 𝜈 pvt⊥ .call-Frontend call-KeyGen ret-KeyGen pub⊥ pvt⊥ call-Client pub⊥ ret-Client call-Server pvt⊥ ret-Server ret-Frontend The nested binders implicitly specify the inequality between pub⊥ and pvt⊥ . The following accepted trace on the left uses distinct public and private keys and each is published to the correct party. Meanwhile, the trace on the right is rejected because the public and the private key coincide.

15

« (𝑝𝑢𝑏, ⊥) . « (𝑝𝑣𝑡, ⊥) . call-frontend call-KeyGen ret-KeyGen (𝑝𝑢𝑏, 𝐴4) (𝑝𝑣𝑡, 𝐶2) call-Client (𝑝𝑢𝑏, 𝐴4) ret-Client call-Server (𝑝𝑣𝑡, 𝐶2) ret-Server ret-frontend » » ✓ accepted

« (𝑝𝑢𝑏, ⊥) . « (𝑝𝑣𝑡, ⊥) . call-frontend call-KeyGen ret-KeyGen (𝑝𝑢𝑏, 𝐴4) (𝑝𝑣𝑡, 𝐴4) call-Client (𝑝𝑢𝑏, 𝐴4) ret-Client call-Server (𝑝𝑣𝑡, 𝐶2) ret-Server ret-frontend » » ✗ rejected

Repeated (local) equality check. Running multiple iterations of an operation, each time with (short-lived) independent data is common in applications. For instance, login retries with refreshed keys, multiple file transfers with per-file checksums, CI/CD build retries with their own build IDs, etc. The key here is that the equality constraint is local to one iteration of the operation. All APIs in the same iteration should agree on that iteration’s value, but different iterations may use different local values. In SafeNom, policies on one iteration’s data can be stated using binders. This can be extended to a sequence of independent (per-iteration) constraints using a Kleene star. Consider an authenticator application implemented using: frontend API Auth that initiates a login; API Gen that runs a random number generator and responds with a new short-lived PIN; API Pin that returns a new PIN by calling Gen and returning the PIN in Gen’s response. The authenticator is allowed to retry login by refreshing PINs. The retries can be captured using a Kleene star around pin⊥ ’s binder: call-Auth (𝜈 pin⊥ .call-Pin call-Generate ret-Generate pin⊥ ret-Pin pin⊥ ) ∗ ret-Auth Here, pin⊥ is bound for the scope of one PIN generation request to API Pin: it must satisfy an equality constraint within each iteration, but it may differ across iterations. For instance, the accepted trace on the left uses PIN 100 in the first iteration and 200 in the second, and in each iteration the same PIN that was sampled is passed through the Generate API. Meanwhile, the second trace is rejected because the Generate API returned a PIN that is different from the one sampled by the Pin API. call-Auth « (𝑝𝑖𝑛, ⊥) .call-Pin call-Generate ret-Generate (𝑝𝑖𝑛, 100) ret-Pin (𝑝𝑖𝑛, 100) » « (𝑝𝑖𝑛, ⊥) .call-Pin call-Generate ret-Generate (𝑝𝑖𝑛, 200) ret-Pin (𝑝𝑖𝑛, 200) » ret-Auth ✓ accepted

call-Auth « (𝑝𝑖𝑛, ⊥) .call-Pin call-Generate ret-Generate (𝑝𝑖𝑛, 100) ret-Pin (𝑝𝑖𝑛, 100) » « (𝑝𝑖𝑛, ⊥) .call-Pin call-Generate ret-Generate (𝑝𝑖𝑛, 200) ret-Pin (𝑝𝑖𝑛, 100) » ret-Auth ✗ rejected

Repeated (global) equality check. Developers might want to express that certain data is unmutated or that some API call’s response is the same across invocations. For example, all calls in a transaction should carry the same transaction ID. In these cases, the value is introduced once and then reused many times. The number of reuses is not fixed in advance. SafeNom can specify such properties as unrestricted repetition of some equal values using a Kleene star around the partial

16

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

names. Consider the frontend API Frontend that is the entry service of the application and two arbitrary APIs A and B that both take in a request ID parameter to identify the initial request for which the API calls are being invoked. For end-to-end observability, deployment teams rely on frontend Frontend to carry a request identifier, which is passed unchanged to all downstream APIs during the execution to mark the APIs that are part of the same execution trace. We can specify this by binding a single reqID⊥ and repeatedly using it across all requests invoked while serving a call to Frontend: 𝜈 reqID⊥ . call-Frontend (call-A reqID⊥ + ret-A + call-B reqID⊥ + ret-B + _) ∗ ret-Frontend The reqID⊥ is in scope for the entire execution. Using the Kleene star, we express that any call or return symbol can occur while serving F provided that the call symbols carry the reqID⊥ as their first parameter. The trace on the left satisfies this property as it consistently uses the same request ID. However, the trace on the right is rejected because the third child API to B does not carry a request ID and also the request ID in the fourth child is different from the global identifier. « (𝑟𝑒𝑞𝐼 𝐷, ⊥) . call-Frontend call-A (𝑟𝑒𝑞𝐼 𝐷, 100) ret-A call-A (𝑟𝑒𝑞𝐼 𝐷, 100) ret-A call-B (𝑟𝑒𝑞𝐼 𝐷, 100) ret-B call-A (𝑟𝑒𝑞𝐼 𝐷, 100) ret-A ret-Frontend» ✓ accepted 6

« (𝑟𝑒𝑞𝐼 𝐷, ⊥) . call-Frontend call-A (𝑟𝑒𝑞𝐼 𝐷, 100) ret-A call-A (𝑟𝑒𝑞𝐼 𝐷, 100) ret-A call-B ret-B ✗ call-A (𝑟𝑒𝑞𝐼 𝐷, 200) ret-A ret-Frontend» ✗ rejected

Enforcement: Lazy Nominal Automaton

Nominal languages are recognized by nominal automata. We extend Kurz et al.’s nominal automata (NA) model [Kurz et al. 2012b], which supported only names and equality checks between names, to additionally support partial names for lazy binding and inequality checks on names. In this section, we work with non-deterministic NAs with 𝜖-transitions. In the following definition of our extended (lazy) nominal automata, we use the following notation [𝑖] ≜ {1, . . . , 𝑖}, where 𝑖 ∈ N. Definition 16 (Non-deterministic lazy N𝑓 𝑣 -nominal automaton). Let N be the set of names, N⊥ be the set of partial names, C be the set of constants, and N𝑓 𝑣 ⊆ N⊥ be a finite set of partial names. A N𝑓 𝑣 -nominal automaton is a tuple H = (𝑄, 𝑞 0, 𝐹, Δ, N𝑓 𝑣 ), where: (1) 𝑄 is the finite set of states equipped with a map ∥·∥ : 𝑄 → N, (2) 𝑞 0 ∈ 𝑄 is the initial state and ∥𝑞 0 ∥ = 0, (3) 𝐹 ⊆ 𝑄 is the set of final states and for all 𝑞 ∈ 𝐹 , ∥𝑞∥ = 0. (4) Δ : 𝑄 × (𝐼 N𝑓 𝑣 ∪ {𝜖}) → 2𝑄 , where 𝐼 N𝑓 𝑣 = C ∪ N𝑓 𝑣 ∪ {𝑖 ∈ [∥𝑞∥] | 𝑞 ∈ 𝑄 } ∪ {«, »}, and for any 𝑞 ∈ 𝑄 and 𝑞 ′ ∈ Δ((𝑞, 𝛼)) the following holds: 𝛼 = « =⇒ ∥𝑞 ′ ∥ = ∥𝑞∥ + 1 𝛼 = » =⇒ ∥𝑞 ′ ∥ = ∥𝑞∥ − 1 𝛼 ∈ (𝐼 N𝑓 𝑣 \ {«, »}) ∪ {𝜖} =⇒ ∥𝑞 ′ ∥ = ∥𝑞∥ The states in NA are stratified into levels, where 𝑞 is at level ∥𝑞∥. A transition from 𝑞 on « should go to a state in the next level. Similarly, transitions on » drop down to a state in the previous level. Transitions on constants, partial names in N𝑓 𝑣 , (state) levels, and 𝜖 preserve the level of the source state.

17

A lazy nominal automaton is deterministic if it has a single initial state and for any 𝑞 and 𝛼, Δ((𝑞, 𝛼)) is a singleton set. Operationally, an NA processes a nominal word as a sequence of tokens of the form ‘« n⊥ .’, ‘»’ or symbols in N, C, or N⊥ , reading the tokens from left to right. An NA’s configuration is a pair ⟨𝑞, 𝜎⟩ of a state 𝑞 and a store 𝜎 : [∥𝑞∥] → (N ∪ N⊥ ) × 2 N . The store tracks the names currently in scope. An entry 𝜎 (𝑖) = (𝑎, Γ) records that register 𝑖 currently holds the (partial) name 𝑎 ∈ N ∪ N⊥ for (in)equality checks, and that 𝑎 may later not be resolved to any names in the forbidden set Γ. We write fst(𝜎 (𝑖)) and snd(𝜎 (𝑖)) for the first name component and the second forbidden set component. The small-step semantics of our lazy NA extended with inequality checks and lazy binding is defined as the following transition relation on configurations. Below, we use 𝜎 ↾ [𝑖 ] to denote the restriction of 𝜎 to the domain [𝑖]. We write 𝐼𝑚𝑔fst (𝜎) ≜ {𝑎 | (𝑎, 𝑠) ∈ 𝐼𝑚𝑔(𝜎)} and similarly 𝐼𝑚𝑔snd (𝜎) for the second projections of 𝐼𝑚𝑔(𝜎). We write n#𝑆 when the name n is fresh for every name in set of (partial) names 𝑆. For ordinary nominal words, this is n ∉ 𝑆. For SafeNom names of the form (𝑛, 𝑢), the freshness check (𝑛, 𝑢)#𝑆 holds iff for every name (𝑚, 𝑣) ∈ 𝑆, we have 𝑢 ≠ 𝑣. Definition 17 (Single step transition). Given 𝑞, 𝑞 ′ ∈ 𝑄 and two configurations 𝑡 = ⟨𝑞, 𝜎⟩ and 𝑠 𝑡 ′ = ⟨𝑞 ′, 𝜎 ′ ⟩, a nominal automaton moves from 𝑡 to 𝑡 ′ on some symbol 𝑠, written 𝑡 → − 𝑡 ′ , if there

exists a transition symbol 𝛼 ∈ 𝐼 N𝑓 𝑣 ∪ {𝜖} such that 𝑞 ′ ∈ Δ((𝑞, 𝛼)) and  if 𝑠 = « n⊥ . then 𝛼 = « and 𝜎 ′ = 𝜎 [||𝑞 ′ || ↦→ ( n⊥ , ∅)]      if 𝑠 = n ∈ N then 𝛼 ∈ [∥𝑞∥] s.t. ∀𝑗 > 𝛼 . 𝜂 + (fst(𝜎 (𝛼))) ≠ 𝜂 + (fst(𝜎 ( 𝑗))) and       𝜎 ′ = 𝜎, if fst(𝜎 (𝛼)) = n         𝜎 ′ = 𝜎 [𝛼 ↦→ (n, ∅)], if fst(𝜎 (𝛼)) = 𝜂 (n),         n#𝐼𝑚𝑔fst (𝜎) and        n#snd(𝜎 (𝛼))       𝜎 ′ = 𝜎 [ | |𝑞 ′ | | ] , if fst(𝜎 (||𝑞||)) ∈ N⊥         if 𝑠 = » then 𝛼 = » and 𝜎 ′ = 𝜎 [||𝑞 ′ ||], s.t.        ∀ 𝑖 ∈ [||𝑞 ′ ||], fst(𝜎 (𝑖)) ∈ N⊥ =⇒ snd(𝜎 ′ (𝑖)) = snd(𝜎 (𝑖)) ∪ {fst(𝜎 (||𝑞||))}        if 𝑠 = 𝜖 then 𝛼 = 𝜖 and 𝜎 ′ = 𝜎     if 𝑠 ∈ C ∪ N𝑓 𝑣 \ 𝐼𝑚𝑔fst (𝜎) then 𝛼 = 𝑠 and 𝜎 ′ = 𝜎  where 𝜂 + ( n⊥ ) = n⊥ and 𝜂 + (n) = 𝜂 (n) for any n⊥ and n. On reading a symbol 𝑠 at a configuration, the automaton picks a valid transition symbol 𝛼 to get the next configuration state. The store update during a transition depends on the token read. (1) A transition on the lazy binder “« n⊥ .” extends the store with the level of the new state 𝑞 ′ mapped to the partial name n. The index of a (partial) name in the store marks the recency of reading the binder associated with the name, with a greater index denoting a more recent binder. (2) A transition on n captures the most important detail of our extended NA semantics for (in)equality checks on names. The automaton first resolves the binder corresponding to n—the partial name associated with the binder should be the same as 𝜂 (n). Operationally, the NA searches for a transition symbol 𝛼 such that either the name stored at 𝜎 (𝛼), i.e. fst(𝜎 (𝛼)) is n or n⊥ . Since there might be many such indices, the NA resolves n to the most recent (innermost) binder; thereby supporting shadowing. In case fst(𝜎 (𝛼)) = n⊥ , the NA also needs to ensure that the current name n being read is distinct from the names

18

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

start

𝑞0

«

𝑞1

1

𝑞2

𝛼=«

𝛼=1

𝑠=«(𝑛,⊥)

𝑠=(𝑛,100)

1

𝑞3

»

𝑞4

⟨𝑞 0, {}⟩ −−−−−−−→ ⟨𝑞 1, {1 ↦→ ((𝑛, ⊥), ∅)}⟩ −−−−−−−→ ⟨𝑞 2, {1 ↦→ ((𝑛, 100), ∅)}⟩ → − . . .→ − ⟨𝑞 4, {}⟩ Fig. 2. Nominal automaton that accepts SNomJ𝜈 (𝑛, ⊥).(𝑛, 100)(𝑛, 100)K.

in: (a) the set 𝐼𝑚𝑔fst (𝜎) of names in the current store, and (b) the forbidden set for this register, i.e., snd(𝜎 (𝛼)). The freshness check against 𝐼𝑚𝑔fst (𝜎) prevents the new name from coinciding with other names that are currently in scope and, thus, in the registers. The second check prevents the new name from coinciding with an old name that was bound in an inner scope that has ended. Such names no longer occur in the current store image and are therefore retained in the register’s forbidden set. Once both checks succeed, register 𝛼 is updated to (n, ∅). The forbidden set is then discarded because once the name has been stored at a register, the role of the forbidden set is complete. (3) A transition on » closes the most recent binder scope, erases its register content, and updates the NA state. If the erased register contains a name, the NA adds that name to the forbidden set of every remaining register that holds a partial name. This propagation preserves the freshness constraint after the current bound name disappears from the current store. It is necessary because in the future, if a name is bound to one of the outer binders associated with the registers holding only partial names, the chosen name must be distinct from all names bound in inner scopes during the outer binder’s lifetime. Registers that already contain names are not updated because their contents are already fixed and will not undergo another freshness check. (4) Transitions on constants, (free unbound) partial names and 𝜖 only update the state. Note that the last transition rule handles (free) partial names in N𝑓 𝑣 that are not bound (i.e., not in the current store’s image). Example 18. Consider the NA H𝑛𝑒 in fig. 2 for the following SafeNom policy: 𝑛𝑒 = 𝜈 (𝑛, ⊥).(𝑛, 1) (𝑛, 1). Here, 𝑞 0 is the initial state and 𝑞 4 is the final state, and a transition labeled with 𝛼 from some state 𝑞𝑖 to another 𝑞 𝑗 denotes 𝑞 𝑗 ∈ Δ((𝑞𝑖 , 𝛼)). In the run of the word «(𝑛, ⊥).(𝑛, 100) (𝑛, 100)», the NA first transitions from the initial state on the symbol 𝛼 = « and adds the partial name (𝑛, ⊥) and empty forbidden set in the store indexed by the binder’s level, i.e., 1; then on the name (𝑛, 100), the NA transitions on symbol 𝛼 = 1, which is the store’s index mapping to the partial name corresponding to (𝑛, 100); and so on. Finally, the NA accepts the word by arriving at the final state with an empty store. The following example illustrates how the forbidden sets enforce freshness with respect to names whose scopes have already ended. Example 19. Consider the policy: 𝜈 (𝑛, ⊥).(𝜈 (𝑚, ⊥). (𝑚, ⊥)) (𝑛, ⊥), which requires the names bound to (𝑛, ⊥) and (𝑚, ⊥) to be distinct. Importantly, in a trace, a name will be bound to the outer binder only after the scope of the inner binder has ended. Consider the word: « (𝑛, ⊥).« (𝑚, ⊥). (𝑚, 100) »(𝑛, 200)». Suppose after reading the two binders, the store contains 𝜎 (1) = ((𝑛, ⊥), ∅) and 𝜎 (2) = ((𝑚, ⊥), ∅). Reading (𝑚, 100) will update the second register to 𝜎 (2) = ((𝑚, 100), ∅). When the inner scope closes, the NA will erase the second register. Since the first register still holds a partial name,

19

(𝑚, 100) will be added to its forbidden set, resulting in 𝜎 (1) = ((𝑛, ⊥), {(𝑚, 100)}). The subsequent transition on (𝑛, 200) will succeed because it is distinct from every name in the forbidden set. In contrast, the word «(𝑛, ⊥). «(𝑚, ⊥). (𝑚, 100) » (𝑛, 100) » is rejected because the freshness check against the forbidden set is violated. However, if our freshness check was limited to only the currently stored names in the registers, we would have incorrectly accepted the trace. This example highlights a subtlety of supporting freshness with lazy binders. We write L (H ) for the language of a nominal automaton H : the set of all accepted words. These languages are closed under 𝛼-equivalence: Theorem 20. Consider a lazy N𝑓 𝑣 -nominal automaton H . For any two 𝛼-equivalent well-formed words 𝑤, 𝑤 ′ , if 𝑤 ∈ L (H ) then 𝑤 ′ ∈ L (H ). The proof for this theorem and the others in this section are in the Appendix. Our SafeNom policy to NA compiler. A SafeNom policy is compiled into a deterministic NA using Kurz et al.’s Thompson-style inductive construction of an NA from an NRE. Our compilation details can be found in Appendix ; here, we summarize its main cases. Let H𝑛𝑒 denote the NA constructed for a policy 𝑛𝑒. • H0 is a single-state NA with no transitions and no final state. H1 is a single state NA with no transitions and a final state that is the same as the initial state. • Each of Hc and H n⊥ is a two-state NA with a singleton transition on c and n⊥ , respectively. • For the binder case H𝜈 n⊥ .𝑛𝑒 , the construction introduces new initial and final states. The new initial state enters H𝑛𝑒 on “ «” and the final state of H𝑛𝑒 transitions to the new final state on ». Within H𝑛𝑒 , every transition labeled by the bound partial name n⊥ is replaced by a transition labeled 1, the register level of the newly introduced binder. Wrapping 𝑛𝑒 in this binder shifts every binder already occurring inside 𝑛𝑒 one level deeper. Accordingly, each existing transition labeled by a level 𝑖 is relabeled by 𝑖 + 1. • For the union, concatenation, and Kleene star cases, the construction goes through a Thompson-style construction [Thompson 1968]. Finally, the resulting non-deterministic NA is converted into a deterministic NA using Kurz et al.’s layer-wise powerset construction. As expected, our compilation procedure is sound: Theorem 21. Let 𝑛𝑒 be a SafeNom policy. Then SNomJ𝑛𝑒K = L (H𝑛𝑒 ), i.e, 𝑤 matches 𝑛𝑒 iff H𝑛𝑒 accepts 𝑤. 7

Implementation

To demonstrate our policy checking design for a microservice application, we implemented a prototype in ∼ 3000 lines of Java. Given a SafeNom policy, our tool compiles a nominal automaton. Then the tool extracts runtime monitors, each of which simulates the compiled NA’s transitions atop the Istio service mesh [Istio 2024a], a new networking layer. Each service has a co-located monitor, as shown in fig. 3, running outside the service without any invasive changes to the service implementations. The runtime monitoring is distributed across the (local monitors at) services.

20

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

The monitor at a service runs when the given service sends or receives an HTTP message. Our monitor’s Istio-specific design aspects are described below. Istio-based design. Service mesh design enables blackbox enforcement of our safety properties. In an application deployed on top of the Istio service mesh, each microservice runs in an independent (service) container and is paired with a co-located sidecar container that implements an Envoy proxy [Envoy 2024]. The proxy intercepts all HTTP requests and responses corresponding to its service and can read the HTTP message headers, query parameters, response values, add/delete/update the headers, or allow/block HTTP messages. We implement our monitor in the proxy using a WebAssembly Envoy filter [Istio 2026]. These filters can be dynamically plugged into the sidecar proxy. Thus, SafeNom can be deployed dynamically without modifying service implementations. From HTTP events to nominal words. The proxy can only observe API call/return events and the parameters, but the NA needs its input to be nominal words. To bridge this gap, we insert a lightweight parsing stage in the monitor to reconstruct the implicit nominal structure in the trace before running the nominal automaton. The parser is a symbolic finite-state transducer compiled from the SafeNom policy being enforced. The transducer’s role is to simply parse the flat sequence of API events, extract the relevant parameter values, and insert nominal tokens, like binder delimiters at positions specified by the policy. The transducer does not perform the semantic checks for equality, freshness, or scope; these checks are performed by the NA. Thus, the monitoring pipeline separates parsing from enforcement. Consider a policy requiring the ID received by Frontend to be the same as the ID used to look up data in a database: 𝜈 id⊥ . call-Front id⊥ . call-DB id⊥ ret-DB ret-Front . . . Suppose call-Front received input 100. Since the policy says that id⊥ gets bound at call-Front, the transducer emits an opening binding delimiter « (𝑖𝑑, ⊥) ., followed by call-Front; then the policy specifies that the name following call-Front should be bound to id⊥ , so the transducer parses the value 100 observed in the raw trace and emits (𝑖𝑑, 100) . At each step the transducer updates its local state. These four tokens then get fed to the NA located at the sidecar proxy at the Front service. The NA updates its states and pushes the name (𝑖𝑑, 100) in the first register. This separation is useful as the transducer handles the syntactic parsing while the NA handles the policy checking. Monitor configuration. The monitor’s configuration—transducer state, the NA state, and the NA store—is carried as custom HTTP headers as shown in fig. 3. When an HTTP message arrives at a monitor, the transducer and the NA run in lockstep. First, the transducer reads its current state from the HTTP headers and transitions on the sequence of API names and parameter values carried in the message. The value of the transducer’s old state header is updated with the transducer’s new state and the transducer’s output tokens are fed to the NA. Then, the NA reads its current configuration headers and transitions on the input tokens. The value of the NA’s old state header is updated with the NA’s new state. The update to the headers encoding the NA store requires some care. On reading a token of the form “«(𝑛, ⊥).”, the monitor adds a new header named 𝑛 and sets its value to ⊥. This corresponds to extending the store with (𝑛, ⊥). Meanwhile, on reading », the most recently added header in the store is removed. On reading a parameter value, the relevant store headers are compared for (in)equality. Note that the services are responsible for propagating the headers from the parent to the child request/response for distributed monitoring.

21

Deterministic transducer. Since our monitor is online, the transducer must be deterministic because the transducer cannot backtrack to change its output. After reading a prefix of the trace, the transducer should determine what symbol to output simply by looking at the next event. For example, consider the above policy were part of some bigger policy, and below is a small sub-expression of that policy: . . . (call-Front ret-Front) ∗ 𝜈 id⊥ . call-Front id⊥ call-DB id⊥ ret-DB ret-Frontend . . . Here, Front may be invoked repeatedly, but starting from some intermediate invocation, the monitor must bind the name id⊥ . However, a transducer cannot determine the occurrence of call-Front at which it should introduce the binder for id⊥ . Disambiguating the position matched by a symbol without more than one-symbol lookahead is central for an online transducer to emit the binder delimiters at correct positions and correctly parse the required data from the API parameters. To avoid such cases, we enforce a syntactic well-formedness requirement on policies used for online monitoring. The condition is stated on the sequence of observable API events obtained by erasing all binder annotations from the policy. Intuitively, the regular expression skeleton we get after ignoring the binder annotations, must have a unique left-to-right parse. Formally, the binder-free regular expression skeleton of the SafeNom policy being monitored should be oneunambiguous. One-unambiguity lets the transducer deterministically choose the position in the NRE from which the currently read symbol has been generated. The benefit of this condition is that it makes the monitor frontend deterministic by construction while keeping the NA’s semantics unchanged. This is crucial for an online monitor. We can statically check the well-formedness of a property using the definition in Appendix. Also, a detailed explanation of the transducer construction is given in the Appendix. Rejecting invalid traces. For simplicity, our prototype logs any policy violation by checking if after processing the trace, the NA is in an accepting configuration or not. However, it is possible to actively block intermediate HTTP messages as soon as the NA’s rejecting configuration is reached. 8

Evaluation

We evaluate SafeNom monitor’s memory footprint and performance overhead by answering the following research questions: • RQ1: How much header space is required for the configuration headers? • RQ2: How much latency overhead does the monitor add? We evaluate SafeNom on a suite of policies that cover the main language constructs. The SafeNom monitor is deployed in an Istio-enabled Kubernetes cluster. We instantiate the policy suite on two Gobased microservice applications: a hospital workflow and a hotel reservation application [Gan et al. 2019] running in the cluster. The average number of nodes in the service tree of both applications is 6 and 4.5, respectively. Since SafeNom runs outside the application, its performance overhead is not affected by the application’s internal implementation. However, it depends on the policies being checked, which we evaluate. The case studies and the detailed deployment information are in Appendix .

22

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

docker

HTTP to B Config: 𝑋

docker

Service A

Service B

1

3

HTTP to B Config: 𝑌

HTTP to B Config: 𝑋

envoy

envoy

2

NA monitor

NA monitor 𝑋 → 𝑌

header update

: Service mesh layer Fig. 3. Blackbox deployment of SafeNom monitor. Each service runs in its own Docker container and the service mesh layer pairs each container with a sidecar container running Envoy proxy. When a request from A is sent to B in step 1, the HTTP header carries the current monitor configuration. Upon arrival at B’s sidecar proxy, the monitor updates the configuration in step 2, and forwards it to the service container in step 3. Table 1. Policies prefixed with “Hotel” are evaluated on the hotel application, and the remainder on the hospital application. Main findings: (1) monitor configuration can be encoded in a few bits of extra header space, and (2) monitoring adds minimal latency, on the order of milliseconds to the application.

Policy 1. EU Data 2. CI/CD 3. Propagate Trace ID 4. Data Encryption 5. Key 6. Session Auth 7. Three levels 8. Hotel Data Encryption 9. Hotel EU Data 10. Hotel Three levels

#nstates

NA #nbits

#ntrans

Max. Nesting #levels

5 10 10 15 17 10 12 15 5 12

3 4 4 4 5 4 4 4 3 4

17 33 21 26 16 10 11 26 17 11

0 1 1 2 2 2 3 2 0 3

Transducer Latency #tbits overhead (ms) 5 6 5 5 5 4 4 5 5 4

1.08 0.86 1.26 0.50 0.329 0.83 0.55 0.800 0.45 0.61

RQ1: Header Space Overhead Carrying the NA’s and transducer’s current configuration is key to our enforcement mechanism. Table 1 presents (for each policy in the Policy column) the total number of NA states (#nstates); number of bits for encoding the maximum number of NA states (#nbits) and transducer states (#tbits); number of NA transitions to non-rejecting state (#ntrans); and the maximum number of headers for the NA store (#levels). All our policies, ranging from no nesting to three levels of nesting, require at most twelve bits of header space for the NA and transducer state. In our experiments, we consider 32-bit parameters. So the number of bits for carrying the NA store is equal to the #𝑙𝑒𝑣𝑒𝑙𝑠 × 32. This is minimal compared to the available space of HTTP headers (on the order of kilobytes). To summarize, the SafeNom monitor compactly encodes its configuration into a few bits of extra header space.

23

4

Overhead (ms)

Overhead (ms)

102

101

3 2 1

100 101

102

Number of Calls

103

0

5

10

15

20

25

Number of Calls

30

35

40

(b) Overhead vs ≤40 Calls

(a) Overhead vs Calls

Fig. 4. Latency overhead vs topology scale, measured as number of API calls.

RQ2: Latency Overhead To measure SafeNom’s impact on the application’s performance, we compare the latency of requests when the application is being monitored versus when it is not on a workload of 200 requests for all user-facing endpoints in our benchmark applications. We average the latency over five such workloads. Our experiment setup involves extracting Envoy filters from each policy’s NA and then measuring latency overhead when the filter is enabled versus disabled. Overhead versus policy. The average latency overhead of monitoring each policy in table 1 is reported in milliseconds in table 1’s “Latency overhead” column. The policies prefixed with “Hotel” were evaluated on the hotel application and others were evaluated on the hospital application. Observe that across both applications, the values are consistently at most ∼ 1.5ms. This is expected since the internal service implementation should not impact the monitoring overhead. To conclude, the SafeNom monitor adds minimal latency overhead on the order of a millisecond.

Overhead / Calls (ms per call)

Overhead versus topology scale. To assess SafeNom monitor’s scalability, we measure the increase in latency overhead with the scale of the application’s topology, which we measure as the number of API calls in an execution trace. To measure this, we synthetically generate applications with execution traces ranging from 3 to 1365 API calls by considering different application topology (or call tree) shapes—all combinations of depths from 2 to 5 and fan-outs from 1 to 4. Fig. 4a shows that the average latency overhead in milliseconds (on the y-axis) linearly increases with the number of calls in the trace (plotted on the x-axis). Both axes in the plot use a logarithmic scale. As per Alibaba’s study [Luo et al. 2021], the common-case execution traces have fewer than 31 API calls. As shown in Fig. 4b, which zooms into the latency overhead plot for traces of length at most 40 API calls, the latency overhead for common case traces is less than 4ms. We also plot the per-hop monitoring overhead (latency Observed 0.40 Average ~ 0.1614 ms/calls overhead divided by number of API calls in the trace) in 0.35 milliseconds on the y-axis of fig. 5 and the number of 0.30 API calls (on log scale) on the x-axis. Each hop incurs 0.25 0.20 an average 0.16 ms overhead. In summary, SafeNom 0.15 monitor is scalable with the common-case latency 0.10 overhead under ∼ 4 ms and a linear increase in the 0.05 0.00 overhead with the length of the trace, adding 0.16ms 10 10 10 Number of Calls of average per-hop overhead. 1

2

Fig. 5. Ratio of overhead to calls.

3

24

9

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

Related Work

A large body of work studies automata whose input symbols are drawn from an infinite or a very large domain. Representative models include register automata, finite-memory automata, fresh-register automata, pebble automata, class-memory automata, history-dependent automata, and nominal automata [Bojańczyk et al. 2006; Bojańczyk et al. 2014; Kaminski and Francez 1994a; Montanari and Pistore 1998; Segoufin 2006; Tzevelekos 2011]. These models differ in how they store names, compare them, or enforce freshness. These models are relevant to SafeNom because our policies must relate names at different positions for equality patterns. However, SafeNom also needs a language model with first-class support for binding, scope, and alpha-renaming notions, rather than only a part of the automata implementation. Below we survey some automata models with register-style implementation and nominal formalism like our model, followed by work on runtime monitoring of microservice applications. Register-based Automaton and languages over infinite alphabet. Register-based automata vary in how they handle the memory and here we describe some of the key details. Finite memory automaton (FMA) [Kaminski and Francez 1994b] and register automaton (RA)[D’Antoni et al. 2019; Kaminski and Francez 1994a] extend a finite-state automaton with a fixed finite set of registers to store and compare data values in a flat word with values, and depending on the model update registers. The maximum number of values that can be simultaneously tracked is statically fixed in the automaton definition. These models can express equality and inequality relationships between values in the flat trace. Some variants can test local freshness, i.e., the current value is not in one of the registers, while others like fresh-register automaton [Tzevelekos 2011] can test a form of global freshness, where the current value must be fresh with respect to the entire run. These models offer a promising automata machinery for data-aware monitoring, but they do not make lexical scope and alpha-renaming a primitive parts of the language semantics. One could extend these models to add an ad-hoc register allocation/deallocation discipline to store and compare values within an active scope. However, then the scope information gets baked into the automata machinery. In contrast, SafeNom makes binders and scope explicit in the policy language. Our automaton still has register-based operational semantics. Nominal Automata. Nominal automata study languages over an infinite alphabet through the lens of symmetry [Ciancia and Montanari 2010; Gabbay and Pitts 2002; Kozen et al. 2015; Schröder et al. 2017]. In the standard nominal setting, the concrete names are not important in themselves; the only aspect that matters is how names are compared, reused, and required to be fresh. Formally, states and transitions are equivariant under permutation of names, so the automaton can be orbitfinite—the automaton has finitely many states up to consistent renaming–despite names ranging over an infinite (or large) set of names. The nominal view is the right starting point for SafeNom as our policies should be invariant under consistent renaming of API values. The policy should not depend on the concrete values carried by API calls and returns, but only on the values’ equality, inequality, freshness, and reuse patterns. However, the general nominal automaton model is too abstract to be directly operationalized into a deployable monitor in the microservice setting. Instead, we build on the register-style nominal automaton model by Kurz et al. [2011, 2012a,b] rather than a fully general nominal automaton. Binder-based nominal automata. The closest technical foundation for SafeNom is the binderbased nominal automaton model of Kurz et al. [2012b]. This work builds on history-dependent automata [Montanari and Pistore 1998]. History-dependent automata already provide a means to allocate names, compare, rename, and forget them; but they recognize flat words. However, in our setting, input words have explicit binders. Many binder-based automata models are designed to

25

characterize the language expressiveness and often allow non-deterministic choice about name generation, matching, and binding [Brunet and Silva 2019; Kaminski and Zeitlin 2010; Kurz et al. 2011]. Our online monitor should deterministically update its state by observing just one symbol at a time; it cannot backtrack its transitions. So we go with the binder-based automata model by Kurz et al., which satisfies our need for determinism. Runtime monitoring of data-aware properties. There is a plethora of runtime verification work for systems with parametric events [Barringer et al. 2012, 2010a,b; Jin et al. 2012], register automata-based (invasive) monitoring of Java programs [Grigore et al. 2013], and more recently stream runtime verification [Gorostiaga and Sánchez 2021]. These systems focus on parametrized monitoring, but SafeNom focuses on policies with primitive support for scope, binding, and freshness. One data-aware monitoring system, BeepBeep [Hallé et al. 2010; Hallé and Villemaire 2012a,b] is close in spirit to SafeNom. It is an LTL-based runtime enforcement mechanism for safety properties over sequences of web service calls and first-order quantification over data. Unlike SafeNom, it does not support properties that require freshness and scoping constructs. Also, BeepBeep compiles to a more complicated Büchi automata-based monitor in comparison to lightweight nominal automata. Monitoring microservice safety properties. Several recent works generalize microservice safety properties [Grewal et al. 2025, 2023; Saxena et al. 2025] beyond pair-wise properties and offer a service mesh based monitoring mechanism. SafeTree [Grewal et al. 2025] shows that API-level monitoring is a practical way to enforce safety properties for blackbox microservice applications. Local monitors deployed outside each service running atop service mesh layer can observe all the API calls/returns into the service and efficiently enforce the properties using a relevant automaton model. SafeNom also uses this service mesh-based deployment for its monitor to meet its monitor’s non-invasive and blackbox deployment requirements. However, SafeTree and related systems abstract away the API parameters and can only enforce properties over an execution’s control-flow, like which API may call which API, which API must happen before another API, or which service call tree shapes are permitted. Such policies are useful, but they are insufficient for the data-aware safety properties described in this paper. SafeNom addresses this orthogonal dimension of data-aware properties. It retains the blackbox API-level view of microservice execution, but enriches the events with logical names that represent parameter values. SafeNom policies can then specify both the order of API events and the scoped equality or inequality relationships among their parameters and responses, and enforce these properties using a nominal automaton. 10

Conclusion

We present SafeNom, a nominal language-based policy language to specify data-aware microservice safety properties. SafeNom policies are enforced in a blackbox manner using a nominal automaton-based runtime monitor that runs efficiently without any invasive changes to the service implementations. SafeNom currently assumes that API calls are sequentially invoked. We see a future possibility of extending SafeNom to an asynchronous setting, where an API call sends data in parallel to other services. References Howard Barringer, Yliès Falcone, Klaus Havelund, Giles Reger, and David Rydeheard. 2012. Quantified Event Automata: Towards Expressive and Efficient Runtime Monitors. In FM 2012: Formal Methods, Dimitra Giannakopoulou and Dominique Méry (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 68–84.

26

Karuna Grewal, P. Brighten Godfrey, and Justin Hsu

Howard Barringer, Alex Groce, Klaus Havelund, and Margaret H. Smith. 2010a. Formal Analysis of Log Files. J. Aerosp. Comput. Inf. Commun. 7, 11 (2010), 365–390. doi:10.2514/1.49356 Howard Barringer, David Rydeheard, and Klaus Havelund. 2010b. Rule Systems for Run-time Monitoring. J. Log. and Comput. 20, 3 (June 2010), 675–706. doi:10.1093/logcom/exn076 Mikołaj Bojańczyk, Mathias Samuelides, Thomas Schwentick, and Luc Segoufin. 2006. Expressive power of pebble automata. In Proceedings of the 33rd International Conference on Automata, Languages and Programming - Volume Part I (Venice, Italy) (ICALP’06). Springer-Verlag, Berlin, Heidelberg, 157–168. doi:10.1007/11786986_15 Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. 2014. Automata theory in nominal sets. Logical Methods in Computer Science Volume 10, Issue 3, Article 4 (Aug 2014). doi:10.2168/LMCS-10(3:4)2014 Paul Brunet and Alexandra Silva. 2019. A Kleene Theorem for Nominal Automata. In 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, Patras, Greece, July 9-12, 2019 (LIPIcs, Vol. 132), Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 107:1–107:13. doi:10.4230/LIPICS.ICALP.2019.107 Vincenzo Ciancia and Ugo Montanari. 2010. Symmetries, local names and dynamic (de)-allocation of names. Inf. Comput. 208, 12 (Dec. 2010), 1349–1367. doi:10.1016/j.ic.2009.10.007 Loris D’Antoni, Tiago Ferreira, Matteo Sammartino, and Alexandra Silva. 2019. Symbolic Register Automata. In Computer Aided Verification - 31st International Conference, CAV 2019, New York City, NY, USA, July 15-18, 2019, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 11561), Isil Dillig and Serdar Tasiran (Eds.). Springer, 3–21. doi:10.1007/978-3-03025540-4_1 Envoy. 2024. Envoy Proxy. https://www.envoyproxy.io/. Accessed: 2024-11-04. Murdoch J. Gabbay and Andrew M. Pitts. 2002. A New Approach to Abstract Syntax with Variable Binding. Form. Asp. Comput. 13, 3–5 (July 2002), 341–363. doi:10.1007/s001650200016 Yu Gan, Yanqi Zhang, Dailun Cheng, Ankitha Shetty, Priyal Rathi, Nayan Katarki, Ariana Bruno, Justin Hu, Brian Ritchken, Brendon Jackson, Kelvin Hu, Meghna Pancholi, Yuan He, Brett Clancy, Chris Colen, Fukang Wen, Catherine Leung, Siyuan Wang, Leon Zaruvinsky, Mateo Espinosa, Rick Lin, Zhongling Liu, Jake Padilla, and Christina Delimitrou. 2019. An Open-Source Benchmark Suite for Microservices and Their Hardware-Software Implications for Cloud & Edge Systems. In Proceedings of the Twenty-Fourth International Conference on Architectural Support for Programming Languages and Operating Systems (Providence, RI, USA) (ASPLOS ’19). Association for Computing Machinery, New York, NY, USA, 3–18. doi:10.1145/3297858.3304013 Felipe Gorostiaga and César Sánchez. 2021. Stream runtime verification of real-time event streams with the Striver language. Int. J. Softw. Tools Technol. Transf. 23, 2 (April 2021), 157–183. doi:10.1007/s10009-021-00605-3 Karuna Grewal, Brighten Godfrey, and Justin Hsu. 2025. SafeTree: Expressive Tree Policies for Microservices. Proc. ACM Program. Lang. 9, OOPSLA2, Article 349 (Oct. 2025), 27 pages. doi:10.1145/3763127 Karuna Grewal, Philip Brighten Godfrey, and Justin Hsu. 2023. Expressive Policies For Microservice Networks. In Proceedings of the 22nd ACM Workshop on Hot Topics in Networks, HotNets 2023, Cambridge, MA, USA, November 28-29, 2023. ACM, 280–286. doi:10.1145/3626111.3628181 Radu Grigore, Dino Distefano, Rasmus Lerchedahl Petersen, and Nikos Tzevelekos. 2013. Runtime Verification Based on Register Automata. In Tools and Algorithms for the Construction and Analysis of Systems, Nir Piterman and Scott A. Smolka (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 260–276. Sylvain Hallé, Tevfik Bultan, Graham Hughes, Muath Alkhalaf, and Roger Villemaire. 2010. Runtime Verification of Web Service Interface Contracts. Computer 43, 3 (2010), 59–66. doi:10.1109/MC.2010.76 Sylvain Hallé and Roger Villemaire. 2012a. Runtime Enforcement of Web Service Message Contracts with Data. IEEE Trans. Serv. Comput. 5, 2 (2012), 192–206. doi:10.1109/TSC.2011.10 Sylvain Hallé and Roger Villemaire. 2012b. Runtime Enforcement of Web Service Message Contracts with Data. IEEE Trans. Serv. Comput. 5, 2 (2012), 192–206. doi:10.1109/TSC.2011.10 Istio. 2024a. Istio. https://istio.io/. Accessed: 2024-11-04. Istio. 2024b. The Istio service mesh. https://istio.io/latest/about/service-mesh/. Accessed: 2024-11-06. Istio. 2026. wasm Plugin. https://istio.io/latest/docs/reference/config/proxy_extensions/wasm-plugin/. Accessed: 2026-01-01. Dongyun Jin, Patrick O’Neil Meredith, Choonghwan Lee, and Grigore Roşu. 2012. JavaMOP: efficient parametric runtime monitoring framework. In Proceedings of the 34th International Conference on Software Engineering (Zurich, Switzerland) (ICSE ’12). IEEE Press, 1427–1430. Michael Kaminski and Nissim Francez. 1994a. Finite-Memory Automata. Theor. Comput. Sci. 134, 2 (1994), 329–363. doi:10.1016/0304-3975(94)90242-9 Michael Kaminski and Nissim Francez. 1994b. Finite-Memory Automata. Theor. Comput. Sci. 134, 2 (1994), 329–363. doi:10.1016/0304-3975(94)90242-9 Michael Kaminski and Daniel Zeitlin. 2010. Finite-Memory Automata with Non-Deterministic Reassignment. Int. J. Found. Comput. Sci. 21, 5 (2010), 741–760. doi:10.1142/S0129054110007532

27 Dexter Kozen, Konstantinos Mamouras, and Alexandra Silva. 2015. Completeness and Incompleteness in Nominal Kleene Algebra. In Relational and Algebraic Methods in Computer Science, Wolfram Kahl, Michael Winter, and José Oliveira (Eds.). Springer International Publishing, Cham, 51–66. Alexander Kurz, Tomoyuki Suzuki, and Emilio Tuosto. 2011. Towards Nominal Formal Languages. CoRR abs/1102.3174 (2011). arXiv:1102.3174 http://arxiv.org/abs/1102.3174 Alexander Kurz, Tomoyuki Suzuki, and Emilio Tuosto. 2012a. A Characterisation of Languages on Infinite Alphabets with Nominal Regular Expressions. In Theoretical Computer Science - 7th IFIP TC 1/WG 2.2 International Conference, TCS 2012, Amsterdam, The Netherlands, September 26-28, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7604), Jos C. M. Baeten, Thomas Ball, and Frank S. de Boer (Eds.). Springer, 193–208. doi:10.1007/978-3-642-33475-7_14 Alexander Kurz, Tomoyuki Suzuki, and Emilio Tuosto. 2012b. On Nominal Regular Languages with Binders. In Foundations of Software Science and Computational Structures - 15th International Conference, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings (Lecture Notes in Computer Science, Vol. 7213), Lars Birkedal (Ed.). Springer, 255–269. doi:10.1007/978-3-642-28729-9_17 Shutian Luo, Huanle Xu, Chengzhi Lu, Kejiang Ye, Guoyao Xu, Liping Zhang, Yu Ding, Jian He, and Chengzhong Xu. 2021. Characterizing Microservice Dependency and Performance: Alibaba Trace Analysis. In ACM Symposium on Cloud Computing (SoCC), Seattle, Washington. Association for Computing Machinery, New York, NY, USA, 412–426. doi:10.1145/3472883.3487003 Ugo Montanari and Marco Pistore. 1998. An Introduction to History Dependent Automata. Electron. Notes Theor. Comput. Sci. 10, C (May 1998), 170–188. doi:10.1016/S1571-0661(05)80696-6 Divyanshu Saxena, William Zhang, Shankara Pailoor, Isil Dillig, and Aditya Akella. 2025. Copper and Wire: Bridging Expressiveness and Performance for Service Mesh Policies. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1 (Rotterdam, Netherlands) (ASPLOS ’25). Association for Computing Machinery, New York, NY, USA, 233–248. doi:10.1145/3669940.3707257 Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. 2017. Nominal Automata with Name Binding. In Foundations of Software Science and Computation Structures, Javier Esparza and Andrzej S. Murawski (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 124–142. Luc Segoufin. 2006. Automata and Logics for Words and Trees over an Infinite Alphabet. In Computer Science Logic, 20th International Workshop, CSL 2006, 15th Annual Conference of the EACSL, Szeged, Hungary, September 25-29, 2006, Proceedings (Lecture Notes in Computer Science, Vol. 4207), Zoltán Ésik (Ed.). Springer, 41–57. doi:10.1007/11874683_3 Ken Thompson. 1968. Programming Techniques: Regular expression search algorithm. Commun. ACM 11, 6 (June 1968), 419–422. doi:10.1145/363347.363387 Nikos Tzevelekos. 2011. Fresh-register automata. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, Thomas Ball and Mooly Sagiv (Eds.). ACM, 295–306. doi:10.1145/1926385.1926420 Margus Veanes, Pieter Hooimeijer, Benjamin Livshits, David Molnar, and Nikolaj Bjorner. 2012. Symbolic finite state transducers: algorithms and applications. SIGPLAN Not. 47, 1 (Jan. 2012), 137–150. doi:10.1145/2103621.2103674