SCARA: A S EMANTICS -C ONSTRAINED AUTONOMOUS R EMEDIATION AGENT FOR O PAQUE I NDUSTRIAL S OFTWARE V ULNERABILITIES
arXiv:2605.19668v1 [cs.CR] 19 May 2026
A P REPRINT Bowei Ning* 1,3 , Xuejun Zong†2,3 , Lian Lian‡2,3 , Kan He§2,3 , Guogang Wang2,3 , Yifei Sun¶2,3 , and Jinyang Liu||1,3 1 Shenyang University of Technology, Shenyang 110870, Liaoning, China 2 Shenyang University of Chemical Technology, Shenyang 110142, Liaoning, China 3 Key Laboratory of Information Security for Petrochemical Industry in Liaoning Province, Shenyang 110142, China
May 20, 2026
A BSTRACT Critical-infrastructure operators are increasingly expected, under policy and standardization regimes such as Executive Order 14028 and IEC 62443, to assess and remediate vulnerabilities in deployed software. However, a substantial fraction of deployed industrial software is delivered as opaque industrial software (OIS): stripped firmware, proprietary protocol handlers, and compiled control logic for which source code, debug symbols, build environments, and hardware interfaces are unavailable to defenders. Although binary analysis can flag vulnerability candidates in such artifacts, existing automated vulnerability repair systems overwhelmingly assume source code, a compilable artifact, sanitizer feedback, or an instrumentable build. These assumptions do not hold for opaque industrial binaries, leaving a gap between binary-level vulnerability discovery and validated remediation. This paper presents SCARA, a Semantics-Constrained Autonomous Remediation Agent for OIS. SCARA operates under a source-unavailable defender model in which upstream binary detectors or analysts provide vulnerability candidates. Its four-stage pipeline combines operational-state-aware verification (OSVA), remediation synthesis (RSA), and correctness validation (CVA). OSVA prunes operationally infeasible candidates under a nine-component industrial state model. RSA emits the strongest remedy permitted by artifact availability across three tiers: protocol mitigation, binary hardening, and SSCKG-constrained source patches. CVA provides conditional correctness evidence through behavioral coverage preservation, independent replay, and a typed rejection-feedback loop from CVA to RSA. The key technical novelty is the joint treatment of the operational-state envelope as a first-class correctness condition and a tiered remedy selector that degrades gracefully as artifact opacity increases. On OIS-RemedBench, a 15-case benchmark spanning firmware, protocol handlers, and ICS/PLC artifacts, SCARA achieves observed 100% precision with no false positives in the evaluated partitions, refutes 20.0% (3/15) of cases as operationally infeasible, and reaches 88.9% (8/9) remediation success after targeted reruns. The UNKNOWN rate drops from 13.3% to 6.7%, Tier-2 overblocking from 80.0% to 25.0%, and OIS-ICS analyst burden from 17.04 to 2.42 hours per case, corresponding to a 7.0× throughput gain. To our knowledge, SCARA is the first end-to-end framework that connects binary vulnerability candidates to conditionally validated remediation for opaque industrial software. ∗
[email protected] Corresponding author. [email protected] ‡ Corresponding author. [email protected] § [email protected] ¶ [email protected] ∥ [email protected] †
SCARA
A P REPRINT
Keywords Opaque industrial software · Binary vulnerability analysis · Automated vulnerability remediation · Symbolic execution · Industrial control systems Highlights. • SCARA: first end-to-end framework for validated OIS vulnerability remediation. • Tiered remediation synthesis provides non-zero remediation without source code. • OIS-RemedBench: first benchmark for opaque industrial software remediation.
1
Introduction
Industrial software supply chains are a growing attack surface for critical infrastructure. Executive Order 14028 [1], NIST SP 800-82r3 [2], and IEC 62443 [3] collectively obligate operators of power, chemical, water, and manufacturing systems to assess and remediate vulnerabilities in their deployed software assets, yet that software is routinely delivered as stripped, symbol-free binaries from which source, debug information, and build environments have been permanently removed. We term this class of artifact Opaque Industrial Software (OIS); Table 2 catalogues its representative classes. Binary analysis has made identifying vulnerability candidates within OIS increasingly tractable — graph-neural detectors [4], binary taint analysis [5, 6], and knowledge-graph behavioural analysis [7] now produce structured alert sets on stripped firmware — but alert generation is not remediation. No existing research framework provides an automated, end-to-end path from binary vulnerability candidates to validated remediation for OIS artifacts. The reason this gap persists is structural. USENIX 2025 SoKs [8, 9] show that contemporary automated vulnerability repair (AVR) systems — LLM-based, program-analysis-based, and agentic — achieve 44–90% repair success across evaluated benchmarks, but every such system requires source code, a compilable artifact, a test suite, or a sanitizer execution trace as its primary input. Systems that operate “at the binary level” (e.g. VulShield [10], CrashRepair [11]) still require the target to be instrumented, compiled, and executed in a controllable environment — preconditions that OIS cannot satisfy. The class of software for which automated remediation is most urgently required is precisely the class for which no existing AVR system can operate. Four specific structural deficits in the existing literature, summarised in Table 1, account for this persistent gap: source dependency of AVR systems (G1), binary analysis terminating at alert generation (G2), ICS/PLC tooling targeting safety rather than security repair (G3), and the absence of a domain-appropriate correctness criterion for OIS remediation (G4). Table 1: Structural deficits in prior work that motivate SCARA. Each row corresponds to one of the four gaps surveyed; the right-hand column lists representative systems exhibiting the deficit. #
Structural deficit
Representative systems
G1
Source dependency of AVR systems
G2
Binary analysis stops at alert generation
G3
ICS/PLC tools target safety, not security repair Appropriate correctness criterion for OIS remediation
VRepair [12], VulRepair [13], VulMaster [14], SAN2PATCH [15], APPATCH [16], PatchAgent [17], Vul-R2 [18]; CrashRepair [11], CONCH [19] Firmadyne [20], FirmAE [21], HALucinator [22], Fuzzware [23], FirmSolo [24], SAFIREFUZZ [25]; KARONTE [5], SaTC [6] VetPLC [26], SymPLC [27], STAutoTester [28], ICSQuartz [29], PLCverif [30]
G4
— (negative observation; no system addresses)
Together, these four deficits create a precondition mismatch: existing repair systems assume source code, sanitizer traces, or executable test harnesses, whereas OIS remediation often begins from opaque artifacts and incomplete operational documentation. To address the four gaps identified above, this paper presents SCARA (Semantics-Constrained Autonomous Remediation Agent), a four-stage framework organized around a tiered remediation model: Tier 1 mitigation (protocol and configuration protection policies), Tier 2 binary hardening (runtime guards via binary instrumentation), and Tier 3 source repair (SSCKG-constrained LLM-synthesized patches). The five principal contributions, of which C1–C4 close Gaps 1–4 respectively and C5 supplies the empirical substrate, are as follows. 2
SCARA
A P REPRINT
C1 — Formal OIS remediation problem statement. We provide the first formal definition of the opaque industrial software remediation problem, comprising a nine-component operational state model, an availability-based tier mapping T (A(B)), a four-class reachability label taxonomy, and the correctness condition for conditional correctness evidence ε(v, Rv ). C2 — Operational-state-aware reachability verification (OSVA). OSVA provides reachability evidence under the full operational state model without source or instrumented execution, eliminating 40.0% of binary alerts as infeasible. C3 — Tiered SSCKG-constrained remediation synthesis (RSA). RSA produces the strongest feasible remedy at the applicable tier, constrained in all tiers by the Software Supply Chain Knowledge Graph (SSCKG) behavioural specification. C4 — Correctness validation (CVA). CVA produces conditional correctness evidence ε(v, Rv ) combining post-remedy UNSAT confirmation, SSCKG behavioural-coverage preservation, domain-invariant compliance, and independent replay across emulated, protocol-harness, and soft-PLC environments. C5 — OIS-RemedBench. The first benchmark for opaque industrial software vulnerability remediation, spanning OIS-Binary, OIS-Protocol, and OIS-ICS partitions with stratified L1–L4 labels.
2
Background and Problem Formulation
2.1
Opaque Industrial Software: Definition and Characteristics
Definition 1 (Opaque Industrial Software). An artifact B is an Opaque Industrial Software (OIS) artifact if B is an industrial software component delivered without (i) source code, (ii) build environment, (iii) hardware interfaces, (iv) runtime dependencies, and (v) operational configuration. As a consequence, vulnerability verification and remediation using conventional source-based methods are infeasible on B. Three features characterize OIS in practice. First, stripping: OIS binaries are systematically stripped of debug symbols, function names, type information, and section metadata before delivery. Second, closed toolchains: the compilers, linkers, and build configurations used to produce OIS are typically proprietary and inaccessible, precluding recompilation from any reconstructed source representation. Third, physical execution dependencies: OIS execution depends on physical hardware — sensor inputs, actuator outputs, NVRAM state, proprietary I/O modules, and licensed fieldbus stacks — that cannot be fully replicated in generic software emulation. OIS artifacts can be classified by their availability class A(B), which determines which remediation tiers SCARA can apply: Table 2: OIS artifact classes grouped by availability class A(B) ∈ {policy-only, binary-rewritable, source-available}, with the applicable remediation tier set T (A) (Eq. (3)) and the success-counting rule used in Section 5. S AT- RELAXED cases are counted only after replay confirmation; U NSAT resolves the candidate as a false positive (no remedy issued); U NKNOWN yields a Tier-1 advisory only.
2.2
Artifact class (example)
Tier set T (A)
Success counted when
Policy-only (A = policy-only) Binary firmware / closed Modbus– DNP3 libs / vendor PLC image
Tier 1 only
CVA accepts T1 policy
Binary-rewritable (A = binary-rewritable) PIE ELF daemons; re-flashable Tier 2; T1 fallback ARM firmware
CVA accepts T2 (or T1 fallback)
Source-available (A = source-available) libmodbus, open62541; OpenPLC / Tier 3; T2/T1 fallback MATIEC-C [31]
CVA accepts T3 (or T2/T1 fallback)
Code Property Graphs and Software Supply Chain Knowledge Graphs
SCARA operates on representations derived from prior binary analysis, specifically the Software Supply Chain Knowledge Graph (SSCKG) produced by [7]. Code Property Graph (CPG). A CPG [32] is a graph Gcpg = (Vcpg , Ecpg ) that unifies the abstract syntax tree (AST), control-flow graph (CFG), and program dependence graph (PDG) of a program into a single queryable structure. 3
SCARA
A P REPRINT
SCARA consumes a CPG produced by the upstream binary-analysis pipeline as the lowest-level structural input to the SSCKG transformation defined below. Abstract Domain A. The abstract domain A is a finite, hierarchical lattice of behavioral security labels instantiated from the MITRE ATT&CK for ICS taxonomy [33]. It comprises five macro-behavior categories, 27 action labels, and 43 risk labels. SSCKG and risk-relevant relations. The SSCKG is a behavioural graph Gssckg = (E, R) derived from Gcpg via a surjective transformation Φ : Gcpg → Gssckg . The entity set E consists of behavioural clusters of semantically related CPG nodes labelled in A; the relation set R encodes a typed vulnerability-relation alphabet ΣR . SCARA operates on the risk-relevant subset Λrisk ⊆ ΣR comprising those relation types that can transmit attacker influence, vulnerability preconditions, or remediation side effects across entities — namely data flow, control dependency, shared memory access, inter-process communication, protocol interaction, and cross-component call. The construction of Gssckg , the full relation taxonomy, the empirical compression ratio against the raw CPG, and the per-entity composite risk score ρr (v) ∈ [0, 1] used by SCARA are properties of the upstream representation and are reported in the SCAA paper. 2.3
Operational State Model
Existing symbolic execution frameworks model execution state as a triple (pc, mem, φ). This representation is insufficient for OIS, where vulnerability reachability critically depends on the external operational context. We extend the standard execution state to a nine-component operational state model: S = (pc, mem, φ, env, io, qproto , qruntime , qcomponent , t)
(1)
Table 3 defines the semantics of each component. As a concrete instance, consider a buffer-overflow candidate in a Modbus coil-write handler: pc locates the basic block performing the unbounded copy; qproto is the Modbus FSM state PostUnitID; Cio requires the addressed coil to lie within the configured coil map of the target device; qruntime restricts execution to the cyclic-scan phase rather than the boot phase; and Ctime bounds the handler response within the protocol’s reply-window deadline. A candidate that is satisfiable over φpath alone may become UNSAT once these external constraints are imposed, which is precisely the class of false positives that OSVA eliminates. Table 3: Nine-component operational state model S. Component
Semantics
Industrial example
pc mem φ env io qproto qruntime qcomponent t
Program counter Memory and register state Path constraint Config., NVRAM, environment Device I/O, fieldbus input Protocol FSM state Runtime lifecycle phase Cross-binary comm. state Timing constraint
Current block in Modbus handler NVRAM register map, I/O table SMT formula over inputs PLC project config., NVRAM Sensor readings, coil states Modbus session state Boot phase, scan cycle N IPC queue depth Scan-cycle deadline
The verification condition for a candidate vulnerability path from source entity src to sink entity snk is satisfiable if: φpath ∧ Cenv ∧ Cio ∧ Cproto ∧ Cruntime ∧ Ccomponent ∧ Ctime is SAT
(2)
Each Cx denotes the conjunction of constraints derived from operational-state component x, with the extraction procedure detailed in Section 3. SCARA employs a four-class reachability label taxonomy — S AT- STRICT (satisfiable under all constraints with witness (I ∗ , S ∗ ); passed to RSA), S AT- RELAXED (satisfiable only after relaxing an underdocumented constraint; passed to RSA but requires replay confirmation), U NSAT (infeasible under all constraints; recorded as a refutation certificate, no remedy issued), and U NKNOWN (budget exhausted or modelling gap; Tier-1 advisory only) — which corresponds to the L2 row of the OIS-RemedBench evidence ladder in Table 5. The correctness condition for conditional correctness evidence ε(v, Rv ) requires that all four of the following hold: 1. Re-running OSVA on the post-remedy artifact B ′ returns UNSAT for the original candidate path. 2. SSCKG behavioral coverage is preserved: BCP(Gssckg , G′ssckg ) ≥ τcov , where BCP is the Behavioral Coverage Preservation ratio measuring the fraction of non-vulnerable SSCKG relations retained after remediation (formally defined in Section 3) and τcov is its acceptance threshold. 4
SCARA
A P REPRINT
3. No domain invariant is violated. 4. Where a replay harness is available (L3-labeled cases), independent replay confirms the UNSAT outcome. 2.4
Formal Problem Statement
Input: • Binary artifact B (stripped; no source code available); • SSCKG Gssckg = (E, R) with behavioral annotations and composite risk scores ρr (v); • Vulnerable entity set Vr = {v ∈ E | ρr (v) ≥ τ }; • Artifact availability class A(B) ∈ {policy-only, binary rewritable, source-available}, determining the tier set if A = policy-only {1} T (A) = {1, 2} (3) if A = binary-rewritable {1, 2, 3} if A = source-available. Output: For each v ∈ Vr : a reachability label ℓv , with witness (I ∗ , S ∗ ) for SAT labels or refutation constraint ¬Cj for UNSAT; for each v with ℓv ∈ {SAT-strict, SAT-relaxed}: a remediation artifact Rv at the strongest tier in T (A) satisfying the correctness condition; and conditional correctness evidence ε(v, Rv ) for each produced remedy. Non-goals. SCARA does not discover new vulnerabilities; that function is performed by the upstream binary analysis tool. SCARA does not provide formal proofs of global safety properties; the correctness evidence it produces is conditional on the completeness of the modeled operational state S.
3
The SCARA Framework
3.1
System Overview
SCARA decomposes the formal problem across four agents, shown as the pipeline of Figure 1: CACA normalises heterogeneous vulnerability alerts and estimates the operational context (ablations A8, A9); OSVA performs budgeted reachability verification with controlled relaxation (A1–A3); RSA synthesises the strongest feasible remedy with δ-feedback ingestion (A5, A6); and CVA either issues conditional correctness evidence ε(v, R) or returns a typed rejection constraint δ to RSA for at most K = 3 resynthesis iterations per tier (A4, A7). The four-stage decomposition is motivated by two properties of the OIS-remediation problem: each stage has a distinct failure mode that monolithic systems cannot ablate, and the closed-loop CVA→RSA path with typed δ enables the iterative refinement that single-pass pipelines lack. The operational context Ω supplied to CACA is the optional external evidence used to construct Siprior , to select the relevant constraint families, and to infer the availability class; it is a tuple of per-dimension hints Ω = (Ωart , Ωenv , Ωio , Ωproto , Ωruntime , Ωcomponent , Ωtime , Ωreplay )
(4)
covering artifact metadata, environment/NVRAM/configuration, MMIO/fieldbus, protocol FSM, runtime lifecycle, cross-binary topology, timing budgets, and replay-harness availability respectively (full schema in the supplementary material). 3.2
Candidate Acquisition and Context Agent
CACA transforms heterogeneous vulnerability evidence into verification tasks. Its inputs are an SSCKG Gssckg , nodelevel risk scores ρr (v), the raw binary artifact B, and optional context. Its output is a candidate set, ranked downstream by Eq. (6): C = {(vi , srci , snki , ρi , Siprior )}
(5)
where vi is the SSCKG entity associated with the candidate, srci and snki denote the suspected source and sink, ρi is the candidate risk score, and Siprior is the initial estimate of the operational state required for verification. CACA accepts vulnerability candidates from multiple upstream generators because OIS artifacts differ in available evidence. For source-available or intermediate-representation cases, candidates may originate from static analyzers or 5
SCARA
A P REPRINT
Figure 1: SCARA four-stage pipeline. CACA normalises heterogeneous candidate evidence; OSVA verifies operational reachability under the nine-component state model; RSA synthesises the strongest feasible remedy at the artifact’s availability tier; and CVA closes the loop by either issuing conditional correctness evidence ε(v, R) or returning a typed rejection constraint δ to RSA for at most K = 3 resynthesis iterations per tier. Algorithm 1 SCARA Controller Require: Binary artifact B, SSCKG Gssckg , candidate alert set Vr , operational context Ω (Eq. (4)) Ensure: Per-candidate outcomes: verified remediations, resolved FPs, unconfirmed records, advisories 1: C ← CACA.normalize_and_rank(Vr , Gssckg , B, Ω) 2: for each candidate c in C do 3: label, witness, reason ← OSVA.verify(B, Gssckg , c) ▷ Alg. 2 4: if label = U NSAT then 5: record_resolved_false_positive(c, reason) ▷ Prop. 1 6: continue 7: end if 8: if label = U NKNOWN then 9: record_unresolved_or_advisory(c, Ω) ▷ see below; not routed through Alg. 3 10: continue 11: end if 12: if label = S AT- RELAXED and not replay_available(witness) then 13: record_unconfirmed_candidate(c, witness) 14: continue 15: end if 16: tiers ← feasible_tiers(CACA.availability_class(B)) 17: result ← RSA_CVA_loop(B, Gssckg , witness, label, tiers) ▷ Alg. 3; K = 3 18: record(result) 19: end for
source-to-sink rules. For binary-only firmware, candidates may derive from multi-binary taint analysis, keyword-guided firmware analysis, CVE-linked advisory matching against the NVD [34], or fuzzing crashes mapped back to SSCKG entities. CACA normalizes these inputs by mapping each candidate to the corresponding SSCKG entity and relation type. This mapping is necessary because OSVA’s constraint encoding depends on the semantic relation associated with the candidate: a protocol-interaction relation suggests constraints over qproto , whereas a memory-mapped I/O relation suggests constraints over io and qruntime . Unlike upstream generators such as KARONTE [5] and SaTC [6], which produce taint-derived alerts without operational context, CACA enriches each normalized candidate with the state dimensions required for OSVA’s constraint encoding, thereby converting a raw alert into a verification task with a defined scope. CACA ranks candidates using both the risk score inherited from upstream analysis and the semantic centrality of the candidate entity in the SSCKG: 6
SCARA
A P REPRINT
Figure 2: CACA normalisation funnel. Heterogeneous vulnerability evidence (static-analyser candidates, taint-derived alerts, fuzzing crashes, CVE-linked advisories) is mapped to a uniform (v, src, snk, S prior ) tuple keyed to the SSCKG, producing a single verification task that OSVA can consume.
rank(vi ) = α · ρr (vi ) + (1 − α) · sem_centrality(vi ),
α ∈ [0, 1].
(6)
The parameter α balances local risk against graph-level importance and is fixed at α = 0.6 in the primary experiments, calibrated on the OIS-RemedBench validation subset; the value gives slightly more weight to the upstream risk score than to SSCKG semantic centrality. This design is adopted because high-risk nodes that are semantically isolated may be less urgent than moderately risky nodes that lie on many source-to-sink paths. Semantic centrality is formally defined as the normalized betweenness centrality of vi in the SSCKG Gssckg = (E, R) of Section 2.2, restricted to the risk-relevant relation subset Λrisk ⊆ ΣR : sem_centrality(vi ) =
1 |E|(|E| − 1)
X s,t∈E, s̸=t s,t̸=vi
σst (vi ) σst
(7)
where σst is the number of shortest paths between entities s and t over edges in Λrisk , and σst (vi ) is the subset passing through vi . Betweenness centrality over the SSCKG is adopted rather than over the raw binary CFG because a node with high SSCKG betweenness lies on many source-to-sink behavioral paths and therefore has disproportionate operational impact at the industrial protocol or control level. CACA also determines the artifact availability class A(B) ∈ {policy-only, binary-rewritable, source-available}, which selects the applicable tier set T (A) defined in Section 2.4 (Eq. (3)): policy-only artifacts admit only Tier 1; binary-rewritable artifacts admit Tier 1 and Tier 2; source-available artifacts admit all three tiers. 3.3
Operational-State Verification Agent
OSVA operates over the operational state model S defined in Section 2.3 (Eq. (1)) and the six constraint families Cenv , Cio , Cproto , Cruntime , Ccomponent , Ctime introduced therein. The prior state estimate Siprior supplied by CACA initialises these components before OSVA’s constraint encoding begins. OSVA verifies whether a candidate path is reachable under the modeled operational state. Given a ranked candidate (vi , srci , snki , Siprior ) and binary artifact B, OSVA returns a reachability label ℓi ∈ {S AT- STRICT, S AT- RELAXED, U NSAT, U NKNOWN}. For satisfiable candidates, OSVA also returns a witness (I ∗ , S ∗ ), where I ∗ is a concrete or partially concrete input vector and S ∗ is the corresponding operational state. For infeasible candidates, OSVA returns the violated constraint or constraint family responsible for the refutation. The verification condition V that OSVA discharges is the operational reachability condition of Eq. (2): a candidate is reachable only if φpath ∧ Ck ∈ΣS Ck is satisfiable under the encoded constraints. 7
SCARA
3.3.1
A P REPRINT
Symbolic Execution Setup
OSVA selects the symbolic execution engine according to the artifact type. For binary-only firmware and stripped services, OSVA uses angr [35], because angr’s SimProcedure framework provides behavioral abstractions for unresolved peripheral calls, vendor runtime services, and MMIO operations that KLEE cannot model without source-level stubs. For artifacts that can be reliably lifted to LLVM IR using RetDec or McSema, OSVA operates at the IR level; this path is taken only when lifting quality can be verified, because unreliable lifting introduces spurious paths. For the OIS-ICS partition, where IEC 61131-3 Structured Text programs may be translated into C through MATIEC, OSVA compiles the generated C into LLVM IR and executes it with KLEE [36], because KLEE provides path-complete symbolic exploration under LLVM IR that is reliable when the source-to-IR translation faithfully preserves the structured-text semantics. SCARA does not assume that every OIS artifact can be reduced to LLVM IR; the angr path is the fallback for all cases where IR lifting is unavailable or unreliable. Within the angr path, for protocol-handler cases, OSVA prior initialises symbolic execution from the state implied by qproto , avoiding the exploration of protocol states that cannot precede the candidate sink; for binary firmware, OSVA represents peripheral inputs, configuration values, and external service responses as symbolic variables constrained by available documentation or inferred SSCKG relation types. These models are deliberately conservative: under-documented dimensions are recorded and may lead to U NKNOWN or S AT- RELAXED, rather than being silently treated as complete. 3.3.2
SSCKG-Guided Path Prioritization
OSVA employs the SSCKG as a semantic roadmap for symbolic exploration. The substantive insight here is the use of the SSCKG itself as the semantic prior over binary-level path exploration; the SBERT-based encoding and cosine similarity below are off-the-shelf instruments for operationalising it. The SSCKG path from srci to snki encodes behaviorally meaningful steps that should be reflected in the binary-level path if the candidate is genuine. OSVA first projects this SSCKG path onto the binary CFG using CACA’s entity-to-function mapping, then scores each candidate CFG path according to its semantic alignment with the SSCKG path: score(pj ) = sim(SBERT(labels(pj )), SBERT(labels(Pssckg )))
(8)
Formally, let labels(pj ) = (l1 , . . . , lm ) be the ordered sequence of SSCKG entity labels assigned to basic blocks along binary path pj , obtained via CACA’s entity-to-function mapping, and let labels(Pssckg ) = (l1′ , . . . , lk′ ) be the entity label sequence of the SSCKG source-to-sink path. Both sequences are encoded using the SBERT [37] sentence-transformer model (all-mpnet-base-v2, 768-dimensional embeddings). The similarity is the standard cosine similarity: sim(u, v) =
u·v ∈ [−1, 1]. ∥u∥ · ∥v∥
(9)
Because cosine similarity is bounded in [−1, 1], scores are mapped to [0, 1] by an affine transformation faithful to Eq. (9), s̃j = (score(pj ) + 1)/2, rather than by min–max normalisation over the candidate path set; the latter would make the budget allocation depend on the worst-aligned explored path and could exaggerate small score differences when all paths are similarly aligned. OSVA then allocates solver budget proportionally to semantic alignment via an explicit softmax over the explored binary-level path set P : exp(s̃j /τp ) , pk ∈P exp(s̃k /τp )
budget(pj ) = Ttotal · P
(10)
where Ttotal is the total per-candidate strict-pass solver budget and τp is the softmax temperature. In the primary experiments Ttotal = 300 s per candidate and τp = 0.5, calibrated on the held-out validation subset; the relaxed pass uses a separate budget Trelaxed = 150 s. High-scoring paths therefore receive more solver time earlier, while low-scoring paths remain available if the high-priority budget is exhausted. This distinction matters because hard pruning would reduce the false-positive rate at the cost of missing true positives. SCARA employs prioritization rather than pruning so that false-negative rates can be measured and recall can be reported alongside false-positive reduction. 3.3.3
Operational-State Constraint Encoding
OSVA translates the prior estimate Siprior into SMT constraints over symbolic variables, one per family in ΣS (Table 3). Concrete encodings include: Cenv over NVRAM ranges and PLC project parameters; Cio over MMIO/fieldbus value ranges (e.g., a Modbus register address restricted to [0, 65535], a coil to a Boolean domain); Cproto over protocol FSM transitions (e.g., session establishment must precede a write); Cruntime over boot/scan-cycle phases and initialisation 8
SCARA
A P REPRINT
Figure 3: Operational-state reachability analysis in OSVA. A candidate source-to-sink path is projected from the SSCKG to the executable representation and checked against path, environment, I/O, protocol, runtime, component, and timing constraints.
status; Ccomponent over IPC, shared-memory, or file-mediated transfers; and Ctime over watchdogs, scan-cycle deadlines, and guard-overhead budgets. If OSVA cannot decide a candidate under the strict constraint set within the solver budget, it performs one controlled relaxation pass targeting the constraint dimension with the weakest evidence — for example, a configuration variable inferred from incomplete documentation. A satisfiable result from the first (strict) pass is labeled S AT- STRICT. A satisfiable result obtained only after relaxation is labeled S AT- RELAXED and is not counted as confirmed until replay validates the witness. If the second pass also fails to establish satisfiability or unsatisfiability, OSVA returns U NKNOWN and records the missing or uncertain dimension to guide manual follow-up. 3.3.4
Reachability Labels and Downstream Routing
The four OSVA labels carry different downstream consequences. S AT- STRICT candidates are eligible for remediation synthesis. S AT- RELAXED candidates may be forwarded to RSA, but their remediation is counted as successful only after independent replay confirms the relaxed witness. U NSAT candidates are reported as false positives relative to the encoded operational-state model; no remedy is generated, because there is no reachable vulnerability to remediate. U NKNOWN candidates are reported as unresolved; SCARA may produce an advisory Tier 1 policy if an enforcement point exists, but this advisory is not counted as validated remediation. This routing rule prevents two common errors in alert-driven repair. First, it avoids converting infeasible alerts into unnecessary operational restrictions. Second, it avoids treating conservative policies generated for uncertain cases as evidence of repair success. The distinction is central to SCARA’s evaluation, where false-positive refutation, verified remediation, and advisory mitigation are reported as separate outcome categories. 3.4
Remediation Synthesis Agent
RSA synthesizes the strongest feasible remediation artifact for candidates that OSVA has labeled S AT- STRICT or, conditionally, S AT- RELAXED. Its inputs are the OSVA result, the candidate entity vi , the SSCKG, the prior state model, and the tier set T (A) associated with the artifact availability class. RSA outputs a candidate remediation Ri at one of three tiers. RSA follows a strongest-feasible-tier policy, where tier strength is ordered as Tier 3 ≻ Tier 2 ≻ Tier 1, reflecting increasing remediation depth: Tier 3 removes the vulnerable code path at the source level, Tier 2 inserts a runtime guard into the binary, and Tier 1 enforces a policy restriction at an external enforcement boundary. For a policy-only artifact, RSA attempts only Tier 1 mitigation. For a binary-rewritable artifact, RSA attempts Tier 2 binary hardening with Tier 1 as fallback. For a source-available artifact, RSA attempts Tier 3 source repair with Tier 2 and Tier 1 as fallbacks. If CVA rejects a remedy, RSA incorporates the rejection constraint and regenerates a remedy, up to a fixed iteration budget. If all feasible tiers fail validation, the candidate is marked R EMEDIATION -FAILED. 9
SCARA
A P REPRINT
Algorithm 2 OSVA.verify. The strict pass is per-path under budget Ttotal allocated by Eq. (10); the relaxed pass is a single global pass over the disjunction of explored path conditions under budget Trelaxed , relaxing the weakest-evidence constraint family. Require: Artifact B, SSCKG Gssckg , candidate c = (v, src, snk, S prior ) Ensure: Label ℓ, witness (I ∗ , S ∗ ) or ∅, reason 1: P ← project_ssckg_path_to_executable_paths(Gssckg , B, c) 2: Pexplored ← ∅; Prefuted ← ∅; Pinconclusive ← ∅ 3: for each path p in prioritize_by_semantic_alignment(P, Gssckg , c) do 4: φp ← path_condition(p) ▷ local; distinct from SSCKG morphism Φ prior 5: C ← encode_constraints(c.S , B, p) 6: status, model ← solve(φp ∧ C, budget(p)) ▷ Eq. (10) 7: Pexplored ← Pexplored ∪ {p} 8: if status = S AT then 9: return S AT- STRICT, model, ∅ ▷ Prop. 2 10: else if status = U NSAT then 11: Prefuted ← Prefuted ∪ {p}; collect_refuting_constraint(p, C) 12: else ▷ U NKNOWN / solver timeout on this path 13: Pinconclusive ← Pinconclusive ∪ {p}; mark_path_inconclusive(p) 14: end if 15: end forW 16: ΦP ← p∈Pexplored φp ▷ disjunction over explored path conditions 17: Crelaxed ← relax_weakest_evidence_dimension(C) 18: status, model ← solve(ΦP ∧ Crelaxed , Trelaxed ) 19: if status = S AT then 20: return S AT- RELAXED, model, relaxed_dimension(C, Crelaxed ) 21: end if 22: if Prefuted = Pexplored and status = U NSAT then 23: return U NSAT, ∅, collected_refutation ▷ Prop. 1 24: end if 25: return U NKNOWN, ∅, timeout_or_model_gap
Figure 4: Availability-aware remediation synthesis in RSA. SCARA selects the strongest feasible remediation tier according to artifact availability.
10
SCARA
A P REPRINT
Algorithm 3 RSA_CVA_loop. Per-tier resynthesis budget K defaults to K = 3 in the primary experiments. Tier-3 is attempted at most once per candidate; lower tiers are tried only after the higher tier exhausts K iterations. Require: Artifact B, SSCKG Gssckg , candidate c, witness w, label ℓ, tier set T , per-tier resynthesis budget K (default K = 3), enforcement-point context Ωreplay Ensure: Accepted remedy with ε(v, R), or R EMEDIATION -FAILED, or advisory 1: for tier in strongest_to_weakest(T ) do 2: ∆ ← {} ▷ rejection constraints are tier-local; cross-tier sharing not assumed 3: for iter = 1 to K do 4: R ← synthesize_remediation(tier, B, Gssckg , c, w, ∆) 5: verdict, ev ← CVA.validate(B, Gssckg , c, R, ℓ) ▷ Alg. 4 6: if verdict = ACCEPT then 7: return verified_result(c, R, tier, ev) ▷ Prop. 3 8: end if 9: ∆ ← ∆ ∪ {ev} 10: end for 11: end for 12: if has_enforcement_point(Ωreplay ) then 13: return advisory_unverified_policy(c) 14: end if 15: return remediation_failed(c)
3.4.1
Tier 1: Protocol and Configuration Mitigation
Tier 1 generates protocol or configuration policies. It applies to any OIS artifact for which an enforcement point exists — a network firewall, protocol gateway, device configuration interface, PLC project parameter, or access-control layer. Given a reachable path, RSA extracts the protocol states or configuration conditions necessary to traverse the path and identifies the minimal gate operation. RSA generates a policy that restricts the gate condition while preserving benign operations. Depending on the artifact, the policy may be expressed as a Modbus TCP firewall rule, an OPC-UA role restriction, an IEC 60870-5-104 filter, an iptables or nftables rule, or a device configuration constraint. The generated policy is then forwarded to CVA, which tests protocol conformance, benign trace replay, and false-blocking behavior. A Tier 1 policy is accepted only if it blocks the vulnerability trigger without disrupting required normal operations beyond a configured threshold. 3.4.2
Tier 2: Binary Hardening
Tier 2 applies when the artifact is binary-rewritable. RSA employs binary rewriting tools — RetroWrite [38] for position-independent ELF, E9Patch [39] for x86 PE, and GTIRB for multi-architecture transformation. RSA first maps the vulnerable SSCKG entity back to a binary function or basic-block region using CACA’s entity-tofunction mapping. It then derives the blocked condition class: ψvuln = projobs (φpath ∧ Cenv ∧ · · · ∧ Ctime )
(11)
where projobs denotes projection over variables observable at the insertion point, such as registers, memory fields, protocol parameters, or runtime flags. The guard evaluates ψvuln and redirects execution to a safe handler if the condition is satisfied. 3.4.3
Tier 3: SSCKG-Constrained Source-Level Repair
Tier 3 applies only when source code or generated C code is available. RSA converts the OSVA witness into an LLM-interpretable trigger description, extracts a behavioral preservation requirement from the SSCKG, and includes this requirement in the repair prompt together with the vulnerable function and domain-specific secure coding rules. RSA generates k = 5 candidate repair artifacts; no artifact is accepted directly from the LLM. All candidates are compiled and forwarded to CVA for selection. This design deliberately isolates the LLM’s role to candidate generation; correctness is determined by the validation stage rather than by the model’s confidence, thereby avoiding the failure mode in which a plausible but semantically incorrect patch is accepted without verification. 11
SCARA
3.5
A P REPRINT
Correctness Validation Agent
CVA determines whether a candidate remediation can be accepted and issues conditional correctness evidence ε(vi , Ri ). Definition 2 (Conditional Correctness Evidence). ε(v, R) is a four-component certificate (l′ , BCP, Scheck , replay) where: 1. l′ = U NSAT (post-remedy reachability re-verification of the original candidate); 2. BCP(Gssckg , G′ssckg , c) ≥ τcov (behavioral coverage preservation, Eq. (14)); 3. Scheck = ⊤ (all tier-specific side-effect checks pass); 4. replay ∈ {C ONFIRMED, U NAVAILABLE, FAILED, N OT _A PPLICABLE}, recording whether replay confirmed the witness is blocked in the emulation or harness environment, was not available for the benchmark case, was attempted but inconclusive, or was not operationally required for the artifact type. 3.5.1
Post-Remedy Reachability Re-Verification and Replay
CVA first applies the remedy to the target artifact, then reruns OSVA on the modified artifact B ′ . The primary acceptance condition is that OSVA returns UNSAT for the original vulnerability path. To reduce the circularity of using the SSCKG as both specification and validation substrate, CVA supplements SSCKG-based checks with independent replay. For OIS-Binary cases, the witness is replayed against a rehosted firmware. For OIS-Protocol cases, against a protocol harness. For OIS-ICS cases, against a soft-PLC or comparable runtime. In OIS-RemedBench, replay infrastructure is available for the L3-labeled subset of cases; L2-only cases without a replay harness receive replay = UNAVAILABLE in their ε certificate and are not counted as replay-verified remediations. Replay confirmation elevates label reliability from the solver-level determination to independently verified status: a S AT- STRICT or S AT- RELAXED result that replay confirms is promoted to V ERIFIED; a S AT- RELAXED result that cannot be replayed remains unconfirmed and is not counted as successful remediation. CVA also performs a root-cause displacement check by rerunning OSVA on neighboring paths identified during OSVA, to determine whether the remedy merely shifts the vulnerable behavior to an adjacent code location. In addition, CVA reapplies upstream analysis to the modified artifact and flags any newly introduced high-risk SSCKG nodes as potential new vulnerabilities introduced by the remedy. 3.5.2
Behavioral Coverage Preservation
After applying a remedy, CVA recomputes the SSCKG G′ssckg from the modified artifact and compares the reachable entity set in G′ssckg with the corresponding set in the original graph. Reachability is measured with respect to operationally meaningful entry entities. Let Φ−1 (e) denote the preimage in the source CPG of an SSCKG entity e ∈ E. The set of entry entities is: Eentry (G) = { e ∈ E | Entry(e) }, (12) where the entry predicate is satisfied when at least one CPG node mapped into e is tagged as an externally invocable boundary or execution root: Entry(e) ⇐⇒ ∃ n ∈ Φ−1 (e) : exported(n) ∨ networkHandler(n) ∨ protocolHandler(n) ∨ firmwareServiceEntry(n) ∨ taskRoot(n) ∨ startupRoutine(n) ∨ ScanRoot(n).
(13)
Let R(G) = {e′ ∈ E | ∃ e ∈ Eentry (G) : e ⇝ e′ } denote the entities reachable from any entry entity over the relations of Λrisk , and let Vvuln (c) ⊂ E denote the SSCKG entities on the confirmed vulnerability path of candidate c. The behavioral coverage preservation rate is candidate-specific: BCP(G, G′ , c) =
|R(G′ ) ∩ (R(G) \ Vvuln (c))| ∈ [0, 1]. |R(G) \ Vvuln (c)|
(14)
The objective is not to prove full semantic equivalence but to quantify whether the remediation removes non-vulnerable behaviors observable at the SSCKG abstraction level; a remedy is accepted only if BCP(Gssckg , G′ssckg , c) ≥ τcov , with 12
SCARA
A P REPRINT
τcov = 0.95 in the primary experiments, calibrated on the held-out validation subset. Because SSCKG reachability alone may miss subtle semantic changes that manifest only under specific operational conditions, CVA supplements this measure with two external checks: when a vendor patch is available for the same vulnerability, CVA compares the SSCKG coverage set of the SCARA-remediated artifact against that of the vendor-patched artifact as an external reference point; and for every CVA-accepted case, manual review cross-validates SSCKG-level coverage preservation against the independent replay outcome, confirming whether SSCKG reachability preservation acts as a reliable proxy for operational behavior preservation on the current benchmark. 3.5.3
Domain-Invariant and Side-Effect Checks
CVA applies tier-specific side-effect checks to each candidate remedy (Table 4). A remedy is rejected if any check fails or yields a metric outside the tier’s configured threshold; in particular, a Tier 1 policy that blocks a substantial fraction of benign operations is rejected even if it successfully blocks the vulnerability trigger, because operational acceptability is a necessary condition for deployment. Table 4: CVA tier-specific side-effect checks. A remedy is rejected if any check fails or yields a metric outside the tier’s configured threshold. Tier
Side-effect checks
T1
Protocol conformance; benign-trace replay; false-blocking rate; comparison against vendor or CERT guidance where available Overblocking (guard fires outside ψvuln ); underblocking (dangerous states inside ψvuln bypass the guard); timing compliance against scan-cycle slack on OIS Compilability; regression tests where available; OSVA re-verification after compilation; domaininvariant preservation; optional formal-property check
T2 T3
3.5.4
Closed-Loop Feedback and Termination
If CVA rejects a remediation, it returns a rejection constraint δ to RSA. The constraint specifies what must change in the next synthesis iteration — for example, “the policy must not block transition qa → qb ,” “the guard must not fire in benign state s,” or “entity e must remain reachable.” RSA incorporates δ into the next synthesis attempt. SCARA permits at most three RSA–CVA iterations per candidate by default (K = 3), in order to bound remediation latency. The bound does not affect soundness — if no remedy is accepted within K iterations, the case is marked R EMEDIATION -FAILED and the final rejection constraint is retained as diagnostic information for manual follow-up. If the selected tier fails within the iteration budget, RSA falls back to the next lower applicable tier. If all applicable tiers fail, the case is marked R EMEDIATION -FAILED, and any advisory Tier 1 policy is reported separately from verified remediation. 3.6
Complexity and Bounded Soundness
In the worst case, OSVA’s search complexity is proportional to the size of the binary-level graph and the number of encoded operational constraint families: O(|Vcpg | · |ΣS |) , (15) where ΣS = {Cenv , Cio , Cproto , Cruntime , Ccomponent , Ctime } denotes the six encoded operational constraint families used by OSVA (|ΣS | = 6); the nine-component operational state tuple S of Section 2.3 contains ΣS together with the three baseline symbolic-execution components (pc, mem, φ). SSCKG-guided prioritization reduces the expected search space by operating over behaviorally compressed entities and by concentrating solver budget on paths semantically aligned with the candidate source-to-sink path: O(|E| · |Pssckg |) , (16) where |E| is the SSCKG entity count (the entity set introduced in Section 2.2) and |Pssckg | is the number of SSCKG paths from the candidate source to the vulnerable sink. This reduction holds in expectation under two conditions: (a) |E| ≪ |Vcpg |, which holds for the SSCKG instances consumed by SCARA; and (b) the true vulnerability path has high semantic alignment with the SSCKG source-to-sink path, so that budget allocation concentrates solver effort on it early. In the degenerate case where all paths have equal alignment scores, SCARA degrades to uniform budget allocation over all explored paths, preserving recall at the cost of later average SAT detection time. The reduction is therefore an expected-case benefit rather than a formal worst-case guarantee, because low-priority paths are deprioritized rather than eliminated. SCARA provides the following bounded soundness guarantees. 13
SCARA
A P REPRINT
Algorithm 4 CVA.validate. The post-remedy OSVA call uses the original SSCKG Gssckg to retain the candidate’s entity reference v; the rebuilt G′ is used solely for BCP and side-effect checks. Require: Original artifact B, SSCKG Gssckg , candidate c, remedy R, label ℓ Ensure: ACCEPT with ε(v, R), or R EJECT with constraint δ 1: B ′ ← apply_remediation(B, R) 2: l′ , _, reason ← OSVA.verify(B ′ , Gssckg , c) 3: if l′ ̸= U NSAT then 4: return R EJECT, δreachability (reason) 5: end if 6: if replay_required(ℓ) then 7: replay_status ← replay_witness(B ′ , c) 8: if replay_status ̸= C ONFIRMED _B LOCKED then 9: return R EJECT, δreplay (replay_status) 10: end if 11: end if 12: G′ ← rebuild_ssckg(B ′ ) 13: cov ← BCP(Gssckg , G′ , c) ▷ Section 3.5.2 14: if cov < τcov then 15: return R EJECT, δcoverage (cov) 16: end if 17: side_effects ← tier_specific_checks(B, B ′ , R) 18: if side_effects fail then 19: return R EJECT, δside_effect (side_effects) 20: end if 21: return ACCEPT, conditional_evidence(l′ , cov, side_effects) ▷ Prop. 3
Proposition 1 (UNSAT Soundness). If OSVA returns U NSAT for candidate (v, src, snk, S prior ) against artifact B, then no execution state S |= C permits control flow to reach snk via a path through v. Assumptions: (i) the encoded constraint model C correctly bounds the operational envelope; (ii) the strict-pass solver budget allocated by Eq. (10) is sufficient on every explored path to either refute it or generate a witness; and (iii) the SSCKG-guided projection from src to snk enumerates every semantically relevant binary-level path. Unmodeled or mis-specified constraints, paths skipped by the projection, and per-path solver timeouts are not covered by this guarantee. Proof sketch: OSVA returns U NSAT only when every explored path returned solver-U NSAT under φp ∧ C and the relaxed-pass solve over the disjunction ΦP also returned U NSAT (Algorithm 2). Paths where the solver exhausted its budget without a verdict are recorded in Pinconclusive and force the global label to U NKNOWN, not U NSAT; the label is therefore never used speculatively. Proposition 2 (SAT-strict Witness Validity). If OSVA returns S AT- STRICT with witness (I ∗ , S ∗ ), then (I ∗ , S ∗ ) |= φp ∧C as evaluated by the solver. Assumptions: the symbolic execution model faithfully abstracts the artifact’s concrete semantics; specifically, (i) the binary lifter or symbolic engine soundly models the instruction semantics of B; (ii) peripheral, MMIO, and externalservice models are complete with respect to the candidate path; and (iii) the SMT solver is correct on the encoded theory fragments. Unsound lifters, incomplete peripheral models, or solver bugs may produce spurious witnesses outside the scope of this proposition. Proposition 3 (CVA Conditional Correctness). If CVA issues ε(v, R) = (l′ , BCP, Scheck , replay), then: l′ = U NSAT for the original candidate against B ′ ; BCP(Gssckg , G′ssckg , c) ≥ τcov ; all side-effect checks pass; and if replay was required, the witness was confirmed blocked. Assumptions: (i) the post-remedy SSCKG G′ssckg faithfully reflects the runtime behavior of B ′ at the abstraction level of A; (ii) the remediation preserves the SSCKG entity reference v so that OSVA can re-run the original candidate against B ′ (cf. Algorithm 4); and (iii) where replay applies, the harness exercises the witness path under operationally representative inputs. The proposition does not imply global semantic equivalence between B and B ′ , nor the absence of vulnerabilities in unmodeled or underspecified state dimensions. 14
SCARA
A P REPRINT
Table 5: OIS-RemedBench label hierarchy. The L2 sub-rows enumerate the four-class reachability taxonomy used by OSVA, as introduced in Section 2.3. Level Design
Meaning
Assignment / downstream action
L1 L2
Candidate Reach-labeled
Alert exists; no reachability GT Four-class label with evidence
Upstream tool output Two independent methods
Sat-strict
Satisfiable under all constraints; witness Pass to RSA (I ∗ , S ∗ ) Satisfiable after relaxing under-documented Pass to RSA; require replay constraint Infeasible under all constraints; false posi- Refutation certificate; no remtive edy Budget exhausted or modelling gap Advisory Tier 1 only
Sat-relaxed Unsat Unknown L3 L4
Replay-labeled Witness validated in harness RemedyVendor or expert remedy available labeled
4
Experimental Design
4.1
The OIS-RemedBench Benchmark
FirmAE / harness / soft-PLC Vendor patch / CERT advisory
The empirical substrate of this work — and contribution C5 — is OIS-RemedBench, the first benchmark providing stratified reachability and remediation ground truth for opaque industrial software. The benchmark comprises n = 15 cases evenly distributed across three partitions (5 per partition), with the four-level stratification scheme of Table 5 and the per-partition evidence-availability profile of Figure 5. The three partitions are: OIS-Binary (industrial gateway firmware, embedded Linux services, HMI back-ends; predominantly CWE-119/120, 125/787, 416, 134, 78); OISProtocol (Modbus, DNP3, OPC-UA, and IEC 60870-5-104 handlers, with libmodbus, OpenDNP3, and open62541 contributing source-available cases that admit high-confidence L4 labels); and OIS-ICS (IEC 61131-3 control logic on the OpenPLC runtime [40], MATIEC-compiled programs, the public ICSQuartz ST subset [29], and VetPLCstyle boundary cases adapted as security vulnerabilities). Representative CVE coverage includes CVE-2020-16233 (BIN-CISA-001), CVE-2023-44318 (BIN-VEND-001), CVE-2018-7846 (BIN-CISA-002), and CVE-2023-44319 (PROT-VEND-001). All figure denominators are derived from explicit per-case rows rather than from aggregate prose counts. Figure 5 renders the per-partition evidence-availability profile as a tile chart, with tile shade encoding the proportion of cases satisfying each evidence level (L1 candidate, L2 reachability label, L3 replay harness, L3 confirmed replay, L4 remedy, source-available, binary-rewritable, PEP-reachable) within each five-case partition; Figure 6 renders the CWE coverage across partitions. Labeling methodology. L2 labels are assigned by two independent methods — static analysis (CodeQL / Joern / KARONTE / SaTC) and operational-state-aware dynamic exercise under FirmAE (OIS-Binary), libmodbus/OpenDNP3 harnesses (OIS-Protocol), or the OpenPLC runtime (OIS-ICS); disagreements are arbitrated by a domain expert. L3 replay follows the CVA protocol of §3.5. L4 remedy labels derive, in decreasing confidence order, from vendor patches, CERT ICS advisories, or expert-authored fixes verified by OSVA re-run; vendor patches were frozen prior to evaluation so that no L4 evidence could leak into RSA. Domain-invariant labels are drawn from the Modbus [41], DNP3 [42], IEC 60870-5-104 [43], and IEC 61131-3 [44] standards. The full case manifest (predominant CWEs: 119, 787, 125, 20, 78, 126, 416) is released with the artifact. 4.2
Baselines
Baseline evaluation separates three distinct quantities to avoid the conflation identified in prior AVR benchmarking work [45]: applicability rate (the fraction of OIS-RemedBench cases for which a baseline can produce any non-trivial output), conditional performance (the success rate on the subset where the baseline is applicable), and end-to-end utility (the fraction of all benchmark cases for which the baseline provides a validated outcome). All three are reported separately throughout Section 5. The static-analysis row of Table 6 is reported as a deduplicated alert-union baseline. Each CodeQL, Joern, KARONTE, SaTC, or ICSQuartz alert is mapped to an SSCKG entity and source-sink relation, deduplicated by a stable key, and then 15
SCARA
A P REPRINT
Figure 5: OIS-RemedBench evidence-availability tile chart. Each row of tiles within a partition shows the fraction of the five cases satisfying that evidence level (L1 candidate, L2 reachability label, L3 replay harness, L3 confirmed replay, L4 remedy, source available, binary rewritable, PEP available). Equal-size tiles with explicit count labels are used because partition denominators are fixed at n = 5; the OIS-Binary ‘source 0/5’ tile is the only structural gap in the benchmark. retained or removed from the union; tools that are not applicable to a given artifact class are recorded in the per-alert trace with an explicit not-applicable reason rather than silently dropped. The per-alert trace contains 69 raw alert rows and 6 explicit not-applicable rows — 75 data rows in total — so that categorical tool inapplicability is distinguishable from genuine zero-alert outcomes. The vanilla-SE row aggregates KLEE and angr under their default settings on the subset where each tool admits the artifact (KLEE for IR-liftable cases, angr for stripped binaries); reported metrics are the per-tool best on each case, deduplicated by candidate. The PLCverif/CBMC row reports each tool only where it is applicable: PLCverif on the OIS-ICS partition where IEC 61131-3 ST is available, and CBMC on the OIS-ICS subset where C is generated via MATIEC. The “-style” / “-inspired” baselines (ICSQuartz, VetPLC, VulShield) are faithful re-implementations on the same SSCKG substrate, calibrated to match the original tools’ published per-case behaviour on shared cases to within 5%. Table 6: Baseline systems and their applicability on OIS-RemedBench. The “Role” column gives the comparison purpose; the per-baseline applicability rate is the fraction of the n = 15 benchmark cases for which the baseline produces any non-trivial output (see Section 4.2 for the deduplicated alert-union and the per-tool-on-each-case accounting rules). Baseline
App. rate
Role
Static analysis (CodeQL, Joern, KARONTE, SaTC, ICSQuartz; dedup. union) Vanilla SE (KLEE + angr; no S-model) SymPLC / STAutoTester DSE [27, 28] ICSQuartz-style scan-cycle fuzzing [29] VetPLC-inspired temporal event seq. [26] VulShield-style policy gen. [10] SAN2PATCH [15] VulRepair [13] CrashRepair [11]
100% (15/15)
Alert-generation upper bound
40% (6/15) 33% (OIS-ICS) 33% (OIS-ICS) 33% (OIS-ICS) 73% (11/15) 27% (src-avail.) 27% (src-avail.) 0% (sanitizer req.) 33% (OIS-ICS)
OSVA constraint isolation Domain-aware SE baseline Dynamic testing baseline Safety-vetting baseline Tier 1 quality baseline Tier 3 LLM repair baseline Tier 3 source-AVR baseline Binary-claim AVR baseline
PLCverif / CBMC [30, 46]
16
Formal verification baseline
SCARA
A P REPRINT
Figure 6: CWE coverage across the three OIS-RemedBench partitions. Regions list the CWEs unique to a partition or shared between two or three. CWE-119 and CWE-787 appear in all three partitions; CWE-416 is OIS-Binary-only; CWE-126 is OIS-Protocol-only; OIS-ICS has no partition-unique CWE class. Circle sizes are not area-weighted.
Figure 7 visualises Table 6 as an applicability heatmap. Zero-applicability cells are hatched to mark them as categorically non-applicable rather than simply low-rate; this distinction is load-bearing for CrashRepair, which requires a sanitizer trace and therefore has 0/15 applicability on OIS-RemedBench despite operating “at the binary level” in its source venue. 4.3
Research Questions
The evaluation is organized around seven research questions that together assess SCARA’s contributions to verification quality (RQ1–RQ3), remediation coverage and quality (RQ4–RQ5), cross-partition generalization (RQ6), and analyst effort (RQ7). Figure 8 maps each question to the SCARA stage under evaluation and the primary metric family. RQ1 and RQ2 together assess whether OSVA’s operational-state constraints genuinely contribute to reachability accuracy, or whether the apparent FPR reduction is achieved by artificially increasing the UNKNOWN rate. Both FPR and FNR are reported in all RQ1 comparisons precisely because a system can achieve arbitrarily low FPR by assigning UNKNOWN to every case — a failure mode that reporting FPR alone would not expose. RQ4 uses SAT-strict cases as the denominator for remediation success rate to ensure that UNSAT-resolved false positives and UNKNOWN-advisory cases are not inadvertently counted as remediation successes. 4.4
Metrics
Verification metrics. Precision = TP/(TP + FP); Recall = TP/(TP + FN). FPR and FNR are reported explicitly and jointly throughout Section 5. Time to first SAT-strict witness is measured in wall-clock seconds. Solver queries per confirmed path is the count of Z3 check-sat invocations issued before the first S AT- STRICT verdict on a candidate. The OSVA scheduling layer is parameterised by the path beam width b, the number of top-ranked SSCKG path candidates retained for OSVA validation at each scheduling round; b is an execution-budget parameter rather than a SCARA component, with default b = 8 in the primary experiments. Recall@K is path-candidate recall: the fraction of cases in 17
SCARA
A P REPRINT
Figure 7: Baseline applicability heatmap on OIS-RemedBench (n = 15). Cells show per-partition k/n counts; tile shade encodes the applicability rate. Hatched cells indicate categorical non-applicability (e.g., CrashRepair requires a sanitizer-instrumented trace that none of the 15 cases admits). The vertical separator after the OIS-ICS column marks the boundary between per-partition columns and the ‘All’ summary column. Drank for which a ground-truth vulnerable path appears within the top-K SSCKG-ranked path candidates for that case, # " X 1 (17) 1 min ranki (p) ≤ K , Recall@K = |Drank | p∈Pi+ i∈Drank
where Pi+ is the set of ground-truth vulnerable paths for case i. Reported K ∈ {1, 3, 5, 10, 20, 50}. Remediation metrics. All remediation metrics use DSAT (S AT- STRICT confirmed cases under the seed-42 main run) as the primary denominator. Applicability rate per tier is the fraction of DSAT cases for which each tier is feasible given the artifact’s availability class. Root-cause removal rate is the fraction of remediated cases for which OSVA re-run on the post-remedy artifact returns U NSAT for the original candidate. Behavioral coverage preservation rate (BCP) is defined in Eq. (14) and accepted at threshold τcov = 0.95. New-vulnerability introduction rate (NVR) is the fraction of remediated cases in which upstream re-analysis flags at least one newly introduced high-risk entity. False-blocking rate is the fraction of benign protocol or runtime traces a Tier-1 policy blocks; a Tier-1 remedy is rejected when the false-blocking rate exceeds τblock = 5%. First-submission CVA acceptance is the fraction of CVA-accepted remediations accepted on the first synthesis attempt (∆ = ∅ at acceptance). Mean RSA-to-CVA rounds is the average count of synthesis attempts per accepted remedy at the chosen tier, bounded by the per-tier iteration budget K of Algorithm 3. Replay automation rate is the fraction of L3-labelled cases for which the harness can replay the OSVA witness without manual scripting. For the CVA-quality audit we additionally report the oracle-audit denominator DCVA-audit (n = 9 for the main run, n = 1 for the targeted rerun), reported separately from DSAT . Statistical reporting. Given n ≤ 15 across all comparisons, we follow the estimation-based reporting convention used in small-n systems studies. We report absolute differences and Cliff’s δ as the primary effect size, with 95% bootstrap confidence intervals (10 000 resamples) over benchmark cases (artifact variance) reported as the headline CI. For binary-rate metrics we additionally report Clopper–Pearson exact CIs. Where p-values are reported they are descriptive secondary quantities only; with |Dpartition | = 5 the Wilcoxon signed-rank test [47] has a p-floor of ≈ 0.0625 18
SCARA
A P REPRINT
Figure 8: Three-column flow diagram from research question to SCARA stage to primary metric family.
that prevents any post-correction p < 0.125, so we de-emphasize hypothesis testing. Multiple-comparison control, where used, is Benjamini–Hochberg FDR at q = 0.10. Algorithmic stability is characterised separately by repeating each OSVA scheduling experiment under five seeds (42–46) and reporting the seed-variance min/max alongside the artifact-variance CI. 4.5
Ablation Study Design
The ablation study isolates the contribution of each architectural decision in SCARA. Nine ablation variants are evaluated; each disables one component while holding all others constant. Table 7 maps each ablation to the component disabled and the specific architectural claim under test. Table 7: Ablation study: disabled components and tested claims. A4 disables only the closed-loop CVA→RSA feedback path (CVA still evaluates and either accepts or rejects, but no δ is returned for resynthesis); A7 disables the CVA correctness check entirely (the first RSA synthesis is accepted unchecked, with neither BCP, side-effect, nor replay validation). Ablation
Disabled component
Claim tested
Evaluated in
A1 A2 A3 A4 A5 A6 A7 A8 A9
No operational-state constraints No SSCKG path scheduling No constraint relaxation No CVA feedback loop Tier 1 only No SSCKG constraint in RSA Tier 3 No CVA correctness check No CACA ranking No SSCKG substrate
C2: OSVA constraints reduce FPR C2: semantic scheduling reduces time to first SAT Effect of relaxation on UNKNOWN rate vs. recall C4: closed-loop CVA–RSA reduces misremediation Incremental value of Tier 2 and Tier 3 C3: SSCKG spec. reduces BCP degradation C4: CVA reduces NVR and domain-inv. viol. C1: composite ranking improves Recall@K SSCKG value vs. raw CPG input
RQ1 RQ3 RQ1 RQ5 RQ4 RQ5 RQ5 RQ3 RQ1, RQ3
19
SCARA
A P REPRINT
Each ablation is evaluated on the full benchmark under identical conditions to SCARA-full. Figure 9 renders the ablation-to-agent-to-RQ mapping as an arc diagram.
Figure 9: Ablation–to–RQ arc diagram. Component brackets along the bottom group ablations by the SCARA subsystem they disable. Edge colour denotes the RQ subsection that reports the ablation result. Headline results for each ablation are integrated into the corresponding §5 subsection (e.g., A1 in §5.1, A2/A8 in §5.3). In addition to the structural ablations, we report sensitivity sweeps over α ∈ {0.0, 0.3, 0.6, 0.9, 1.0}, τp , the percandidate solver budget Ttotal , the path beam width b, and the CVA thresholds (τcov , τblock ) in §5.5. The selected α = 0.6 remains within the ±1-case stability band for both recall and Recall@10, while the extreme α = 1.0 setting introduces one false positive and reduces recall to 0.5455 — robustness evidence that the headline conclusions are not the product of cherry-picked thresholds. 4.6
Implementation Details
SCARA is implemented in Python 3.11. OSVA uses angr 9.2 [35] for binary-level analysis and KLEE 3.1 [36] compiled against LLVM 14 for OIS-ICS cases. Binary rewriting uses RetroWrite [38] for PIE ELF and E9Patch [48] for x86 PE. Tier 3 patch generation uses Qwen3-7B [49] as the runtime model; DeepSeek-V3 [50] is used offline only, before evaluation, to construct repair exemplars and prompt rubrics that Qwen3-7B consumes at inference time. No DeepSeek-V3 inference occurs during evaluation runs, and no OIS-RemedBench test case is included in the exemplar set. LLM inference is served via vLLM with a per-case Tier-3 wall-clock cap of 60 s. SSCKG path alignment uses SBERT [37]. The SMT solver is Z3 4.12 [51] with incremental mode; Ttotal = 300 s per candidate, relaxed pass Trelaxed = 150 s. Replay uses FirmAE [21] for OIS-Binary, libmodbus and OpenDNP3 harnesses for OIS-Protocol, and the OpenPLC runtime [40] for OIS-ICS. All experiments run on a single server: 24-core CPU, 128 GB RAM, one NVIDIA A6000 GPU (48 GB VRAM). Hyperparameters. All hyperparameters were fixed before test-set evaluation (τp = 0.5, α = 0.6, τcov = 0.95, τblock = 5%, Ttotal = 300 s, Trelaxed = 150 s, K = 3, b = 8) based on domain constraints, engineering feasibility, and preliminary development runs on artifacts outside OIS-RemedBench. No OIS-RemedBench test case was used for threshold selection. Sensitivity to the four primary thresholds is reported in §5.5; the headline conclusions are stable within the ranges studied.
5
Results and Analysis
The evaluation is organised around the seven research questions mapped in Figure 8. The benchmark is OISRemedBench (n = 15; OIS-Binary: 5; OIS-Protocol: 5; OIS-ICS: 5). All headline confidence intervals are 95% 20
SCARA
A P REPRINT
Figure 10: Experimental architecture diagram of SCARA implementation. bootstrap intervals over 10 000 resamples over benchmark cases (artifact variance); for binary-rate metrics we additionally report Clopper–Pearson exact CIs. Algorithmic stability is characterised separately by the seed-42–46 min–max range. Effect sizes are Cliff’s δ unless otherwise noted; p-values, where shown, are Benjamini–Hochberg-adjusted at q = 0.10 and read as descriptive secondary quantities given the small n. Evaluation denominator key. • Dall (n = 15): all OIS-RemedBench cases. • Dreach (n = 11): ground-truth reachable cases. • Dinf (n = 3): ground-truth infeasible cases. • Dunk (n = 1): ground-truth unresolved cases. • DSAT (n = 7): SCARA S AT- STRICT cases under the seed-42 main run (OIS-Binary: 2, OIS-Protocol: 1, OIS-ICS: 4); denominator for remediation-success metrics. • Drank (n = 11): path-ranking cases (the 11 reachable cases of Dreach ); Recall@K denominator. • Drerun (n = 6): targeted enriched-envelope rerun set comprising the 3 ground-truth infeasible cases, the 1 U NKNOWN case, and the 2 S AT- RELAXED cases. • DPLC (n = 5): OIS-ICS subset used for the RQ7 PLCverif comparison. • DVulShield (n = 11): cases with accessible Tier-1 enforcement points; Tier-1 baseline denominator. Figure 11 renders the per-case trajectory from L2 ground truth through CVA outcome to post-rerun verdict, and Figure 12 renders the headline effect-size profile. Ablation results overview. Table 9 consolidates the per-partition headline metric for each of the nine ablation variants; the per-RQ subsections below cite the rows individually. 5.1
RQ1 — Verification Precision and False-Positive Reduction
The 15 L2-labelled cases of Dall comprise 11 ground-truth reachable cases (Dreach ), 3 ground-truth infeasible cases (Dinf ), and 1 ground-truth unresolved case (Dunk ). On the seed-42 main run, SCARA’s OSVA stage achieved precision = 100.0% (Clopper–Pearson 95% CI [59.0%, 100.0%]) and recall = 63.6% (7/11; Clopper–Pearson 95% CI [30.8%, 89.1%]), corresponding to FPR = 0.0% with respect to the encoded constraint envelope C and FNR = 36.4%. Against the static-analysis union baseline (CodeQL, Joern, KARONTE, SaTC, ICSQuartz; deduplicated by SSCKG entity), OSVA 21
SCARA
A P REPRINT
Figure 11: Per-case outcome waterfall on OIS-RemedBench. Each row is one of the 15 cases, ordered by partition (OIS-Binary, OIS-Protocol, OIS-ICS); coloured cells encode (i) the L2 ground-truth verdict (REACHABLE / INFEASIBLE / UNKNOWN), (ii) the CVA outcome at the seed-42 main run, and (iii) the post-rerun verdict on Drerun . Three previously non-strict reachable cases (BIN-OPEN-002, ICS-MATIEC-001, PROT-IEC104-001) recover to S ATSTRICT after envelope enrichment, and the three ground-truth infeasible cases (BIN-VEND-001, ICS-VETPLC-001, PROT-OPENDNP3-001) remain U NSAT confirmed-TN.
Figure 12: Cliff’s δ forest plot summarising Table 8. Each row reports a per-RQ effect estimate with its 95% bootstrap CI; reference lines mark the conventional small (|δ| = 0.147), medium (|δ| = 0.33), and large (|δ| = 0.474) thresholds following the magnitude conventions of [52]. Direction-of-effect colour: blue = favourable to SCARA, red = unfavourable. Sample size n shown per row.
22
SCARA
A P REPRINT
Table 8: Per-RQ summary of SCARA against the best applicable baseline. The “Result” column reports SCARA versus baseline together with the absolute difference ∆ and its 95% CI (10 000 bootstrap resamples over the n benchmark cases). Bold Cliff’s δ indicates that the 95% CI on ∆ excludes zero. BH-adjusted p-values are descriptive only (n ≤ 15); their values are released in the supplementary package. RQ2 (per-dimension ∆FPR/∆FNR) is reported in Figure 14 and the §5.2 prose. RQ
Stage
Result (SCARA vs. baseline; ∆ [95% CI])
n
Cliff’s δ
RQ1
OSVA
15
+0.31
RQ1 RQ1 RQ3
OSVA OSVA Sched.
15 11 11
−0.75 −0.45 −0.78
RQ3
Sched.
11
+0.48
RQ4
RSA+CVA
7
+0.71
RQ4
RSA+CVA
4
+1.00
RQ5
CVA
6
+0.42
RQ5
CVA
7
+0.62
RQ5
CVA
6
−0.18
RQ6
Full
5
—
RQ6
Full
5
—
RQ7
Full
Precision: 100.0% vs. 84.6% (static union); +15.4pp [+1.2, +30.8] FPR: 0.0% vs. 50.0% (static union); −50.0pp [−83.3, −16.7] FNR: 36.4% vs. 62.5% (vanilla SE); −26.1pp [−58.0, +5.8] Median time-to-S AT- STRICT: 56.4 s vs. 140.9 s (random); −84.5 s [−118.0, −51.0], 2.5× Recall@10: 85.0% vs. 60.0% (random); +25.0pp [+5.5, +44.5] Remed. success on DSAT : 85.7% (6/7) vs. 42.9% (VulShield T1); +42.8pp [+6.5, +78.6] T3 conditional success: 100% (2/2) vs. 0% (0/3 SAN2PATCH); +100pp [+16, +100] Root-cause removal: 66.7% (4/6) vs. 45.5% (A4); +21.2pp [−15.4, +57.4] Mean BCP on DSAT : 93.3% vs. 88.2% (A4); +5.1pp [+2.0, +8.0] New-vuln. introduction: 16.7% (1/6) vs. 22.2% (A7); −5.5pp [−30.0, +18.9] OIS-Binary precision: 100.0% (Clopper–Pearson [56.6%, 100%]) OIS-ICS remed. success (all tiers): 100.0% (Clopper–Pearson [56.6%, 100%]) Verified-and-remediated cases/analyst-hr: 0.413 vs. 0.035 (PLCverif); +0.378 [+0.21, +0.55]
5
+1.00
Table 9: Ablation results on OIS-RemedBench, grouped by SCARA component family. (a) OSVA constraint ablations — FPR / FNR (per partition) OIS-Binary
OIS-Protocol
OIS-ICS
Variant
FPR
FNR
FPR
FNR
FPR
FNR
A1 A3 A9
0.00 0.00 0.00
0.50 0.50 0.25
0.50 0.00 0.00
0.67 0.67 0.33
0.00 0.00 0.00
0.00 0.25 0.50
(b) Remediation ablations — Remed. success / BCP OIS-Binary
OIS-Protocol
OIS-ICS
Variant
R.S.
BCP
R.S.
BCP
R.S.
BCP
A5 A6
0.33 —
— 0.78
0.50 —
— 0.77
0.67 —
— 0.80
(c) CVA ablations — NVR / BCP OIS-Binary
OIS-Protocol
OIS-ICS
Variant
NVR
BCP
NVR
BCP
NVR
BCP
A4 A7
0.00 0.00
0.89 —
0.00 0.00
0.85 —
0.00 0.50
0.89 —
23
SCARA
A P REPRINT
Figure 13: FPR and FNR by partition for SCARA (reconciled after-rerun rates), the deduplicated static-analysis union, and the vanilla symbolic-execution baseline (KLEE + angr without operational-state constraints).
reduces FPR by 50.0pp (Cliff’s δ = −0.75, 95% CI on ∆FPR [−83.3, −16.7]pp). Of the seven cases that received an OSVA U NSAT verdict on the main run, three correspond to ground-truth infeasible artefacts in Dinf (BIN-VEND-001 on Cruntime ; PROT-OPENDNP3-001 on Cproto ; ICS-VETPLC-001 on Cio ) and four are correctly refuted alerts within reachable cases. The single U NKNOWN case (PROT-IEC104-001) and the two S AT- RELAXED cases (BIN-OPEN-002, ICS-MATIEC-001) are conservative outcomes rather than false negatives; they recover to S AT- STRICT after targeted envelope enrichment (§5.2). Against the vanilla symbolic execution baseline (KLEE on IR-liftable cases, angr on stripped binaries), SCARA achieves substantially higher recall: FNR of 36.4% is 26.1pp lower than vanilla SE’s 62.5% (Cliff’s δ = −0.45). Vanilla SE’s UNSAT rate of 70.0% substantially exceeds SCARA’s 46.7% (7/15), indicating that unconstrained symbolic execution over-refutes vulnerability candidates by exhausting path budgets without operational-state guidance. OIS-Binary’s 20.0% U NKNOWN rate reflects Cenv documentation gaps, OIS-Protocol’s high UNSAT rate reflects the strength of Cproto FSM constraints, and OIS-ICS achieves perfect precision and recall on the main run; the targeted rerun of §5.2 confirms these as conservative outcomes rather than false negatives. Under the primary reachable-case denominator Dreachable = 11, targeted enrichment improves recall from 7/11 to 9/11 (+18.2pp) without changing FPR. Under strict SAT-only accounting the improvement is +9.1pp, because one S AT- RELAXED case was already counted as reachable; under the expanded denominator that includes the U NKNOWN-toS AT- STRICT recovery (PROT-IEC104-001), the improvement is +25.0pp on Dexpanded = 12. We report the +18.2pp figure as the primary value and keep the other two as denominator-sensitivity checks. Figure 13 renders the partition-level FPR and FNR comparison against the static-union and vanilla-SE baselines. Soundness boundary. The 0.0% FPR figure is with respect to the encoded constraint envelope C, in line with Proposition 1’s assumption clause. The targeted envelope-enrichment rerun on Drerun (3 U NSAT + 1 U NKNOWN + 2 S AT- RELAXED) confirms that the three U NSAT verdicts on Dinf remain U NSAT under enrichment: SCARA’s specificity is preserved when the constraint envelope is widened. 5.2
RQ2 — State Dimension Contribution Analysis
Figure 14 presents the per-dimension contribution as a two-panel heatmap; cell labels carry the percentage-point delta and the underlying (±k/n) count, and the full numeric source values are released in the supplementary package. The post-rerun recovery story is reported under three accounting views: two recoveries improve recall under Dreachable = 11, one strict-label upgrade (ICS-MATIEC-001) affects only the strict SAT-only view, and the U NKNOWN-to-S AT- STRICT recovery is reported only under the expanded denominator. Targeted envelope enrichment on Drerun recovered three previously non-strict reachable cases without introducing new false positives (PROT-IEC104-001 on Cproto ; BIN-OPEN-002 on Cenv ; ICS-MATIEC-001 on Cruntime ); the three ground-truth infeasible cases of Dinf remained U NSAT under the same enrichment. 24
SCARA
A P REPRINT
Figure 14: Per-dimension contribution heatmap. Left panel: ∆FPR when each constraint family is removed; right panel: ∆FNR. Positive ∆FPR (red) indicates the dimension is critical for specificity; negative ∆FNR (blue) indicates the dimension is critical for recall. Column headers carry the per-partition nFP and nFN denominators. White cells indicate no measurable contribution at the ±20pp resolution of n = 5.
The results confirm domain-specificity: Cruntime is the dominant FPR filter for OIS-Binary, Cproto for OIS-Protocol, and Cio /Ccomponent for OIS-ICS, each contributing ≥ +50pp |∆FPR| when removed. The matched global ablation A1 (Table 9) confirms the upper-bound interpretation: removing every Cx family simultaneously introduces a false positive on OIS-Protocol (FPR = 0.50 vs. 0.00 for SCARA-full). The ceiling-saturation pattern (multiple cells at +100pp, the n = 5 maximum) reflects that each partition’s false-positive elimination rests on a small number of decisive constraint families; this answers RQ2 affirmatively for the ≥ 20pp threshold on every partition. 5.3
RQ3 — SSCKG-Guided Scheduling Efficiency
SSCKG-guided path prioritisation reduced the median time to first S AT- STRICT witness from 140.9 s (random CFG ordering, ablation A2) to 56.4 s — a 2.5× reduction (median over Drank = 11 cases per seed, aggregated over seeds 42–46; seed-variance min–max [49.0, 63.5] s). Against static risk-score ranking alone (ablation A8), median time-to-confirmation fell from 123.8 s to 56.4 s (2.2× reduction). Figure 15 renders the Recall@K curve over Drank = 11 for K ∈ {1, 3, 5, 10, 20, 50} on a log axis. The denominator throughout is |Drank | = 11 path-ranking cases, distinct from the seed-42 DSAT remediation denominator. At the headline operating point K = 10, SSCKG-guided scheduling achieves Recall@10 = 85% against 55% (static-risk, A8) and 60% (random, A2). Figure 16 renders the underlying time-to-S AT- STRICT distribution across the three strategies as box-plus-strip plots over the seed-level scheduling trace. SSCKG-guided is evaluated over 55 = 11 cases × 5 seeds observations (median 46.8 s, no timeouts, Recall@10 = 0.85); static-risk and random each use 11 seed-42 observations (median 98.2 s and 99.1 s, 1 timeout each, Recall@10 = 0.55 and 0.60). Timeout observations are rendered as censored upward-triangle markers at the budget ceiling rather than silently omitted. SSCKG-guided scheduling improves Recall@10 by 30pp over static-risk ranking and 25pp over random ordering, and reaches Recall@50 = 100% — consistent with the design intent that SSCKG guidance is path prioritisation rather than pruning. The recall difference between SSCKG-guided and unconstrained exploration converges to within ±9pp at K = 50 (95% bootstrap CI on the difference [−9, +9]pp), supporting the equivalence claim that scheduling does not sacrifice recall when the budget is large. 5.4
RQ4 — Remediation Applicability and Conditional Success
SCARA achieved a remediation success rate of 85.7% (6 of 7 cases in DSAT received CVA-issued conditional correctness evidence; Clopper–Pearson 95% CI [42.1%, 99.6%]). The tier distribution over DSAT is 1 / 4 / 2 cases for Tier 1 / Tier 2 / Tier 3 respectively; among the 6 CVA-accepted remediations the distribution is 1 / 3 / 2. Figure 17 shows the 25
SCARA
A P REPRINT
Figure 15: Recall@K on Drank = 11 for the three scheduling strategies; K is on a log axis. SSCKG-guided ranking dominates static-risk and random for every K < 50 and reaches Recall@50 = 1.0, supporting the design intent that SSCKG guidance is path prioritisation rather than pruning.
Figure 16: Time-to-first-S AT- STRICT-witness distribution on Drank . Boxes show median/IQR; overlaid dots are per-caseper-seed measurements with horizontal jitter; red triangles mark censored timeouts at the budget ceiling. SSCKG-guided (n = 55, 0 timeouts) sits well below static-risk and random (n = 11 each, 1 timeout each at seed 42).
26
SCARA
A P REPRINT
per-partition tier mix (left panel) and the per-tier conditional success rate before and after the targeted Tier-2 rerun (right panel); the ‘T2 recovered’ segment in OIS-Binary captures the BIN-CISA-002 recovery described below.
Figure 17: Tier distribution and per-tier remediation success on DSAT . (a) Accepted remedy tier per partition; the lighter ‘T2 recovered’ segment marks the BIN-CISA-002 OIS-Binary case accepted at attempt 3 of the targeted Tier-2 rerun. (b) Conditional success rate per tier, before and after the rerun; Wilson 95% intervals are shown for the after-rerun bars and are wide at n ∈ {1, 2}. The lower bound on this remediation-success rate is set by ablation A5 (Tier 1 only; Table 9), under which SCARA is forced to attempt only protocol/configuration mitigation. Removing access to Tier 2 and Tier 3 drops the per-partition remediation success rate to 0.33 (OIS-Binary) / 0.50 (OIS-Protocol) / 0.67 (OIS-ICS), confirming that the two upper tiers together contribute the bulk of the 88.9% headline value. The single R EMEDIATION -FAILED case is BIN-CISA-002 (CWE-125, Tier-2 binary hardening). The seed-42 main run exhausted all three CVA–RSA iterations because the initial guard overblocked an adjacent read/write region (BCP below τcov = 0.95). A targeted Tier-2 rerun with a 512-byte budget and a +0x10 guard offset (minimal-gate + E9Patch placement) was accepted at attempt 3 with BCP = 0.951 and false-blocking 0.06%, with replay confirmed; we therefore characterise this failure as search-budget/placement-limited rather than as evidence against Tier-2 hardening as a class. Against SAN2PATCH (applicable to 4 OIS-ICS source-available cases), SAN2PATCH produced candidate patches for 3 of 4 cases; none passed CVA validation (Clopper–Pearson 95% CI on the 0/3 success rate [0%, 70.8%]). All three rejections shared the same failure mode: the SAN2PATCH patch removed the vulnerability path but simultaneously removed reachable non-vulnerable SSCKG entities, dropping BCP below τcov = 0.95. Figure 18 renders the per-case BCP comparison; we caution that this pattern is observed on three cases only, but the consistency of the BCP-failure mechanism is the kind of misremediation that SCARA’s SSCKG-constrained RSA avoids by design. 5.5
RQ5 — CVA Validation Quality
CVA validation quality is assessed on DSAT (n = 7). In ablation A4 (CVA feedback loop disabled — CVA still evaluates and either accepts or rejects, but no rejection constraint δ is returned to RSA), the observed Tier-2 overblocking rate across DSAT was 80.0% versus 25.0% with the feedback path enabled; observed domain-invariant compliance fell from 83.3% to 60.0%; and only 45.5% of cases met the behavioural standards for ε(v, R). In ablation A7 (CVA correctness check entirely disabled — BCP, side-effect, and replay all skipped, so RSA’s first synthesis is accepted unchecked), the accepted-remediation pool exhibited 22.2% NVR, 50.0% Tier-1 false-blocking, and 50.0% Tier-2 overblocking. We report these as observations within the respective ablations rather than as population-level counterfactuals. Per-partition replay-automation rates are reported in Table 10; replay automation, rather than solver verification, is the limiting factor for stronger conditional-correctness claims on the OIS-ICS partition. The CVA stage’s quality profile on DSAT : mean BCP = 93.3% across all 7 cases (the figure is dragged below 0.95 by the single CVA-rejected case BIN-CISA-002, which had BCP ≈ 0.82 on the seed-42 main run); among the 6 CVA-accepted remediations, every case satisfied BCP ≥ τcov = 0.95, with mean accepted-case BCP = 95.2%. NVR is 16.7% (1 of 6 accepted cases). Root-cause removal rate is 66.7% (4 of 6 accepted cases); the remaining 2 include one 27
SCARA
A P REPRINT
Figure 18: SAN2PATCH vs SCARA behavioural coverage preservation on the SAN2PATCH-applicable OIS-ICS cases. SAN2PATCH (grey) falls below the τcov = 0.95 acceptance threshold on every shared case. Paired SCARA bars show pre-rerun (light) and post-rerun (dark) BCP; for ICS-MATIEC-001 and ICS-QUARTZ-001 the post-rerun value crosses τcov (red-outlined post bar, ↑ annotation), bringing both into the CVA-accepted pool. BIN-CISA-002 is reported separately as the seed-42 main-run Tier-2 failure recovered by the targeted Tier-2 rerun and is described in §5.4. OIS-ICS case in which the remedy relocated rather than eliminated the vulnerability root cause — a residual-risk pattern that BCP and side-effect checks alone do not detect, and which we revisit as a Threats-to-Validity item in Section 7.3. CVA quality under a full-CVA oracle. Figure 19 reports SCARA-full and the relevant ablations / baseline re-scored by a common full-CVA oracle (DCVA-audit = 9 for the main-run variants and n = 4 for SAN2PATCH). Under oracle evaluation, A4 (no CVA feedback) collapses on BCP pass rate to 44.4% and on replay confirmation to 0%; A7 (no CVA correctness check) preserves BCP self-reported pass rate at 100% (since it skips the check) but its replayconfirmation and CVA-acceptance rates collapse to 0%; SAN2PATCH fails BCP entirely. Only SCARA-full achieves a non-zero CVA-acceptance rate (88.9% on DCVA-audit , rising to 100% on the targeted-rerun row). The direct C3-isolation comparator is ablation A6 (no SSCKG constraint in RSA Tier 3; Table 9): BCP drops to 0.78 / 0.77 / 0.80 across the three partitions, all below the acceptance threshold τcov = 0.95. A6 thus quantifies the degradation that the SSCKG behavioural specification prevents and supports contribution C3 as a standalone claim, distinct from the CVA-stage contributions tested by A4 and A7. Hyperparameter sensitivity. Figure 20 reports the sensitivity sweep across τp , Ttotal , α, and the joint CVA pair (τcov , τblock ). The default operating point sits at or near the recall/CVA-acceptance knee on every axis, and headline conclusions are stable to within ±1 case across every sweep range except the extreme τcov = 0.98 corner. 5.6
RQ6 — Cross-Partition Generalization
100% precision is preserved across all three partitions (Figure 13); recall varies from 33.3% (OIS-Protocol) to 100.0% (OIS-ICS), tracking the per-dimension documentation gaps in Cenv and Cproto identified in §5.2. The OIS-Binary remediation-success shortfall (50.0% vs 100% in the other two partitions) is attributable to the single BIN-CISA-002 case discussed in §5.4 and is search-budget-limited rather than tier-incompatible: the supplementary Tier-2 rerun accepts the case at attempt 3. 5.7
RQ7 — Manual Modeling and Replay Burden
RQ7 is evaluated on DPLC , the full OIS-ICS partition of OIS-RemedBench (n = 5). For each case we record PLCverif property-authoring, model-construction, and debugging effort, and compare against SCARA’s operational-context review effort. Table 11 reports the per-case measurements; the partition-level summary follows. On DPLC , PLCverif required a mean of 17.04 analyst-hours per case (median 17.20) versus 2.42 for SCARA (median 2.50). PLCverif verified 3 of 5 cases within its model-checking budget and timed out on 2; SCARA reached a terminal verdict on all 5 cases. The corresponding throughput statistics are 0.035 verified cases per analyst-hour for PLCverif 28
SCARA
A P REPRINT
Figure 19: CVA quality on DCVA-audit , with all four variants re-scored under the same full-CVA oracle. Bars are per-variant rates for root-cause removed, BCP ≥ τcov , no-new-vulnerability (NVR), replay confirmation, and final CVA acceptance. Variants that disable a CVA component score 0% on the dependent components, supporting the §3.5 argument that each component is load-bearing.
Figure 20: Hyperparameter sensitivity grid. Top: τp (path-priority temperature) and Ttotal (solver budget). Bottom-left: α (CACA ranking weight) — both recall and Recall@10 peak at α = 0.6 and stay flat to α = 0.9 before degrading at α = 1.0. Bottom-right: joint (τcov , τblock ) sweep with the operating point at (0.95, 0.05). The dashed vertical line in each panel marks the default operating point.
29
SCARA
A P REPRINT
Table 10: Full per-partition SCARA results on OIS-RemedBench (n = 5 per partition), grouped into four blocks: verification outcome, label-class mix, remediation tier and quality, and operational diagnostics. Tier mix is reported as T1 / T2 / T3 fractions of remediated cases. Metric
OIS-Binary
OIS-Protocol
OIS-ICS
Verification TP / FP / TN / FN (counts) Precision / FPR Recall / FNR UNKNOWN rate
2/0/1/2 100.0% / 0.0% 50.0% / 50.0% 20.0%
1/0/1/2 100.0% / 0.0% 33.3% / 66.7% 20.0%
4/0/1/0 100.0% / 0.0% 100.0% / 0.0% 0.0%
Label-class mix S AT- STRICT rate U NSAT rate
40.0% (n = 2) 40.0%
20.0% (n = 1) 60.0%
80.0% (n = 4) 20.0%
Remediation Remed. success (over S AT- STRICT) Tier mix (T1 / T2 / T3) First-submission CVA accept. Mean RSA-to-CVA rounds
50.0% 0 / 100 / 0% 50.0% 1.0
100.0% 0 / 0 / 100% 100.0% 2.0
100.0% 25 / 50 / 25% 100.0% 2.75
Diagnostics Median time-to-S AT- STRICT (s) Solver queries per confirmed path Replay automation rate
49.2 402 100.0%
44.3 354 100.0%
61.5 523 50.0%
Table 11: Per-case analyst burden on DPLC (n = 5). PLCverif effort is dominated by LTL/PLTL property authoring; SCARA effort is dominated by reviewing the SSCKG-derived S prior estimate against documentation. V = verified; T = timeout; V-I NF = verified-infeasible; S AT-R EM = S AT- STRICT-then-remediated; U NSAT-R ES = U NSAT- RESOLVED. Case
PLCverif(h)
SCARA(h)
PLCverif
SCARA
ICS-OPENPLC-001 ICS-MATIEC-001 ICS-QUARTZ-001 ICS-VETPLC-001 ICS-INJECT-001
13.5 19.8 17.2 11.2 21.0
2.2 2.8 2.5 2.0 2.6
V T V V-I NF T
S AT-R EM S AT-R EM S AT-R EM U NSAT-R ES S AT-R EM
Mean
17.04
2.42
—
—
and 0.413 verified-and-remediated cases per analyst-hour for SCARA, an absolute difference of +0.378 (95% bootstrap CI [+0.21, +0.55] over the 5 cases). Recall-within-budget is 0.60 for PLCverif and 1.00 for SCARA. We caution that this comparison measures person-hours per task-completion without normalising for the rarity of the LTL/PLTL property-authoring skill; the practical analyst-pool difference is therefore likely larger than the throughput ratio alone suggests. PLCverif provides formal proofs of property satisfaction for cases within its model-checking budget — a stronger guarantee than SCARA’s conditional evidence on the verified subset; SCARA does not claim to match this guarantee level. The contribution of RQ7 is to bound the manual-effort cost of obtaining the stronger PLCverif guarantee on this partition.
6
Related Work and Positioning
6.1
Automated Vulnerability Repair
Family A — Neural and LLM-based patch generation. VRepair [12] introduced transfer learning from general bug-fix corpora to the vulnerability repair domain. VulRepair [13] employed a T5-based encoder-decoder architecture trained on CVE-linked vulnerability functions. VulMaster [14] extended this with broader repository context and CWE-aware prompt construction. More recent agentic systems: SAN2PATCH [15] drives repair through a tree-ofthought reasoning process guided by sanitizer traces; APPATCH [16] introduces adaptive prompting conditioned on vulnerability-semantic features; PatchAgent [17] constructs a repair agent with a language server and build-feedback 30
SCARA
A P REPRINT
Figure 21: Per-case analyst-hour comparison on DPLC (n = 5). X-axis: PLCverif total analyst-hours (property authoring + model construction + debugging); y-axis: SCARA operational-context review hours. Marker shape encodes the PLCverif outcome (circle = VERIFIED, triangle = TIMEOUT, diamond = VERIFIED-INFEASIBLE). The y = x and y = x/5 reference lines bracket the case-by-case throughput gap; every OIS-ICS case sits well below y = x/5.
loop; and Vul-R2 [18] applies reasoning-oriented LLM fine-tuning. All Family A systems require at minimum a compilable source fragment. Their applicability to OIS-Binary and OIS-Protocol is zero; applicability to OIS-ICS extends only to the source-available subset. Family B — Program-analysis-based repair. CrashRepair [11] employs sanitizer-guided concolic execution then applies mutation-based search over the surrounding code. CONCH [19] constructs a null-pointer dereference context graph through interprocedural source analysis. VulShield [10] translates sanitizer vulnerability reports into runtime protection policies. Among existing systems, VulShield is conceptually closest to SCARA’s Tier 1 stage, as both generate protection policies; however, VulShield derives policies from sanitizer reports of instrumented execution, whereas SCARA’s Tier 1 synthesizes equivalent policies from static SSCKG behavioral analysis. Family B systems achieve zero applicability on OIS-Binary and OIS-Protocol. Family C — Evaluation and benchmarking. APR4Vul [45] evaluated generic APR tools on Java vulnerability benchmarks, demonstrating a systematic gap between generic APR success rates and security repair success rates. ExMit [53] established that syntactic correctness is insufficient as a security repair criterion; semantic equivalence of non-vulnerable behaviors must also be verified. The 2025 USENIX SoK surveys [8, 9] identified vulnerability analysis precision and patch validation as the primary bottlenecks. Positioning. No existing AVR work addresses stripped industrial binaries. SCARA is evaluated on the domain that defines its applicability. Direct conditional performance comparison with SAN2PATCH is reported in Section 5.4 only on the OIS-ICS source-available subset, where applicability overlap exists. Table 12 presents a comparative summary across seven dimensions. 31
SCARA
A P REPRINT
Table 12: Comparison of related systems across seven dimensions. Symbols: ✓ = supported, ✗ = not supported, ∼ = partial. The upper block lists systems re-implemented or compared quantitatively in Section 5. System
No src
Reach. cert.
Remed.
Ind. constrs
Evaluated head-to-head in Section 5 VRepair [12] ✗ VulRepair [13] ✗ SAN2PATCH [15] ✗ CrashRepair [11] ✗ VulShield [10] ✗ SymPLC [27] ∼ ICSQuartz [29] ∼ PLCverif [30] ✗ SCARA (this work) ✓
✗ ✗ ✗† ✗† ✓ ✗ ✗ ✗ ✓
✗ ✗ ✗ ✗ ✗ ∼ ✗ ∼ ✓ (4-class)
T3 T3 T3 T3 T1 ✗ ✗ ✗ T1–T3
Related; positioning only APPATCH [16] PatchAgent [17] KARONTE [5] SaTC [6] Firmadyne / FirmAE VetPLC [26]
✗ ✗ ✓ ✓ ✓ ✓
✗ ✗ ✗ ✗ ✗ ✗
T3 T3 ✗ ✗ ✗ ✗
6.2
Opaque bin.
✗ ✗ ✓ ✓ ✓ ∼
OIS-RemedBench app.
Primary positioning
✗ ✗ ✗ ✗ ✗ ∼ ✓ ✓ ✓
OIS-ICS src subset OIS-ICS src subset OIS-ICS src subset 0% ≈0% OIS-ICS only OIS-ICS only ≈10% 100%
Family A LLM repair Family A LLM repair Nearest T3 baseline Family B; sanitizer req. Nearest T1 baseline SE baseline for OSVA Dynamic testing baseline Formal verif. baseline End-to-end OIS
✗ ✗ ✗ ✗ ✗ safety
OIS-ICS src subset OIS-ICS src subset 100% (upstream) 100% (upstream) OIS-Binary replay OIS-ICS only
Not evaluated Agentic repair Upstream CACA generator Upstream CACA generator Replay infrastructure Safety verif.; no remed.
Binary Analysis and Firmware Security
Firmware rehosting and emulation. Firmadyne [20], FirmAE [21], HALucinator [22], P2IM [54], Fuzzware [23], FirmSolo [24], and SAFIREFUZZ [25] address executing stripped firmware in controllable environments. FirmAE provides the replay infrastructure for independent SAT-witness validation in the OIS-Binary partition. Binary taint analysis. KARONTE [5] performs inter-binary taint tracking via identification of shared data sources across firmware components. SaTC [6] combines keyword-guided taint analysis with front-end code identification. Both tools represent important upstream generators for SCARA’s CACA stage. Vulnerability reachability analysis. Recent work on reachability analysis for third-party library vulnerabilities [55] demonstrated that determining whether a CVE is reachable from the calling application can substantially reduce false-positive rates in software composition analysis tools. SCARA extends this concept to the industrial binary domain. 6.3
ICS/PLC Verification and Testing
Safety verification and formal methods. VetPLC [26] employs temporal invariant mining from normal PLC execution traces and generates timed event sequences to detect safety violations. PLCverif [30] and its extensions perform formal model checking of PLC control programs against manually specified PLTL or LTL properties. Section 5.7 compares SCARA directly with PLCverif on the OIS-ICS formal-spec-available subset. Symbolic and dynamic-symbolic execution for PLC programs. SymPLC [27] applies symbolic execution to IEC 61131-3 structured text by translating them to C via MATIEC and analyzing with KLEE to achieve high structural coverage. STAutoTester [28] extends this with dynamic symbolic execution. These works establish the MATIEC translation approach that SCARA adopts for the OIS-ICS partition. Fuzzing for ICS software. ICSQuartz [29] introduces scan-cycle-aware fuzzing for IEC 61131-3 structured text programs. ICSFuzz [56] manipulates physical I/O signals to trigger anomalous behavior. Both are complementary to SCARA rather than competitive.
7
Discussion
7.1
Conditional Correctness Evidence via SSCKG and Independent Replay
The SSCKG serves a dual role in SCARA: as a behavioral specification guiding both repair synthesis (RSA) and correctness validation (CVA). This dual use creates a potential circularity — a system using the same knowledge base to specify and to verify a remedy could, in principle, validate incorrect remediations that happen to preserve SSCKG-level coverage while silently breaking real industrial behavior. SCARA addresses this through independent replay validation. SCARA’s CVA stage addresses the AVR community’s recurring “plausible but incorrect patch” failure mode with two complementary signals: SSCKG behavioral coverage preservation provides a domain-grounded behavioural 32
SCARA
A P REPRINT
specification without requiring a manually authored test suite, and independent replay provides an empirical check. The combination is conditional, not formal. SSCKG coverage preservation does not assert that every byte of non-vulnerable behavior is preserved. Replay confirmation does not prove that all inputs in ψvuln are blocked. These limitations are the reason SCARA issues conditional correctness evidence ε(v, Rv ) rather than a proof. 7.2
Practical Implications and Deployment Considerations
SCARA’s output is operator-actionable in three deployment modes that align with the existing OIS-asset-management workflow. (i) CVE-triage pre-filter: SCARA converts 20% (3/15) of L2 candidates to U NSAT refutation certificates at 0% FPR, removing them from the analyst queue with documented evidence; on a larger corpus this fraction is what determines the per-case analyst-hour cost shown in Figure 21. (ii) Tier-1 policy generator: for the 73% (11/15) of cases with a reachable enforcement point (Figure 5), SCARA emits a deployable Modbus-TCP / OPC-UA / IEC 60870-5-104 / firewall policy whose false-blocking rate is bounded by τblock and that is validated against benign traffic traces. (iii) Assisted Tier-2 / Tier-3 repair: for the binary-rewritable and source-available subsets, SCARA produces a candidate remedy with CVA-issued conditional correctness evidence ε(v, Rv ), ready for analyst review before deployment. Operator cost on the OIS-ICS partition is 2.42 analyst-hours per case (Section 5.7), compared with 17.04 for PLCverif on the same five cases. The framework deliberately does not target safety-critical controllers with enforced secure boot or cryptographic code-signing (cf. Section 7.3 L2), and the Tier-3 LLM channel requires offline guardrails — the prompt rubrics constructed from DeepSeek-V3 outputs and the SSCKG behavioural specification — before being placed in a production change-management flow. 7.3
Limitations
L1 — State model completeness. The S model is only as complete as available documentation and known industrial state assumptions. The targeted envelope enrichment of §5.2 reduces the UNKNOWN rate from 13.3% to 6.7% without introducing false positives, indicating that residual conservatism is tractable when additional Cx documentation is supplied. L2 — Binary rewriting feasibility. Tier 2 requires an ELF or PE binary that can be rewritten without violating secure boot, code signing, or cryptographic integrity checks. Many production ICS binaries include these protections. The OIS-Binary benchmark’s bias toward binary-rewritable firmware means that Tier 2 performance on secure-boot-enforced firmware is not evaluated. L3 — Tier 3 LLM repair quality. LLM-based Tier 3 repair inherits hallucination limitations. The SSCKG constraint check and CVA validation catch many incorrect patches, but a subtly wrong patch that passes SSCKG coverage checks may still be accepted. The NVR of 16.7% captures the most consequential form of this failure. L4 — Benchmark representativeness. The n = 15 benchmark, constrained by industrial-firmware licensing, supports estimation-based effect-size claims but cannot promote them to classical significance under any post-correction threshold; replication on a larger v0.2.0 cohort is the primary external-validity risk. L5 — OSVA scalability. The overall timeout rate was 13.3% (OIS-Binary and OIS-Protocol each 20.0%, OIS-ICS 0.0%). These cases are correctly reported as UNKNOWN rather than incorrectly classified, preserving the precision guarantee at the cost of lower recall. Increasing Ttotal or applying SSCKG-guided budget allocation more aggressively are the primary engineering levers available. 7.4
Threats to Validity
Construct. L2 reachability labels and L4 remedy labels are each assigned by two independent procedures with human-expert arbitration on disagreements; SCARA’s FPR = 0.0% across all SAT-confirmed cases indicates that no SAT verdict rests on a disputed L2 label. Baseline applicability is defined as the ability to produce any non-trivial output, restricted to the source-available subset where source is required. Internal. All experimental results derive from a verified seed-42 main run, with seeds 43–46 used to characterise algorithmic stability (min–max ranges reported in §5.3); OSVA symbolic execution is deterministic under a fixed seed. With |Dpartition | = 5 the Wilcoxon signed-rank test has a one-sided p-floor of ≈ 0.0625, so we de-emphasise hypothesis testing in favour of Cliff’s δ with bootstrap CIs and Benjamini–Hochberg control at q = 0.10. All hyperparameters were fixed prior to test-set evaluation on artifacts outside OIS-RemedBench; sensitivity to the four primary thresholds is stable to within ±1 case across the studied ranges (§5.5). External. The benchmark’s three artifact categories are bounded by the legal accessibility of CVE-linked industrial firmware, with safety-critical proprietary firmware excluded for licensing reasons. The abstract behavioural lattice A is 33
SCARA
A P REPRINT
instantiated from MITRE ATT&CK for ICS; transfer to non-ICS opaque domains requires lattice and constraint-template expansion. Tier-3 results are bounded to OpenPLC- and MATIEC-comparable artifacts under Qwen3-7B as the runtime model; under the full-CVA oracle SCARA-full’s CVA-acceptance rate is 88.9% on DCVA-audit = 9, recoverable to 100% on the targeted-rerun subset. 7.5
Future Work
Three extensions are deliberately deferred to v0.2.0. (i) The Tier-3 LLM channel currently uses Qwen3-7B as the runtime patch-generation model and DeepSeek-V3 offline for prompt and rubric construction. A controlled offlineversus-runtime role comparison — Qwen3-7B runtime only, Qwen3-7B with DeepSeek-V3-derived offline rubric support, and DeepSeek-V3 as a runtime model where licensing and inference reproducibility permit — under the same Tier-3 budget and the same full-CVA oracle would isolate the runtime-LLM contribution from the rubric-construction contribution. (ii) A benchmark expansion targeting n ≥ 50 cases with broader vendor coverage (additional firmware vendors, additional protocol implementations, and a wider CWE distribution) would convert the present effect-size estimates into population-level claims. (iii) Extension of the abstract behavioural lattice A beyond MITRE ATT&CK for ICS to non-ICS opaque domains — automotive ECUs, network appliances, embedded medical devices — would generalise the SCARA pipeline beyond industrial control. An open-competitor comparison against alternative sourceaware repair LLMs (e.g., DeepSeek-Coder) is an optional v0.2.0 extension, contingent on the same Tier-3 budget, prompt, and full-CVA oracle being applied so that the comparison remains controlled.
8
Conclusion
This work has developed SCARA, the first end-to-end framework that converts binary-only vulnerability candidates in opaque industrial software into either validated remediation artifacts or refutation certificates. In support of the five contributions stated in Section 1, we have formalised the OIS remediation problem under a nine-component operational state model (C1); designed and evaluated operational-state-aware reachability verification that eliminates 40.0% of incoming binary alerts as infeasible (C2); implemented a tier-appropriate remediation synthesiser that degrades gracefully with artifact opacity across protocol mitigation, binary hardening, and SSCKG-constrained source patch tiers (C3); introduced a closed-loop correctness validation stage that issues conditional correctness evidence ε(v, Rv ) via behavioural-coverage preservation and independent replay (C4); and released OIS-RemedBench v0.1.0, the first benchmark spanning firmware, protocol handlers, and ICS/PLC artifacts with stratified reachability and remediation labels (C5). The headline numbers — 100% precision, 88.9% post-rerun remediation success, and a 7.0× analyst-hour gain on OIS-ICS — are attributable to three distinct mechanisms rather than to the symbolic-execution engine, the patch generator, or the LLM channel individually: the operational-state envelope discharges the implicit assumptions that vanilla SE leaves unconstrained; the CVA-to-RSA δ-feedback loop converts open-loop misremediations into accepted refinements; and the tier mechanism resolves most ICS cases at Tier 1 or Tier 2, bypassing source dependency for the bulk of the workload. The evidence is conditional on the encoded operational-state envelope (L1), on Tier-2 binary-rewrite feasibility (L2), and on the Qwen3-7B Tier-3 runtime model (L3); the n = 15 benchmark supports estimation-based effect-size claims but not population-level inference. Three directions follow from these limitations: a controlled runtime-versus-offline Tier-3 LLM comparison under the full-CVA oracle to quantify L3, an OIS-RemedBench v0.2.0 expansion (n ≥ 50, broader vendor and CWE coverage) to convert the present estimates into population-level claims, and extension of the abstract behavioural lattice A beyond MITRE ATT&CK for ICS to automotive, network, and medical opaque-software domains. The framework and evaluation infrastructure are released as open artifacts (Section 8).
Data and Code Availability The SCARA framework implementation7 and the OIS-RemedBench benchmark cases (excluding artifacts subject to vendor licensing restrictions)8 are released as open artifacts at the project repositories. Cases derived from proprietary vendor firmware are documented by their CVE identifiers and inclusion criteria so that licensed researchers can reconstitute the corresponding partition; redistribution of the binaries themselves is prohibited by the originating vendor licenses. 7 8
https://github.com/Mewtwoz/SCARA-framework https://github.com/Mewtwoz/Scara-Dataset
34
SCARA
A P REPRINT
Acknowledgements This work was supported in part by the Major Science and Technology Project of Liaoning Province (grant Nos. 2025JH1/11700021 and 2024JH1/11700049), and by the Applied Basic Research Program of Liaoning Province (grant No. 2025JH2/101300012).
References [1] Executive Office of the President. Executive order 14028 of may 12, 2021: Improving the nation’s cybersecurity. Federal Register, vol. 86, no. 93, pp. 26633–26647, May 2021. URL https://www.federalregister. gov/documents/2021/05/17/2021-10460/improving-the-nations-cybersecurity. Accessed: 202501-15. [2] Keith Stouffer, Michael Pease, CheeYee Tang, Timothy Zimmerman, Victoria Pillitteri, Suzanne Lightman, Adam Hahn, Stephanie Saravia, Aslam Sherule, and Michael Thompson. NIST special publication 800-82 rev. 3: Guide to operational technology (OT) security. NIST Special Publication 800-82 Rev. 3, National Institute of Standards and Technology, September 2023. URL https://csrc.nist.gov/pubs/sp/800/82/r3/final. [3] International Electrotechnical Commission. IEC 62443-4-1:2018: Security for industrial automation and control systems — part 4-1: Secure product development lifecycle requirements, 2018. URL https://webstore.iec. ch/en/publication/33615. International standard, Edition 1.0. [4] Yuede Ji, Lei Cui, and H. Howie Huang. BugGraph: Differentiating source-binary code similarity with graph triplet-loss network. In Proceedings of the 2021 ACM Asia Conference on Computer and Communications Security, pages 702–715. ACM, 2021. doi:10.1145/3433210.3437533. [5] Nilo Redini, Aravind Machiry, Ruoyu Wang, Chad Spensky, Andrea Continella, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. KARONTE: Detecting insecure multi-binary interactions in embedded firmware. In Proceedings of the 2020 IEEE Symposium on Security and Privacy, pages 1544–1561. IEEE, 2020. doi:10.1109/SP40000.2020.00036. [6] Libo Chen, Yanhao Wang, Quanpu Cai, Yunfan Zhan, Hong Hu, Jiaqi Linghu, Qinsheng Hou, Chao Zhang, Haixin Duan, and Zhi Xue. Sharing more and checking less: Leveraging common input keywords to detect bugs in embedded systems. In Proceedings of the 30th USENIX Security Symposium, pages 303–319. USENIX Association, 2021. URL https://www.usenix.org/conference/usenixsecurity21/presentation/chen-libo. [7] Bowei Ning, Xuejun Zong, Lian Lian, Kan He, Yifei Sun, Yuxiang Lei, and Plamen Vasilev. Securing the dark matter: A semantic-enhanced neuro-symbolic framework for supply chain analysis of opaque industrial software, 2026. URL https://arxiv.org/abs/2605.07737. [8] Yiwei Hu, Zhen Li, Kedie Shu, Shenghua Guan, Deqing Zou, Shouhuai Xu, Bin Yuan, and Hai Jin. SoK: Automated vulnerability repair: Methods, tools, and assessments. In Proceedings of the 34th USENIX Security Symposium, pages 4421–4440. USENIX Association, 2025. URL https://www.usenix.org/conference/ usenixsecurity25/presentation/hu-yiwei. [9] Ying Li, Faysal Hossain Shezan, Bomin Wei, Gang Wang, and Yuan Tian. SoK: Towards effective automated vulnerability repair. In Proceedings of the 34th USENIX Security Symposium, pages 4441–4462. USENIX Association, 2025. URL https://www.usenix.org/conference/usenixsecurity25/presentation/li-ying. [10] Yuan Li, Chao Zhang, Jinhao Zhu, Penghui Li, Chenyang Li, Songtao Yang, and Wende Tan. VulShield: Protecting vulnerable code before deploying patches. In Proceedings of the Network and Distributed System Security Symposium. Internet Society, 2025. doi:10.14722/ndss.2025.240298. URL https://www.ndss-symposium. org/ndss-paper/vulshield-protecting-vulnerable-code-before-deploying-patches/. [11] Ridwan Shariffdeen, Christopher S. Timperley, Yannic Noller, Claire Le Goues, and Abhik Roychoudhury. Vulnerability repair via concolic execution and code mutations. ACM Transactions on Software Engineering and Methodology, 2025. doi:10.1145/3707454. [12] Zimin Chen, Steve Kommrusch, and Martin Monperrus. Neural transfer learning for repairing security vulnerabilities in C code. IEEE Transactions on Software Engineering, 49(1):147–165, 2023. doi:10.1109/TSE.2022.3147265. [13] Michael Fu, Chakkrit Tantithamthavorn, Trung Le, Van Nguyen, and Dinh Phung. VulRepair: A T5-based automated software vulnerability repair. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 935–947. ACM, 2022. doi:10.1145/3540250.3549098. 35
SCARA
A P REPRINT
[14] Xin Zhou, Kisub Kim, Bowen Xu, DongGyun Han, and David Lo. Out of sight, out of mind: Better automatic vulnerability repair by broadening input ranges and sources. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering. ACM, 2024. doi:10.1145/3597503.3639222. [15] Youngjoon Kim, Sunguk Shin, Hyoungshick Kim, and Jiwon Yoon. Logs in, patches out: Automated vulnerability repair via tree-of-thought LLM analysis. In Proceedings of the 34th USENIX Security Symposium, pages 4401– 4419. USENIX Association, 2025. URL https://www.usenix.org/conference/usenixsecurity25/ presentation/kim-youngjoon. [16] Yu Nong, Haoran Yang, Long Cheng, Hongxin Hu, and Haipeng Cai. APPATCH: Automated adaptive prompting large language models for real-world software vulnerability patching. In Proceedings of the 34th USENIX Security Symposium, pages 4481–4500. USENIX Association, 2025. URL https://www.usenix.org/conference/ usenixsecurity25/presentation/nong. [17] Zheng Yu, Ziyi Guo, Yuhang Wu, Jiahao Yu, Meng Xu, Dongliang Mu, Yan Chen, and Xinyu Xing. PATCHAGENT: A practical program repair agent mimicking human expertise. In Proceedings of the 34th USENIX Security Symposium, pages 4381–4400. USENIX Association, 2025. URL https://www.usenix.org/conference/ usenixsecurity25/presentation/yu-zheng. [18] Xin-Cheng Wen, Zirui Lin, Yijun Yang, Cuiyun Gao, and Deheng Ye. Vul-R2: A reasoning LLM for automated vulnerability repair. In Proceedings of the 40th IEEE/ACM International Conference on Automated Software Engineering, pages 26–38. IEEE, 2025. doi:10.1109/ASE63991.2025.00011. [19] Yunlong Xing, Shu Wang, Shiyu Sun, Xu He, Kun Sun, and Qi Li. What IF is not enough? fixing null pointer dereference with contextual check. In Proceedings of the 33rd USENIX Security Symposium, pages 1367– 1382. USENIX Association, 2024. URL https://www.usenix.org/conference/usenixsecurity24/ presentation/xing. [20] Daming D. Chen, Manuel Egele, Maverick Woo, and Maverick Brumley. Towards automated dynamic analysis for Linux-based embedded firmware. In Proceedings of the Network and Distributed System Security Symposium. Internet Society, 2016. doi:10.14722/ndss.2016.23415. URL https://www.ndss-symposium.org/wp-content/ uploads/2017/09/towards-automated-dynamic-analysis-linux-based-embedded-firmware.pdf. [21] Mingeun Kim, Dongkwan Kim, Eunsoo Kim, Suryeon Kim, Yeongjin Jang, and Yongdae Kim. FirmAE: Towards large-scale emulation of IoT firmware for dynamic analysis. In Proceedings of the 36th Annual Computer Security Applications Conference, pages 733–745. ACM, 2020. doi:10.1145/3427228.3427294. [22] Abraham A. Clements, Eric Gustafson, Tobias Scharnowski, Paul Grosen, David Fritz, Christopher Kruegel, Giovanni Vigna, Saurabh Bagchi, and Mathias Payer. HALucinator: Firmware re-hosting through abstraction layer emulation. In Proceedings of the 29th USENIX Security Symposium, pages 1201–1218. USENIX Association, 2020. URL https://www.usenix.org/conference/usenixsecurity20/presentation/clements. [23] Tobias Scharnowski, Nils Bars, Moritz Schloegel, Eric Gustafson, Marius Muench, Giovanni Vigna, Christopher Kruegel, Thorsten Holz, and Ali Abbasi. Fuzzware: Using precise MMIO modeling for effective firmware fuzzing. In Proceedings of the 31st USENIX Security Symposium, pages 1239–1256. USENIX Association, 2022. URL https://www.usenix.org/conference/usenixsecurity22/presentation/scharnowski. [24] Ioannis Angelakopoulos, Gianluca Stringhini, and Manuel Egele. FirmSolo: Enabling dynamic analysis of binary Linux-based IoT kernel modules. In Proceedings of the 32nd USENIX Security Symposium, pages 5021– 5038. USENIX Association, 2023. URL https://www.usenix.org/conference/usenixsecurity23/ presentation/angelakopoulos. [25] Lukas Seidel, Dominik Christian Maier, and Marius Muench. Forming faster firmware fuzzers. In Proceedings of the 32nd USENIX Security Symposium, pages 2903–2920. USENIX Association, 2023. URL https://www. usenix.org/conference/usenixsecurity23/presentation/seidel. [26] Mu Zhang, Chien-Ying Chen, Bin-Chou Kao, Yassine Qamsane, Yuru Shao, Yikai Lin, Elaine Shi, Sibin Mohan, Kira Barton, James R. Moyne, and Z. Morley Mao. Towards automated safety vetting of PLC code in real-world plants. In Proceedings of the 2019 IEEE Symposium on Security and Privacy, pages 522–538. IEEE, 2019. doi:10.1109/SP.2019.00034. [27] Shengjian Guo, Meng Wu, and Chao Wang. Symbolic execution of programmable logic controller code. In Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pages 326–336. ACM, 2017. doi:10.1145/3106237.3106245. [28] Weigang He, Jianqi Shi, Ting Su, Zeyu Lu, Li Hao, and Yanhong Huang. Automated test generation for IEC 61131-3 ST programs via dynamic symbolic execution. Science of Computer Programming, 206:102608, 2021. doi:10.1016/j.scico.2021.102608. 36
SCARA
A P REPRINT
[29] Corban Villa, Constantine Doumanidis, Hithem Lamri, Prashant Hari Narayan Rajput, and Michail Maniatakos. ICSQuartz: Scan cycle-aware and vendor-agnostic fuzzing for industrial control systems. In Proceedings of the Network and Distributed System Security Symposium. Internet Society, 2025. doi:10.14722/ndss.2025.240795. [30] Dániel Darvas, Enrique Blanco Viñuela, and Borja Fernández Adiego. PLCverif: A tool to verify PLC programs based on model checking techniques. In Proceedings of the 15th International Conference on Accelerator and Large Experimental Physics Control Systems, pages 911–914. JACoW Publishing, 2015. doi:10.18429/JACoWICALEPCS2015-WEPGF092. URL https://jacow.org/ICALEPCS2015/papers/WEPGF092.pdf. [31] Mário de Sousa and Adriano Carvalho. An iec 61131-3 compiler for the matplc. In EFTA 2003. 2003 IEEE Conference on Emerging Technologies and Factory Automation. Proceedings (Cat. No. 03TH8696), volume 1, pages 485–490. IEEE, 2003. [32] Fabian Yamaguchi, Nico Golde, Daniel Arp, and Konrad Rieck. Modeling and discovering vulnerabilities with code property graphs. In Proceedings of the 2014 IEEE Symposium on Security and Privacy, pages 590–604. IEEE, 2014. doi:10.1109/SP.2014.44. [33] MITRE Corporation. MITRE ATT&CK for industrial control systems: ICS matrix, 2024. URL https://attack. mitre.org/matrices/ics/. Accessed: 2025-01-15. [34] National Institute of Standards and Technology. National vulnerability database (NVD), 2024. URL https: //nvd.nist.gov/. [35] Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kruegel, and Giovanni Vigna. SoK: (state of) the art of war: Offensive techniques in binary analysis. In Proceedings of the 2016 IEEE Symposium on Security and Privacy, pages 138–157. IEEE, 2016. doi:10.1109/SP.2016.17. [36] Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: Unassisted and automatic generation of highcoverage tests for complex systems programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, pages 209–224. USENIX Association, 2008. URL https://www.usenix. org/legacy/event/osdi08/tech/full_papers/cadar/cadar.pdf. [37] Nils Reimers and Iryna Gurevych. Sentence-BERT: Sentence embeddings using Siamese BERT-networks. In Proceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing, pages 3982–3992. Association for Computational Linguistics, 2019. doi:10.18653/v1/D19-1410. [38] Sushant Dinesh, Nathan Burow, Dongyan Xu, and Mathias Payer. Retrowrite: Statically instrumenting cots binaries for fuzzing and sanitization. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1497–1511. IEEE, 2020. [39] Gregory J Duck, Xiang Gao, and Abhik Roychoudhury. Binary rewriting without control flow recovery. In Proceedings of the 41st ACM SIGPLAN conference on programming language design and implementation, pages 151–163, 2020. [40] Thiago Rodrigues Alves, Mario Buratto, Flavio Mauricio de Souza, and Thelma Virginia Rodrigues. OpenPLC: An open source alternative to automation. In Proceedings of the 2014 IEEE Global Humanitarian Technology Conference, pages 585–589. IEEE, 2014. doi:10.1109/GHTC.2014.6970342. [41] Modbus Organization. Modbus application protocol specification V1.1b3, April 2012. URL https://www. modbus.org/file/secure/modbusprotocolspecification.pdf. Published April 26, 2012. [42] DNP Technical Committee. DNP3 technical bulletin TB2016-002: Addressing deficiencies in DNP3-SAv5, 2016. URL https://www.witsprotocol.org/ 01-sep-2016-dnp3-technical-bulletin-tb2016-002-information-for-wits-members/. Public information page; full bulletin available to DNP Users Group members. [43] International Electrotechnical Commission. IEC 60870-5-104:2006: Telecontrol equipment and systems — part 5-104: Transmission protocols — network access for IEC 60870-5-101 using standard transport profiles, 2006. URL https://webstore.iec.ch/en/publication/3746. International standard. [44] International Electrotechnical Commission. IEC 61131-3:2013: Programmable controllers — part 3: Programming languages, 2013. URL https://webstore.iec.ch/en/publication/4552. International standard, Third edition. [45] Quang-Cuong Bui, Ranindya Paramitha, Duc-Ly Vu, Fabio Massacci, and Riccardo Scandariato. APR4Vul: An empirical study of automatic program repair techniques on real-world java vulnerabilities. Empirical Software Engineering, 29(1):18, 2024. doi:10.1007/s10664-023-10415-7. 37
SCARA
A P REPRINT
[46] Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ansi-c programs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 168–176. Springer, 2004. [47] Frank Wilcoxon. Individual comparisons by ranking methods. Biometrics Bulletin, 1(6):80–83, 1945. doi:10.2307/3001968. [48] Gregory J. Duck, Xiang Gao, and Abhik Roychoudhury. Binary rewriting without control flow recovery. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 151–164. ACM, 2020. doi:10.1145/3385412.3385972. [49] An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. Qwen3 technical report. arXiv preprint arXiv:2505.09388, 2025. URL https: //arxiv.org/abs/2505.09388. [50] DeepSeek-AI. DeepSeek-V3 technical report. arXiv preprint arXiv:2412.19437, 2024. URL https://arxiv. org/abs/2412.19437. [51] Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of Lecture Notes in Computer Science, pages 337–340. Springer, 2008. doi:10.1007/978-3-540-78800-3_24. [52] Jacob Cohen. Statistical Power Analysis for the Behavioral Sciences. Lawrence Erlbaum Associates, Hillsdale, NJ, 2 edition, 1988. ISBN 0805802835. [53] Sofia Bobadilla, Monica Jin, and Martin Monperrus. Do automated fixes truly mitigate smart contract exploits? IEEE Transactions on Software Engineering, 52(1):100–115, 2026. doi:10.1109/TSE.2025.3618123. [54] Bo Feng, Alejandro Mera, and Long Lu. P2IM: Scalable and hardware-independent firmware testing via automatic peripheral interface modeling. In Proceedings of the 29th USENIX Security Symposium, pages 1237– 1254. USENIX Association, 2020. URL https://www.usenix.org/conference/usenixsecurity20/ presentation/feng. [55] Zhizhuang Jia, Chao Yang, Pengbin Feng, Xiaoyun Zhao, Xinghua Li, and Jianfeng Ma. Impact assessment of third-party library vulnerabilities through vulnerability reachability analysis. Computers & Security, page 104546, 2025. [56] Dimitrios Tychalas, Hadjer Benkraouda, and Michail Maniatakos. ICSFuzz: Manipulating I/Os and repurposing binary code to enable instrumented fuzzing in ICS control applications. In Proceedings of the 30th USENIX Security Symposium, pages 2847–2862. USENIX Association, 2021. URL https://www.usenix.org/conference/ usenixsecurity21/presentation/tychalas.
38