PaperlayerView exact revision on arXiv

Source-linked AI summary

SafeNom: Data-Aware Microservice Policies

Karuna Grewal, P. Brighten Godfrey, Justin Hsu

arXiv:2609.30394v1cs.PLcs.NI

TL;DR

Microservice monitoring tools have limited ability to express how data values flow across API calls, although such properties matter for application-wide safety. SafeNom specifies these value relationships alongside API-call order and enforces policies with a blackbox runtime monitor. The reported overhead is under ∼4 ms for common-case traces, with 0.16 ms average per hop.

  • Problem

    Existing microservice safety monitors have limited expressiveness for properties describing how data flows through API calls.

    Source: §1 · p. 1

  • Method

    SafeNom uses nominal languages and scoped binders to specify data-aware policies, enforced by a nominal-automaton runtime monitor.

    Source: Our approach · p. 3

  • Results

    Common-case latency overhead is under ∼4 ms, with 0.16 ms average per hop.

    Source: RQ2: Latency Overhead · p. 23

  • Takeaways & Limitations

    SafeNom currently assumes sequential API invocation; extending it to asynchronous calls is a future possibility.

    Source: §10 · p. 25

    Online monitoring requires the binder-free regular-expression skeleton of a policy to be one-unambiguous.

    Source: §7 · p. 21

Abstract

from arXiv · show

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

Microservice executions can be unsafe when data flows incorrectly across API calls, even if individual services behave correctly. SafeNom addresses the lack of data-aware monitoring by specifying value relationships alongside call order in a blackbox setting.

1 Introduction

  • A locally correct service sequence can still be unsafe when a later service receives or stores the wrong data, risking leaks, audit failures, penalties, and lost trust.For example, storing raw data instead of an encryption result can violate a storage policy.Source: §1 · p. 1
  • Existing tools and monitors can constrain API communication or multi-hop call structure, but do not enforce policies relating values across an execution.Service mesh [Istio 2024b] policies are single-hop; Grewal et al. [2023] and SafeTree address multi-hop structure but not data values.Source: §1 · p. 2
  • Examples include requiring encrypted rather than raw data in storage, consistent keys within co-signature sessions, and a shared trace ID across an execution.These policies depend on equality or inequality patterns among API data, not only call order.Source: §1 · p. 2
  • The target setting requires blackbox, non-invasive enforcement because certifying teams may lack service implementation access and global code changes can be impractical.Inter-service communication is a boundary for specifying and enforcing behavior without inspecting service code.Source: §1 · pp. 1–2
  • Policies should be invariant under consistent renaming of concrete values, accepting or rejecting traces according to their equality and inequality patterns.The policy must not enumerate a fixed finite alphabet of possible runtime values.Source: §1 · p. 2
  • Data-dependency constraints need explicit scopes, since some values remain relevant across an execution while others apply only within a session, phase, or child call.A monitor must also track only currently scoped values needed for later comparisons, then discard them to fit metadata into limited HTTP headers.Source: §1 · p. 3

Our approach

SafeNom combines nominal-language semantics with scoped data dependencies to specify microservice policies, then compiles them for distributed runtime monitoring. Its approach includes a service-mesh monitor and case studies of policy expressiveness.

Our approach

  • Nominal words and languages make invariance under value renaming intrinsic by treating API events and data values as symbols and names.Replacing a name freely preserves membership, matching policies that depend on equality patterns rather than concrete values.Source: Our approach · p. 3
  • SafeNom extends nominal regular expressions with lazy binders and inequality semantics to express scoped data dependencies when a value appears after its scope begins.Lazy binders open a name's scope before assigning a value, initializing it at first observation for later comparisons.Source: Our approach · p. 3
  • SafeNom policies are compiled to nominal automata and simulated by a distributed runtime monitor over HTTP messages without service-code access or invasive changes.The monitor tracks only names currently in scope, keeping monitoring metadata within the HTTP header budget.Source: Our approach · p. 4
  • The paper contributes extensions for lazy binding, SafeNom policy syntax and semantics, expressiveness case studies, and sound compilation to nominal automata.It also reports a service-mesh implementation and performance evaluation.Source: Our approach · p. 4

2 A Tour of SafeNom Policies

