Composition
YAML and code share the path
YAML route+app branch→request path
YAML decides which service a proxy calls; the application decides what happens after the request arrives.
See how we compose it →Interactive artifact
Intent-Based Verification of Service Mesh ConfigurationDOI
When YAML and code disagree, Z3 finds the request.
Service-mesh routes are written in YAML; application behavior lives in code. Bugs hide where the two meet. This artifact compiles both layers and your intent into one model, asks Z3 whether the intent holds, and shows the request that breaks it.
Istio YAMLroutes
App summariesoperator models
Intentassertions
SMT modelZ3
Verdictcounterexample
Guided walkthrough
Three failures, one model
Full explorer
Explore all cases
Open any case to inspect the complete YAML, generated routing DSL, app models, and solver output.
How to read verdicts and queries
holds
#assert holds for every modeled request.violatedZ3 found a counterexample.
reachable
#exist found a witness.unreachable
#exist is unsat; no witness exists.#assertUniversal property over modeled requests.#existReachability / witness query.NSelectNondeterministic choice for unknown or unspecified behavior (weighted traffic split, app internal state, Istio unspecified behavior).Results are precomputed at build time; Compile and Check reveal saved output.
Istio config
Routing DSL Generated
User intent Assertions
Each numbered item is a property checked by Z3; the formal assertions follow.
With over-approximating app summaries, #exist may pass with an unrealizable witness (false positive), and #assert may fail with an unrealizable counterexample (false alarm).
reqSimple is one fixed empty request: modeled headers are absent (nostr) and modeled HTTP fields are empty strings. It is not an arbitrary request. #exist with reqSimple checks whether a model choice can satisfy the query for that request; forall (req : Req) ranges over all modeled requests.
Verdicts
Counterexamples
Raw Z3 witnesses
Raw Z3 output
Compiler output
Concepts
From service mesh to proof
A short primer from mesh YAML to a solver query.
control planepushes YAML to every sidecar
YAML route tableClick a route to send it
data plane · request path
sidecarservicerequest path
Step 1
What is a service mesh?
Every service gets a sidecar proxy. Service-to-service traffic goes through sidecars, not directly.
The control plane pushes YAML routing rules to every sidecar; the sidecar decides the next hop. The application only handles the request.
Routing, canaries, and access control live in YAML outside the app. A YAML mistake changes the path without touching application code.
See the full model in the walkthrough →Step 2
Why is verification hard?
Three things make the mesh hard to reason about: configuration and code compose, apps branch at runtime, and some behavior is deliberately unspecified.
App behavior
The next hop is decided at runtime
request→if /login→NSelect
The call graph is not fixed: an application can branch on request data or on state it keeps elsewhere.
See how we summarize apps →Unspecified behavior
Istio leaves some behavior unspecified
gw[x] → VS1, VS2 → server[a]
gw[x] → VS2, VS1 → server[b]
When several VirtualServices bind the same host, Istio does not guarantee their merge order.
See the merge-order case →Istio YAMLroutes
App summariesread, write, call
Intentassertions
↓compose
one programproxies + app summaries
SMT / Z3ask the intent
holds
for every modeled request
violated
Z3 found this request
- source
- @attacker
- uri
- /payouts
- observed
- internal = granted
Intent
Step 3
What do we do?
YAML becomes a proxy program. App summaries become functions. Intent becomes a query. Z3 either proves it for every request or returns one request that breaks it.
No sampling, no test suite: the solver reasons about every modeled request.
See the full pipeline in the walkthrough →Application logic
uri != "/login"→frontendelse if session in DB→redirect-serviceelse→login-serviceIntentNon-/login requests always reach frontend.
Summarymore precise → less effort
holdsnon-/login requests reach frontend
false alarmWitness: a non-/login request
uri=/home can be sent to login-service.Step 4
How much app detail?
Exact needs DB state. Mixed keeps the URI guard and turns only the DB choice into NSelect; coarse also drops the URI guard, so it can create false alarms.
Try the login walkthrough → Open the full login case →Step 5
Handling unspecified behavior
Istio deliberately leaves some behavior unspecified. The paper's main example is VirtualService merge order: when multiple VirtualServices bind the same gateway host, their match order depends on the order in which the VirtualServices start and is not formally specified.
Merge order
order-sensitivethe two allowed orders reach different servers
Merge order: the paper's concrete example
Two allowed orders reach different servers. The verifier considers every allowed order, so one counterexample is enough to make an assertion fail.
Open the merge-order example →The walkthrough and examples turn these ideas into executable models.