Searcharxiv⌕ Search

arXiv · 2609.33081

SafePar: Monitoring Asynchrony in Microservices

Abstract

Modern cloud applications are built from loosely-coupled microservices that coordinate through well-defined APIs to service user requests. A single API request often triggers multiple downstream API calls, some executed sequentially and others spawned asynchronously in parallel. To certify safe and secure inter-service interactions in such applications, security and compliance teams must enforce policies not only over nested call/return structure, but also over the parallel structure of an execution: which calls may run concurrently, how many parallel branches can be spawned, and what combination of branch outcomes are allowed. However, existing runtime enforcement mechanisms typically model executions as sequential or purely nested traces, and cannot capture the parallel structure introduced by asynchronous API calls. Furthermore, since application implementations may not be accessible to security and compliance teams, the policy enforcement mechanism should be decoupled from the service implementation. We introduce SafePar, a specification and monitoring framework for policies over concurrent microservice executions. A SafePar policy constrains both the order of API calls and their series-parallel structure. To support seamless deployments, each policy is compiled into a series-parallel visibly pushdown automaton, a new model of computation we propose in this work, that drives a distributed runtime monitor implemented on top of the servicemesh layer. Our technique is blackbox and non-invasive: it requires no access or changes to the service implementation. Our experiments show that SafePar enforces rich concurrency-aware policies while incurring only millisecond-scale latency overhead.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Karuna Grewal, P. Brighten Godfrey, Justin Hsu, Umang Mathur. 2026-09-27. SafePar: Monitoring Asynchrony in Microservices. https://arxiv.org/abs/2609.33081

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

Faultless: A Program Equivalence Technique for Validating and Evaluating Neural Decompilers

Neural decompilers are machine learning models which perform the process of decompilation, lifting code from a lower-level language to a higher one. Neural decompilers offer substantial utility relative to traditional deterministic decompilers because they can probabilistically recover information discarded during lowering, like variable names, types, and control flow structuring. However, they can also make mistakes, producing code that is not equivalent to the original, making it difficult to trust their output. In this work, we introduce Faultless, a program equivalence technique for performing translation validation on neural decompilers. Faultless compares code produced by a deterministic decompiler, which has stronger correctness properties, with that of a neural decompiler. Faultless is also useful for model evaluation, a highly related task, in which the neural decompilers' prediction is compared with a reference solution. Neural decompilation introduces significant challenges to the task of program equivalence which existing techniques are not equipped to handle, including limited extrafunctional context and systematic semantic inconsistencies in decompiled code. Faultless takes a static symbolic execution-based approach with an execution model and memory model designed to handle these challenges.

cs.PL↗

Episodic Loops: Finitary Event Structures and Operational Semantics for C11 Programs with Retries

Lock-free synchronisation algorithms are often implemented with fallible operations, such as compare-and-swap (CAS), wrapped in unbounded retry loops. Verifying such algorithms requires considering arbitrarily many failing iterations, yielding large state spaces, compounded by the interleavings of concurrent threads. Prior work discarded failing iterations, arguing that they leave no trace in the post-loop state. Compilers and hardware reorder instructions, and load-store reorderings may cross the boundaries of failing iterations, introducing subtle concurrency bugs. We demonstrate one such bug, making use-after-free possible in a previously verified variant of Read-Copy-Update - a synchronisation primitive widely adopted in the Linux Kernel - and we provide and verify a fix. We find that practical retries in lock-free algorithms adhere to a common pattern. We introduce episodic loops, a semantic characterisation of unbounded retry loops which is syntactically recognisable in many practical cases, and synchronisation points, operations that bound both instruction reordering and state space within episodic loops. We show that SMRD - a symbolic event structure semantics for C11 programs which allows for load-store reordering - admits a finite representation in programs where unbounded loops are episodic. We further introduce a finitary operational semantics that allows safety properties to be verified in finitely many steps. For the use-after-free bug we demonstrate, verification takes a single pass over the program, linear in the program size. We provide a reference implementation of SMRD reproducing the bug and verifying the fix, and mechanise the operational semantics together with the minimal bug and its fix in Isabelle/HOL.

cs.PL↗

Irene: Equivalence Checking of Hybrid Quantum Programs via Structure-Preserving Symbolic Reduction

Equivalence checking is essential for validating compiler transformations of hybrid quantum programs, which combine quantum operations, measurements, and classical control. Measurement-dependent control limits unitary reasoning, while dependencies between classical outcomes and quantum operations can enlarge intermediate symbolic states. We present Irene, an equivalence-checking framework for bounded hybrid quantum programs based on structure-preserving symbolic reduction. The framework progressively simplifies equivalence obligations through three levels of reasoning. At the gate level, algebraic identities simplify unitary regions. At the hybrid path-sum (HPS) level, reduced symbolic execution states are represented as typed graphs, whose isomorphism certifies equivalence. Remaining obligations are handled by density kernels that characterize transformations of input density operators into observable outputs, allowing comparison even when internal measurement histories differ. Residual coefficient differences are encoded as SMT queries. A common set of symbolic reductions supports HPS and density-kernel reasoning by preserving factored Boolean and arithmetic expressions, eliminating reducible dependencies before expanding residual sums. We evaluate Irene against five equivalence checkers on 1,982 program pairs from seven benchmark suites. Irene solves 1,584 pairs (79.92%), compared with 57.52% for MQT QCEC, the baseline with the highest aggregate coverage, with a mean end-to-end time of 3.93 seconds per solved pair. Applied as an equivalence-checking oracle, Irene also identifies 15 previously unknown bugs in quantum compilers, including Qiskit, Cirq, and PennyLane.

cs.PL↗