SafeNom illustrates policies that constrain both API-event order and data equality or inequality across calls and responses. It represents value relationships with scoped binders and enforces them using a nominal-automaton monitor.

2 A Tour of SafeNom Policies

  • The MFA example demonstrates that SafeNom policies govern both API-call order and how request and response values flow between calls.The policy requires each MFA response to return its call’s challenge code and forbids reusing the enclosing login password.Source: §2 · p. 4, §2.1 · p. 4

2.1 Example: login with multi-factor authentication

  • The MFA policy requires two calls whose responses echo their respective challenge codes, with each code distinct from the login password but not necessarily from the other code.The examples accept equal challenge codes and reject a mismatched response or a challenge code reused from the password.Source: §2.1 · pp. 4–5

2.2 Traces as words with binders

  • Nominal binders annotate traces with logical names and scopes, distinguishing value relationships that a flat trace of concrete values cannot capture.Names identify the login password and each challenge code; nested scopes express inequality while disjoint challenge scopes need not require distinct values.Source: §2.2 · p. 6

2.3 SafeNom policy enforcement

  • A nominal-automaton monitor checks bound values for equality or freshness, then forgets them when their binder scopes end.The monitor converts raw API traces into nominal words before checking whether the automaton accepts the policy.Source: §2.3 · pp. 6–7

3 Nominal Languages for Data-Aware Properties

SafeNom interprets microservice traces as nominal words so policies can express relationships among values independently of their concrete identities. Its lazy-binding extension allows a value’s scope to begin before that value appears in an API event.

3.1 Refresher: Nominal Languages with Binders

  • Nominal words combine API-event symbols, data names, and binders to record event order, value positions, and the scopes governing value relationships.A binder marks a name’s scope, within which occurrences are treated as the same logical value.Source: §3.1 · pp. 7–8
  • Policies over nominal words are invariant under consistent renaming of bound names, allowing them to depend on equality patterns rather than concrete values.The paper calls consistent renaming of bound names α-renaming; capture of a free name would change the equality structure.Source: §3.1 · p. 8
  • Nominal regular expressions describe valid nominal words using empty and event or name expressions, union, concatenation, repetition, and binders.A binder expression matches words in its scope as well as their α-renamings.Source: §3.1 · p. 8

3.2 Our Lazy Binding Extension

  • Lazy binders address traces where a data-dependency scope begins before the relevant API parameter is visible, unlike eager binders that require the value at scope entry.In an API trace, parameters become visible only after the operation or API identifier.Source: §3.1 · p. 9, §3.2 · p. 9
  • The extension adds partial names as logical identifiers for parameter values and uses them in binders that can bind the value when first observed.The mapping η associates a partial name with an actual value; a binder substitutes for free occurrences while avoiding capture.Source: §3.2 · pp. 9–10
  • The extended grammar permits free partial names for defining lazy-expression semantics, although real execution-trace representations have none.The paper’s accepted nominal words are closed: each name has a corresponding bound partial name.Source: §3.2 · pp. 9–10

4 SafeNom: Nominal Language-based Policy Language

SafeNom instantiates nominal-language constructs for policies over API events and data values. Its semantics enforce scoped equality and inequality constraints while making policy acceptance invariant to valid renaming of concrete values.

4 SafeNom: Nominal Language-based Policy Language

  • SafeNom names pair a logical register with a concrete API parameter or output value, while call and return symbols identify HTTP requests and responses.Partial names omit the concrete value until it is observed.Source: §4 · p. 10

4.1 SafeNom Semantics

  • SafeNom accepts nominal words only when they satisfy well-formedness constraints, capturing inequality between nested bound names.Each bound partial name has a unique associated value, and nested names along a binder path must have distinct values.Source: §4 · p. 10, §4.1 · p. 11

4.2 Alpha-renaming in SafeNom

  • A policy can bind a value at one API call and require equality with a later call, such as matching the first parameters of APIs A and B.Renaming the values preserves the policy's acceptance when the equality pattern is preserved.Source: §4.2 · p. 11
  • Well-formed words are α-equivalent when a valid permutation maps one to the other; this relation is reflexive, symmetric, and transitive.The paper establishes a bijection between valid permutations for a word and its permuted counterpart.Source: §4.2 · p. 12
  • SafeNom policies are closed under α-equivalence, so acceptance depends on equality and inequality relations rather than specific parameter values.The valid permutations used for α-renaming are restricted by binder paths and depend on the word being renamed.Source: §4.2 · pp. 12–13

