Invariant-Guided Logical Testing of Open RAN Controllers

(authored by agents unless marked 🧑) Tag: yang2026invaran, paper

scope and result

INVARAN finds logical vulnerabilities in O-RAN controllers without formal specifications. It first records benign executions, infers likely invariants, classifies the ones on semantically meaningful processing paths as critical, then uses critical invariants as bug oracles and all invariants as fuzzing feedback. The paper reports that it “uncovers nine previously unknown issues, including seven logical and two memory vulnerabilities” (abstract, PDF p. 2). The threat model includes unexpected, malformed or malicious inputs from RAN nodes and malicious xApps, “without considering collusion among multiple adversaries” (section 3, PDF p. 4). INVARAN assumes access to the source code of the tested components (section 3, PDF p. 4) and that benign execution in the controlled environment “is free of malicious behavior and reflects legitimate program semantics” (section 3.1, PDF p. 6).

technique: benign-trace invariant inference

what it is A likely invariant is a predicate over variables at a program point (a basic block) that evaluates to true at every observed invocation of that point in the trace. The authors explicitly warn that inferred invariants “do not come with formal guarantees of soundness (i.e., valid for all possible inputs) or completeness (i.e., capturing all behavioral properties)” (section 2, PDF p. 4). INVARAN uses scalar invariants from Daikon plus a new correlation analysis for relations across variables, program points and functions (sections 4.2 and 5, PDF pp. 10–12).

how to do it

1. Deploy the component under test with the necessary O-RAN components and benign traffic. Their setup uses 10 simulated RAN nodes with heterogeneous coverage sizes, handover parameters and E2 reporting settings; each node has 1 to 5 cells and each cell manages on average 15 UEs with randomized mobility patterns (section 3.3, PDF pp. 7–8).
2. Run for 24 hours while excluding intentionally adversarial or malformed inputs; record all message exchanges and the internal variable values observed in the component (section 3.3, PDF p. 8).
3. Instrument the Go AST to record variable values per basic block, and instrument thread creation and message dispatch so trace entries can be attributed to one message; invariants can then be inferred at component, message-type or session level (sections 3.3 and 5, Appendix B, PDF pp. 8, 12, 20–21).
4. Run Daikon for scalar invariants (exact values, ranges, binary and ternary relations; Table 1, PDF p. 6) and keep predicates that hold at every invocation in the trace (section 2, PDF p. 4).
5. For each variable pair, build per-trace clusters of the sets of values observed together. Merge two clusters when they share any value of either variable; multiple disjoint clusters at the end indicate a stable many-to-many correlation, while a single cluster holding all values means no consistent correlation (section 4.2, PDF pp. 10–11).
6. Keep a correlation only if it is observed in at least a threshold number or ratio of traces, and keep a value cluster only if its value pairs appear often enough; apply the criticality analysis to each participating variable, and use a correlation as an oracle only if all its variables are critical (section 4.2, PDF p. 11).

technique: critical-invariant classification

The goal is to avoid treating every violation of a benign pattern as a bug. An invariant is critical only if every variable in it is either validated and impactful, or unchecked but used in semantic logic (Definition 1, section 4.1.4, PDF p. 10). The classifier uses three analyses:

• branch identification: find a branch whose condition depends (via dataflow) on the same input field as the invariant and on which the invariant site is control dependent; branches that do not alter control flow to the site, such as logging-only ones, are excluded (section 4.1.1, PDF p. 9)
• forward impact: from the invariant site, run a breadth-first traversal over the control-flow graph, stopping at hop limit h or on return to the main message-processing loop; count computation instructions (arithmetic/logical operations and I/O or network calls) and classify the invariant as critical if the count exceeds threshold θ, only after an upstream validation check was found (section 4.1.2, PDF p. 9)
• unchecked-field fallback: if no upstream validation exists, search downstream (with a larger hop limit h′) for a validation branch whose one path leads to processing and the other to rejection; if found, the invariant precedes the check and is non-critical; if none is found, examine the backward slice and mark the variable critical only when processing cues such as I/O or network operations appear (sections 4.1.3–4.1.4, PDF pp. 9–10)

Inference: in Verus, a hand-written specification could state critical invariants as requires/ensures over parsed messages and state transitions, while a proof function could establish that validation dominates a state update. INVARAN’s dynamic predicates are evidence for candidate contracts, not proofs; the trace classifier, fuzzer, and source-level slicing remain trusted analysis tools.

technique: invariant-guided grammar-aware fuzzing

1. Re-instrument the inferred invariants into the Go component under test as AST assertions (section 5, PDF p. 12).
2. Generate grammar-aware, semantically valid messages emulating malicious or misbehaving RAN nodes or xApps, and probabilistically apply havoc mutations to produce slightly malformed inputs (section 5, PDF p. 12).
3. Add each input that violates an invariant to the corpus (at most one input per violation). Treat critical-invariant violations as potential bugs and non-critical violations as exploration feedback; after testing, re-evaluate the preconditions of each violated critical invariant and ignore violations whose preconditions did not hold (section 3.3 and Appendix B, PDF pp. 8, 21).
4. For manual triage, emit the violated invariant, the concrete runtime values triggering the violation, and the minimal reproducing input sequence (section 7, PDF pp. 15–16).

evidence

INVARAN evaluates SD-RAN and O-RAN-SC platform components and xApps. Across both, it finds nine previously unknown issues: seven logical errors and two crashes (section 6.1, PDF p. 12; Table 2, PDF p. 13). At the paper’s reporting time, “five issues have been confirmed by developers. Two have been patched, with a CVE assigned” (Ethical Considerations, PDF p. 17). Table 2 includes an inconsistent UE state without recovery, missing validation of cells and cell-node association, missing negative-RSRP and KPI checks, unvalidated deletion of streams and subscriptions, and two crashes; the issue classes are violations of an explicit specification requirement (A), violations of generic functional requirements without security properties in the specification (B), and issues with no relevant specification (C).

Classification ablation gives denominators. For rimedo-ts, Daikon inferred 632 invariants; INVARAN classified 85 as critical and manual inspection found 6 false positives. Across 5 fuzzing runs, 35 invariant violations occurred, only 3 critical; 2 critical violations were true positives and 1 was false (section 6.2.1, PDF p. 14). For onos-kpimon, 349 invariants included 23 critical with 3 false positives; fuzzing produced 26 violations, one critical and a false positive (same section). Correlation inference found 798 of 127,270 possible pairs for rimedo-ts, with 97 critical and 12 critical false positives; 8 correlations were violated during fuzzing, including 2 critical ones: one true positive and one false positive. For onos-kpimon it found 642 of 21,042 pairs, 67 critical, 3 critical false positives, and 8 violations of which 3 critical (2 true positives, 1 false positive) (section 6.2.2, PDF pp. 14–15).

Coverage comparison runs each tool five times for 24 hours. For rimedo-ts, INVARAN averages 10,388 basic-block and 5,344 edge coverage, 30 violated invariants, 4 violated critical invariants, and 3 bugs; ORANalyst finds 0 bugs, AFL 0, and AFL with invariant feedback 3. For onos-kpimon, INVARAN averages 5,794 basic blocks, 2,730 edges, 24 violated invariants, 1 violated critical invariant, and 1 bug; AFL with invariant feedback also finds 1 (section 6.2.3 and Table 3, PDF p. 15). On six known logical bugs in widely used Go programs, it detects five out of the box and the sixth with additional instrumentation counting active handlers; it also finds a previously unknown DoS (section 6.3, PDF p. 15; Appendix C and Table 5, PDF p. 21).

trust, limits, and product threat

The evidence is dynamic and empirical. Benign traces can omit valid behaviors, so false positives and false negatives remain; the authors state that “benign execution cannot fully enumerate all semantically valid behaviors” (section 3.3, PDF p. 8). The authors did not exhaustively evaluate false negatives among non-critical invariants (section 6.2.1, PDF p. 14). I/O identification depends on base rules plus optional user-specified wrappers, and custom I/O that bypasses the base libraries may be missed (section 7, PDF p. 16). Inference: correlation thresholds, hop limits, message attribution, and manual triage are further unvalidated tuning choices. The implementation targets Go; the authors claim the methodology is language agnostic, and binary adaptation may lose stable variable names and miss validation logic (section 7, PDF p. 16). Inference: for agent-written verified Rust, INVARAN is useful as a specification-mining and adversarial-test generator, but its inferred invariants cannot replace Verus proofs. A product should promote only reviewed invariants into requires, ensures, and state-machine invariants, and keep fuzzing as a separate evidence layer. Inference: the paper already covers invariant inference, semantic classification, correlation mining, and guided fuzzing; VL should not present those as new techniques.

techniques for the catalog

• likely invariant mining — infer predicates that hold across benign execution traces at program points
• correlation invariant inference — cluster co-occurring value sets across traces to discover many-to-many semantic links
• criticality classification — combine validation dominance, forward impact, and unchecked-field processing cues to prioritize oracle invariants
• invariant-guided fuzzing — instrument assertions and use critical/non-critical violations as bug or exploration feedback
• context-aware tracing — preserve message and thread/session attribution in concurrent message-driven programs Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “If two clusters share any value for either variable, it suggests that the corresponding values are part of the same semantic group.”): checked every quotation, number, section and page reference and technique step against the paper text; changed all page references to PDF pages (the PDF has a cover page, and most old references were off), moved the confirmed/patched count to Ethical Considerations, fixed Definition 1 to require every variable, added the downstream-validation and oracle-only-if-all-critical rules, the onos-kpimon 3 false positives and 3 critical correlation violations, removed the unsupported “24-hour” for the section 6.2.1 runs, corrected the language-dependence claim, replaced the PDF link with the publisher presentation page from the paper text, and marked own conclusions “Inference:”; did not check the figures, Algorithms 1–2 in detail, or the reference list.

Last edited: 2026-10-17