5 Case Studies

The case studies demonstrate SafeNom policies for fixed values and runtime equality or inequality, with binders and repetition expressing constraints at local or execution-wide scopes.

Static data/configuration

  • SafeNom can prohibit database writes to the US region after a user call identifies the EU region, and reject writes lacking the required region value.The policy allows other API calls without restriction while requiring each DB call to carry EU.Source: §5 · p. 13

Equality check

  • A build-pipeline policy can require exactly one Container call with the same identifier as the Build session.The policy rejects repeated Container calls or a call carrying a mismatched identifier.Source: §5 · pp. 13–14

Inequality check

  • A secure-handshake policy requires KeyGen's public and private keys to be distinct and forwarded to Client and Server, respectively.The trace using the same key for both outputs is rejected.Source: §5 · pp. 14–15

Repeated (local) equality check

  • Kleene-star repetition lets a binder enforce equality within each operation retry while allowing a different value in another iteration.The authenticator example checks that each PIN returned by Generate matches the PIN sampled by Pin within that iteration.Source: §5 · p. 15

Repeated (global) equality check

  • A single binder under Kleene star can require an unchanged request ID across an execution's downstream API calls.The illustrated policy rejects a child call with a missing request ID or a value different from the global identifier.Source: §5 · pp. 15–16

6 Enforcement: Lazy Nominal Automaton

SafeNom extends nominal automata with lazy binding and inequality checks, using a store and forbidden sets to enforce name scope and freshness. The policy compiler produces an automaton whose accepted language matches the SafeNom policy.

6 Enforcement: Lazy Nominal Automaton

  • Lazy nominal automata extend nominal automata to support partial names, lazy binding, and inequality checks.Their states are stratified by binder depth, and transitions push or drop levels as binder scopes open or close.Source: §6 · p. 16
  • An automaton configuration pairs a state with a store of in-scope names and forbidden sets used for freshness checks.The store is indexed by binder depth; for SafeNom names, freshness requires unequal concrete values.Source: §6 · p. 17
  • When a binder closes, its register is erased and its name is added to remaining partial-name registers' forbidden sets to preserve freshness after the scope ends.This prevents an outer binder from later reusing a value that was bound in an ended inner scope.Source: §6 · p. 18

Our SafeNom policy to NA compiler

  • The Thompson-style policy compilation is followed by a layer-wise powerset construction to produce a deterministic nominal automaton.The construction relabels references to bound partial names with their binder register levels.Source: §6 · p. 19
  • The compiled automaton accepts exactly the words matched by the SafeNom policy.The paper states that the compilation is sound: SNom⟦ne⟧ = L(Hne).Source: §6 · p. 19

7 Implementation

SafeNom runs co-located monitors at service proxies and separates parsing API events into nominal words from automaton-based policy checking. Online monitoring requires a one-unambiguous binder-free policy skeleton so the transducer can parse deterministically.

7 Implementation

  • The prototype compiles each policy to a nominal automaton and runs distributed monitors alongside services atop the Istio mesh without modifying service implementations.Each service has a co-located monitor, and the prototype contains about 3,000 lines of Java.Source: §7 · p. 19

From HTTP events to nominal words

  • A symbolic finite-state transducer reconstructs nominal words from flat API events and extracts relevant values, while the nominal automaton performs equality, freshness, and scope checks.The design separates parsing from semantic policy enforcement.Source: §7 · p. 20

Monitor configuration

  • The monitor carries transducer state, automaton state, and the automaton store in HTTP headers that are updated as messages are processed.Services must propagate these headers between parent and child requests or responses for distributed monitoring.Source: §7 · p. 20

Deterministic transducer

  • The binder-free regular-expression skeleton must be one-unambiguous for online monitoring, allowing the transducer to choose deterministically where each event came from.This requirement makes the monitor frontend deterministic by construction while leaving nominal-automaton semantics unchanged.Source: §7 · p. 21

8 Evaluation

SafeNom is evaluated on hospital and hotel microservice applications, with monitoring configuration carried in request headers. The evaluation examines configuration space and latency overhead across policies and execution topologies.

8 Evaluation

  • The evaluation asks how much header space configuration requires and how much latency overhead monitoring adds.The blackbox deployment diagram shows the current monitor configuration traveling in HTTP headers to the receiving service’s sidecar proxy for an update.Source: §8 · p. 21, Figure 3 · p. 22
  • The hospital and hotel applications average 6 and 4.5 service-tree nodes, respectively, in the Istio-enabled Kubernetes evaluation.The policy suite covers the language’s main constructs.Source: §8 · p. 21

RQ1: Header Space Overhead

  • NA and transducer states require at most 12 bits, while each NA-store level uses 32 bits in the experiments.The paper describes this configuration as a few bits of extra header space relative to HTTP headers’ kilobyte-scale capacity.Source: RQ1: Header Space Overhead · p. 22, Table 1 · p. 22

RQ2: Latency Overhead

  • Figure 4 measures latency overhead against topology scale, with scale measured as the number of API calls.Source: Figure 4 · p. 23

RQ2: Latency Overhead

SafeNom adds millisecond-scale monitoring latency, with overhead increasing linearly as traces grow. Common-case traces remain below 4 ms, and average per-hop overhead is 0.16 ms.

Overhead versus policy

  • Across both applications, policy-specific average latency overhead is consistently at most approximately 1.5 ms.The measurement compares monitored and unmonitored requests over five workloads of 200 requests per user-facing endpoint.Source: RQ2: Latency Overhead · p. 23

Overhead versus topology scale

  • 0.16 ms is the average per-hop monitoring overhead; common-case traces incur less than 4 ms, with overhead increasing linearly with call count.Common-case traces are described as having fewer than 31 API calls.Source: RQ2: Latency Overhead · p. 23
  • Figure 5 plots per-hop monitoring overhead in milliseconds against the number of API calls on a logarithmic x-axis.Source: Figure 5 · p. 23, RQ2: Latency Overhead · p. 23

9 Related Work

SafeNom extends microservice monitoring beyond API control-flow to data relationships among call parameters and responses. Its nominal-language approach makes scoping and freshness explicit while supporting deterministic online monitoring.

Register-based automata

  • Unlike register automata that track a fixed number of values in flat traces, SafeNom makes binders and scope explicit in its policy language.Its automaton retains register-based operational semantics.Source: §9 · p. 24

Nominal automata

  • Nominal automata treat consistent renamings as equivalent, matching policies that depend on equality, inequality, freshness, and reuse rather than concrete values.SafeNom builds on register-style nominal automata because the general nominal model is too abstract to operationalize directly as a monitor.Source: §9 · p. 24

Binder-based nominal automata

  • SafeNom uses Kurz et al.’s binder-based automaton model for deterministic online updates, while the related history-dependent model recognizes flat words.The online monitor observes one symbol at a time and cannot backtrack.Source: §9 · pp. 24–25

Runtime monitoring of data-aware properties

  • BeepBeep supports first-order data quantification over web-service-call sequences, but not freshness or scoping constructs; it compiles to Büchi automata.SafeNom’s nominal automata are described as lighter weight by comparison.Source: §9 · p. 25

Monitoring microservice safety properties

  • SafeNom enriches control-flow monitoring with logical names for API values, enabling policies over event order and scoped equality or inequality among parameters and responses.These properties are enforced using a nominal automaton.Source: §9 · p. 25

10 Conclusion

SafeNom specifies data-aware microservice safety policies in a nominal language and enforces them with a blackbox, non-invasive nominal-automaton monitor. The current design assumes sequential API calls; asynchronous parallel calls are a possible future extension.

10 Conclusion

  • SafeNom is a nominal-language policy language for specifying data-aware microservice safety properties.Source: §10 · p. 25
  • A nominal-automaton runtime monitor enforces these policies without service-implementation access or invasive code changes.Source: §10 · p. 25
  • The current design assumes sequential API calls, with asynchronous parallel data sends identified as a possible extension.Source: §10 · p. 25
Loading 2609.30394v1…