ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 UDC: 004.056.5:004.8
https://doi.org/10.15407/jai2026.02.212
О. Mostovyi1, D. Symonov2 1,2
V. M. Glushkov Institute of Cybernetics of the National Academy of Sciences (NAS) of Ukraine, Akademika Glushkova Avenue, 40, Kyiv, 03187 1 [email protected] 2 [email protected] 1 https://orcid.org/0009-0006-6687-866X 2 https://orcid.org/0000-0002-6648-4736
VULNERABILITY DETECTION IN AARCH64 MACHINE CODE USING A DIGITAL TWIN Abstract. This paper proposes an explainable digital twin for vulnerability detection in AArch64 machine code without access to source code. The digital twin reproduces the concrete execution of a program and preserves the state of registers, processor flags, memory, and live allocated blocks. Each instruction is transformed into a trace event containing the instruction name, operand values, and the post-instruction state. Vulnerabilities are represented as symbolic rules in Kleene algebra with tests: each rule specifies an event sequence and predicates over the machine state. This approach enables the detection of not only isolated unsafe instructions but also multi-step execution patterns. The rules are compiled into finite automata that scan the trace without using an SMT solver. The experimental evaluation covers three CWE classes: integer overflow (CWE-190), null pointer dereference (CWE-476), and heap buffer overflow (CWE-122). The system detected all three predefined vulnerabilities and produced no report on the safe trace. Each detection result includes the triggered rule, the trace position, and the concrete state values, thereby providing a reproducible explanation. Keywords: digital twin; vulnerability detection; Kleene algebra; AArch64; CWE; machine code; static rule; software security.
Introduction Software-intensive systems increasingly depend on embedded, mobile, and cyberphysical components whose behaviour is determined by low-level executable code. In many practical cases, especially for firmware, third-party libraries, vendor-specific modules, and closed embedded platforms, the source code is unavailable. Vulnerability detection then cannot rely on source-level abstractions such as data types, function boundaries, or high-level control structures. The observable object is the binary execution itself, represented by processor instructions, operands, registers, condition flags, memory addresses, and state transitions. This setting is particularly important for AArch64, the 64-bit ARM architecture widely used in mobile devices, embedded boards, and edge systems [1]. Security defects at this level may lead to unauthorized memory access, program crashes, privilege escalation, or control-flow manipulation. Binary-level vulnerability detection is therefore both a practical engineering task and a problem of computer science, in which program behavior must be analyzed through formal models of execution, state, and event sequences.
A central difficulty is that many vulnerabilities are not isolated instructionlevel defects. They appear as chains of semantically related events. For example, an arithmetic operation may overflow, the corrupted result may later be used as a size parameter, and a subsequent memory operation may access an invalid region. Similar multi-step mechanisms occur in integer overflow, null pointer dereference, heap buffer overflow, use-after-free, and timeof-check to time-of-use scenarios. The Common Weakness Enumeration (CWE) provides a standardized taxonomy for such classes [2], including integer overflow or wraparound (CWE-190) [3], null pointer dereference (CWE-476) [4], and heap-based buffer overflow (CWE-122) [5]. Existing binary analysis methods provide substantial capabilities but do not remove this difficulty. Symbolic execution systems such as KLEE, angr, and BAP analyse program paths and reason about vulnerabilityrelevant constraints [6]–[8], and SMT solvers such as Z3 with SMT-LIB representations give a strong formal basis for such analysis [9], [10]. These methods may become computationally expensive because of path explosion, complex memory modelling, and
212
ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 architecture-specific instruction semantics. Concrete dynamic analysis is more direct and cheaper, but it observes only executed traces and therefore needs a mechanism for detecting semantically meaningful vulnerability patterns in those traces. This paper proposes such a mechanism by combining a digital twin of machine-code execution with symbolic artificial intelligence. A digital twin is a virtual representation of a real system or process [11], [12]; here it represents the concrete execution of AArch64 code, recording the machine state after each instruction. The artificial-intelligence component is symbolic and knowledge-based: vulnerability classes are encoded as explicit rules over event sequences, expressed in Kleene algebra, which describes event sequences [13], and in Kleene algebra with tests, which adds state-dependent predicates [14]. A rule can thus require not only that certain instructions occur, but also that concrete conditions over registers, flags, addresses, or memory blocks hold at the corresponding steps. Rule matching is performed by compiling each pattern into a finite automaton and scanning the trace [15]. The unresolved problem addressed here is the lack of a compact, explainable method that operates directly on machine code, detects multi-step vulnerability patterns in concrete traces, does not require an SMT solver during matching, and provides a reproducible data of each detection. The goal of this paper is to develop such a method as a symbolic AI digital twin for selected CWE classes in AArch64 traces. The main contributions are: (i) an AArch64 digital-twin model that represents binary execution as a sequence of stateenriched events; (ii) an encoding of vulnerability knowledge as rules in Kleene algebra with tests; (iii) a solver-free, automaton-based detection procedure over concrete traces; and (iv) an evaluation on traces for CWE-190, CWE-476, and CWE122, together with a safe trace that verifies no rule fires when the vulnerability conditions are absent.
object is not a source-level program but a sequence of architecture-specific instructions and machine-state transitions. High-level types, variable names, and semantic annotations are unavailable, so the analysis must rely on instruction semantics, register values, condition flags, memory addresses, allocation states, and execution traces. This makes the problem especially relevant for AArch64 binaries used in embedded, mobile, edge, and firmware systems [1]. Existing methods address the problem from several directions. Static binary analysis reconstructs control-flow graphs, lifts machine code into intermediate representations, and applies data-flow or taint analysis; its precision is limited by indirect jumps, compiler optimizations, stripped symbols, and incomplete recovery of memory semantics. Dynamic binary analysis observes actual execution with concrete values; its advantage is precision on the executed path, and its limitation is trace dependence. Symbolic execution and constraintbased analysis form a more formal class. Tools such as KLEE, Angr, and BAP represent inputs or selected state components symbolically and generate path constraints [6]–[8], which are discharged by SMT solvers such as Z3, often through SMT-LIB [9], [10]. Symbolic execution can reason about alternative paths and synthesize triggering inputs, but its use on real binaries is constrained by path explosion, memory-modelling complexity, and solving overhead, which matter most when the goal is fast analysis of concrete traces rather than exhaustive exploration. Artificial-intelligence methods form a separate direction. Learning-based detectors built on deep neural networks and graph neural networks can flag vulnerability-prone code fragments, but their output is often probabilistic and does not pinpoint a formally verifiable execution condition. Knowledgebased and optimization methods, by contrast, represent decision criteria explicitly [16], [17]. For binary-level cybersecurity the explicit route is attractive, because it is necessary to know which instruction, flag, address, or event sequence caused the detection. This motivates symbolic artificial intelligence, in which knowledge is represented through rules,
Related Work Automated vulnerability detection in binary code is difficult because the analyzed
213
ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 predicates, and automata, so that a detection is justified by a matched event pattern and by the truth of state predicates at specific steps [2]– [5]. The unresolved part of the problem is the lack of a compact, understandable system that combines all of the following: direct operation on machine-code traces, explicit symbolic vulnerability rules, concrete AArch64 states, detection of multi-step patterns, and reproducible explanation without invoking an SMT solver per match. Existing static, dynamic, symbolic, and AI-based approaches meet these requirements only partially. The proposed approach integrates an AArch64 digital twin, Kleene Algebra, and automatonbased inference into a modular framework.
corresponding, respectively, to arithmetic overflow, null pointer access, and memory access outside live allocated blocks. The detection problem is then: given a trace 𝜏 and a rule base ℛ, find all pairs (𝑟, 𝐼), 𝑟 ∈ ℛ, with 𝐼 = (𝑖0 , … , 𝑖𝑘 ) and 0 ≤ 𝑖0 < ⋯ < 𝑖𝑘 ≤ 𝑇 , such that the subsequence 𝜏𝐼 = (𝑒𝑖0 , … , 𝑒𝑖𝑘 ) matches the event structure of 𝑟 and every test in 𝑟 is true on the corresponding state 𝑠𝑖𝑗 . Thus binary-level vulnerability detection is reduced to trace pattern recognition under state-dependent predicates: a detection is valid only when the required event pattern is present and the associated predicates over concrete states hold. Materials and methods Architecture of the Intelligent Digital
Problem Statement Let 𝑃 be an AArch64 binary program or a finite fragment of machine code, and let 𝛴 denote the set of AArch64 instructions supported by the digital twin. Execution is represented through concrete machine states that include registers, processor flags, memory, and live memory blocks. The machine-state space is 𝑆 = 𝑆reg × 𝑆flag × 𝑆mem × 𝑆alloc , (1) where 𝑆reg is the space of register valuations, 𝑆flag contains the processor flags 𝑁, 𝑍, 𝐶, 𝑉 , 𝑆mem represents memory contents, and 𝑆alloc stores the current set of live allocated blocks. For each step 𝑡 = 0, … , 𝑇, let 𝑠𝑡 ∈ 𝑆 be the machine state after the 𝑡-th instruction. The corresponding trace event is 𝑒𝑡 = (𝜄𝑡 , 𝑜𝑝𝑡 , 𝑠𝑡 ), where 𝜄𝑡 ∈ 𝛴 is the executed instruction, 𝑜𝑝𝑡 is the tuple of operand values, and 𝑠𝑡 is the postinstruction state. A concrete execution trace is 𝜏 = (𝑒0 , 𝑒1 , … , 𝑒𝑇 ). Let ℛ be a finite knowledge base of vulnerability rules. Each rule 𝑟 ∈ ℛ is a term of Kleene algebra with tests, generated by the grammar 𝑟:: = 𝑎 ∣ [𝜑] ∣ 𝑟1 ; 𝑟2 ∣ 𝑟1 + 𝑟2 ∣ 𝑟 ∗ , (2) where 𝑎 is an event predicate (with the special predicate any matching every event), [𝜑] is a test over the current machine state, ; denotes sequential composition, + alternative choice, and (⋅)∗ finite repetition. Each test is a predicate 𝜑: 𝑆 → {0,1}. Typical tests used for vulnerability detection are 𝑉 = 1, 𝑎𝑑𝑑𝑟 = 0, ¬ in_alloc(𝑎𝑑𝑑𝑟), (3)
Twin The system is organized as an explainable Symbolic AI digital twin for AArch64 vulnerability detection. Its processing pipeline is 𝑃 → execution twin → 𝜏 → KAT-based matcher → detection report, with four modules: execution twin, event abstraction layer, symbolic knowledge base, and inference and explanation engine. Figure 1 shows the overall flow.
Fig. 1. From a binary program to a detection report
The execution twin reproduces the concrete execution of AArch64 instructions. For each instruction 𝜄𝑡 ∈ 𝛴 it applies the corresponding semantics and updates the machine state 𝑠𝑡 = (𝑟𝑒𝑔𝑡 , 𝑓𝑙𝑎𝑔𝑡 , 𝑚𝑒𝑚𝑡 , 𝑎𝑙𝑙𝑜𝑐𝑡 ) ∈ 𝑆,
(4)
so that instruction execution is a transition operator 𝛥𝜄 : 𝑆 × 𝑂𝑝𝜄 → 𝑆 with 214
ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 𝑠𝑡 = 𝛥𝜄𝑡 (𝑠𝑡−1 , 𝑜𝑝𝑡 ) . The event abstraction layer then forms the event 𝑒𝑡 = (𝜄𝑡 , 𝑜𝑝𝑡 , 𝑠𝑡 ) defined in the Problem Statement, so the run becomes a state-enriched trace 𝜏 = (𝑒0 , … , 𝑒𝑇 ) rather than raw bytes or disassembled text. The symbolic knowledge base holds a finite set ℛ of vulnerability rules. Each rule combines an event pattern with predicates over machine states and is stored as a Kleenealgebra-with-tests term or an equivalent JSON description. This module is the component of Symbolic AI: vulnerability knowledge is explicit, interpretable, and extendable. The inference and explanation engine compiles each rule 𝑟 into an automaton 𝐴𝑟 = (𝑄𝑟 , 𝑞𝑟0 , 𝐹𝑟 , 𝛿𝑟 ), (5) 0 where 𝑄𝑟 is the set of states, 𝑞𝑟 the initial state, 𝐹𝑟 the accepting states, and 𝛿𝑟 the transition relation induced by the event pattern and tests of 𝑟. The engine scans 𝜏 sequentially; at each event it checks both the instruction pattern and the relevant predicate 𝜑(𝑠𝑡 ), and reports a vulnerability only when the required sequence is matched and all tests are true. A detection has the form 𝑑 = (𝑟,CWE, 𝐼, 𝑉𝑑 ), (6) where 𝑟 is the triggered rule, CWE the weakness identifier, 𝐼 = (𝑖0 , … , 𝑖𝑘 ) the matched trace positions, and 𝑉𝑑 the concrete values that justify the detection (for example 𝑉 = 1, 𝑎𝑑𝑑𝑟 = 0, a destination register, or a store address outside all live blocks). The architecture thus separates execution modelling, event abstraction, symbolic knowledge, and inference, which makes each detection traceable to a rule, a trace fragment, and concrete values.
Representation of Vulnerability Knowledge by Kleene Algebra with Tests The knowledge base ℛ represents vulnerability classes as formal rules over the state-enriched events defined above. Rules follow grammar (2). The event predicates form a finite set 𝒜 : each 𝑎: 𝐸 → {0,1} checks whether an event belongs to a given instruction class (for example, arithmetic events add, adds, sub, subs, mul; or store events str, strb, strh). The state predicates form a finite set 𝛷: each 𝜑: 𝑆 → {0,1} checks a condition over the concrete state, the typical ones being 𝑉 = 1, 𝑎𝑑𝑑𝑟 = 0, 𝑎𝑑𝑑𝑟 > 0x1000, and ¬ in_alloc(𝑎𝑑𝑑𝑟). The semantics of a rule 𝑟 is a language ℒ(𝑟) ⊆ 𝐸 ∗ over finite trace fragments. For an event 𝑒 = (𝜄, 𝑜𝑝, 𝑠), ℒ(𝑎) = {(𝑒) ∈ 𝐸 ∗ : 𝑎(𝑒) = 1}, (7) ∗ ℒ([𝜑]) = {(𝑒) ∈ 𝐸 : 𝜑(𝑠) = 1}, (8) and, for compound expressions, ℒ(𝑟1 ; 𝑟2 ) = {𝑢𝑣: 𝑢 ∈ ℒ(𝑟1 ), 𝑣 ∈ ℒ(𝑟2 )}, (9) ℒ(𝑟1 + 𝑟2 ) = ℒ(𝑟1 ) ∪ ℒ(𝑟2 ), (10) ℒ(𝑟 ∗ ) = ∪ ℒ(𝑟)𝑛 . (11) 𝑛≥0
A rule therefore defines not only an instruction pattern but a set of trace fragments in which both the event sequence and the corresponding state predicates are satisfied. The current rule base contains three CWE-oriented rules. The integer-overflow rule for CWE-190 is 𝑟CWE190 ∗ = any ; (𝑎𝑑𝑑 + 𝑎𝑑𝑑𝑠 + 𝑠𝑢𝑏 + 𝑠𝑢𝑏𝑠 + 𝑚𝑢𝑙); [𝑉 = 1], which fires on any add-like arithmetic instruction whose overflow flag is set. In the implementation the same rule is stored in JSON form in Fig. 2.
Fig. 2. JSON Kleene Rule
215
ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 regular for every 𝑟. Therefore each rule can be compiled into a finite automaton. Lemma 1 provides the basis for automaton-based detection: since every rule defines a regular trace language, matching reduces to finite-state recognition, and the tests require no SMT solving because they are evaluated on concrete states produced by the twin.
The null-pointer-dereference rule for CWE-476 is 𝑟CWE476 = any∗ ; (𝑙𝑑𝑟 + ⋯ + 𝑠𝑡𝑟 + ⋯ ); [𝑎𝑑𝑑𝑟 = 0], which fires when a load or store uses an effective address equal to zero. The heapbuffer-overflow rule for CWE-122 is 𝑟CWE122 = any∗ ; (𝑠𝑡𝑟 + 𝑠𝑡𝑟𝑏 + 𝑠𝑡𝑟ℎ); [𝑎𝑑𝑑𝑟 > 0x1000 ∧ ¬ in_alloc(𝑎𝑑𝑑𝑟)], which fires when a store writes to an address above 0x1000 that is not contained in any live allocated block. These three rules constitute the knowledge base ℛ = {𝑟CWE190 , 𝑟CWE476 , 𝑟CWE122 }. The same representation can describe multi-step mechanisms (Figure 3). A heaprelated vulnerability, for instance, links an arithmetic result, a later allocation size, and a subsequent store address: the event predicates select the relevant instruction classes, while the tests preserve equality, range, and membership relations between values stored in machine states. This is the main advantage of Kleene algebra with tests over single-instruction checking: a rule may encode a vulnerability as a trace-level mechanism rather than an isolated event.
Automaton-Based Inference Mechanism For each rule 𝑟 ∈ ℛ the inference engine uses the automaton 𝐴𝑟 of (5) as the symbolic inference mechanism that applies the rule to the trace. A transition is enabled by two conditions: the current event must satisfy the required event predicate, and the current state must satisfy the corresponding test. For an event 𝑒𝑡 = (𝜄𝑡 , 𝑜𝑝𝑡 , 𝑠𝑡 ) a transition has the 𝑎,𝜑
form 𝑞 → 𝑞′, taken at step 𝑡 if 𝑎(𝑒𝑡 ) = 1 and 𝜑(𝑠𝑡 ) = 1 ; a transition without a state condition uses the constant predicate 𝜑(𝑠) = 1. The trace 𝜏 = (𝑒0 , … , 𝑒𝑇 ) is processed in one pass. At each step the engine updates the active automaton states of all rules, without enumerating alternative paths and without invoking an SMT solver. For example, the CWE-190 automaton (Figure 4) stays in a scanning state while arbitrary events are read; when an arithmetic event from the specified class is observed, it checks the overflow flag in the post-instruction state, and if 𝑉 = 1 the accepting state is reached and a CWE-190 detection is generated.
Fig. 3. A multi-step rule links one value across three events
Lemma 1. Every rule 𝑟 generated by grammar (2) defines a regular language over the extended alphabet of events equipped with state predicates. Proof. Each event predicate 𝑎 denotes a set of one-event words and is regular. Each test [𝜑] denotes a set of one-event words selected by a predicate over the state component, hence is regular over the extended alphabet. Regular languages are closed under concatenation, union, and Kleene iteration; since the grammar builds rules only by these operations on elementary event and test languages, ℒ(𝑟) is
Fig. 4. Automaton for the integer-overflow rule (CWE-190)
A match for 𝑟 is fixed when the automaton reaches an accepting state, 𝑞𝑡 ∈ 𝐹𝑟 . The engine then stores the matched positions 𝐼 = (𝑖0 , … , 𝑖𝑘 ) and the concrete values that made the transition sequence valid, and emits a detection report of the form (6). For CWE190, 𝑉𝑑 may contain the destination value, the source operands, and 𝑉 = 1 ; for CWE-476,
216
ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 𝑎𝑑𝑑𝑟 = 0; for CWE-122, the store address and the fact that it lies outside every live block. The procedure is summarized in Algorithm 1.
Experimental Setup The evaluation used the prototype DIGITAL_TWIN_ARM64_v2, a concretestate digital twin of AArch64 execution with 180 instruction meanings loaded from arm64_semantics.json. The vulnerability rules are loaded as Kleene-algebra-with-tests constraints from kat_v1_rules.json. The experiment therefore exercises the full pipeline: instruction execution, state reconstruction, event-trace generation, KATbased matching, and report generation. Each trace was processed by the command
Algorithm 1. Automaton-based symbolic inference Input: trace 𝜏 = (𝑒0 , … , 𝑒𝑇 ), rule base ℛ. Output: set of detection reports 𝒟. 1. For each rule 𝑟 ∈ ℛ , construct the automaton 𝐴𝑟 . 2. Initialize the active state of each 𝐴𝑟 to its initial state 𝑞𝑟0 . 3. For each event 𝑒𝑡 = (𝜄𝑡 , 𝑜𝑝𝑡 , 𝑠𝑡 ) : update every active automaton state using the event predicate 𝑎(𝑒𝑡 ) and the state predicate 𝜑(𝑠𝑡 ). 4. If an accepting state of 𝐴𝑟 is reached, create a report 𝑑 = (𝑟,CWE, 𝐼, 𝑉𝑑 ). 5. Return all reports in 𝒟. For a fixed rule base, the cost is proportional to the trace length and the total number of automaton transitions updated. When the automata are small and the number of active states is bounded, the procedure is a linear streaming pass over the trace, which is sufficient for the compact CWE-190, CWE476, and CWE-122 rules evaluated here. The detector is a symbolic, knowledgebased component rather than a learned one. Vulnerability classes are stored as explicit, inspectable rules, and a positive detection is a reproducible derivation: the automaton path identifies the matched event sequence and the tests identify the concrete state facts that triggered the rule. The system does not train a model or infer rules from data. A future neurosymbolic extension could use machine learning to rank suspicious trace fragments or to propose candidate rules, while keeping the final, explainable verification rule-based.
./bin/digital_twin_arm64 \ -s semantics/arm64_semantics.json \ --kat-constraints \ constraints/kat_v1_rules.json \ <trace>.json
The rule base ℛ contained the three rules defined above. Four execution traces were used: three contain one known vulnerability each, and one is safe. The safe trace verifies that the rule base does not fire when the state predicates are false. Trace 1 (CWE-190) adds 0x7FFFFFFF and 0x1, producing 0x80000000 with 𝑉 = 1. Trace 2 (CWE-476) loads from address 0 . Trace 3 (CWE-122) stores to 0x200000 , outside the live block [0x100000,0x100080) . Trace 4 (safe) performs a small addition 0x10 + 0x20 with no overflow and accesses only the live block [0x800,0x880). Results The prototype detected all three vulnerable traces and produced no detection on the safe trace; the results are summarized in Table 1. For each positive detection the prototype produced a report containing the CWE identifier, the triggering trace position, and the concrete explanatory values.
Table 1. Detection results on the four traces Trace 1 2 3 4
Expected CWE-190 CWE-476 CWE-122 safe
Detected yes yes yes no
Triggering condition (key values) V = 1, dst = 0x80000000 addr = 0x0 addr = 0x200000, outside [0x100000, 0x100080) V = 0, access within [0x800, 0x880)
217
ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 In Trace 1, rule 𝑟CWE190 fired after the 32-bit addition of 0x7FFFFFFF and 0x1: the result was 0x80000000 and the overflow flag 𝑉 was set, so the detection was justified by the arithmetic instruction class together with the post-instruction state satisfying 𝑉 = 1 . In Trace 2, rule 𝑟CWE476 fired when the program loaded from the address held in 𝑥0; since 𝑥0 = 0, the effective address was 𝑎𝑑𝑑𝑟 = 0x0. In Trace 3, rule 𝑟CWE122 fired on a store to 𝑎𝑑𝑑𝑟 = 0x200000, which lies outside the live block [0x100000,0x100080), so the detection was explained by the store event and the predicate ¬ in_alloc(𝑎𝑑𝑑𝑟). Trace 4 served as a negative control: the addition 0x10 + 0x20 did not set the overflow flag, and the memory accesses stayed within the live block [0x800,0x880), so none of the predicates 𝑉 = 1 , 𝑎𝑑𝑑𝑟 = 0 , or ¬ in_alloc(𝑎𝑑𝑑𝑟) held and no rule fired. In every case the detector linked the symbolic rule, the concrete machine state, and the generated explanation.
flat table of live blocks, which is adequate for the reported experiments but weaker than a full symbolic-heap model. Conclusions This paper proposed an explainable Symbolic AI digital twin for vulnerability detection in AArch64 machine-code traces. The approach combines a concrete-state execution twin, a symbolic knowledge base of CWE-oriented rules in Kleene algebra with tests, and an automaton-based inference mechanism. Its methodological core is the reduction of binary-level vulnerability detection to trace pattern recognition under state-dependent predicates: unlike SMT-based symbolic execution, the mechanism does not solve path constraints during detection but evaluates explicit predicates over concrete states, which makes each detection directly described through a rule, a trace position, and concrete evidence such as 𝑉 = 1, 𝑎𝑑𝑑𝑟 = 0, or an address outside a live block. The experimental validation confirmed the expected behaviour on four controlled traces: the system detected integer overflow (CWE-190), null pointer dereference (CWE476), and heap buffer overflow (CWE-122), and produced no detection on the safe trace. The current implementation is limited to concrete traces, 180 AArch64 instruction meanings, and a small rule base. Future work will extend the rule set to further CWE classes, including use-after-free (CWE-416) and timeof-check to time-of-use (CWE-367), improve the memory model, support larger traces, and evaluate the approach on real firmware and binary datasets.
Discussion The evaluation indicates that compact Kleene-algebra-with-tests rules can capture multi-step weaknesses in AArch64 machine code while operating directly on concrete execution traces. Three properties follow from the design. Detection is solver-free: each test is evaluated on a concrete state produced by the twin, which keeps matching to a single linear pass over the trace. Because a rule combines an event pattern with state predicates and may reuse bound values across steps, it expresses vulnerability mechanisms that singleinstruction checks cannot represent. And each detection is accompanied by the concrete values that satisfied the rule, which yields a reproducible explanation rather than an opaque score. The approach also has clear limitations. Detection is confined to the supplied trace, so, unlike symbolic execution [6], [7], it does not explore alternative inputs. Its precision depends on the fidelity of the instruction semantics and on the quality of the traces. The present rule base covers three CWE classes; the safe trace produced no false positive on this controlled set, but a larger and more diverse benchmark is required to estimate precision and recall. Finally, the allocation model is a
References 1. Arm Limited. (2023). Arm architecture reference manual for A-profile architecture (Arm DDI 0487). https://developer.arm.com/documentation/ddi0487/late st 2. MITRE Corporation. (2024). Common Weakness Enumeration (CWE). https://cwe.mitre.org/ 3. MITRE Corporation. (2024). CWE-190: Integer overflow or wraparound. https://cwe.mitre.org/data/definitions/190.html 4. MITRE Corporation. (2024). CWE-476: NULL pointer dereference. https://cwe.mitre.org/data/definitions/476.html 5. MITRE Corporation. (2024). CWE-122: Heapbased buffer overflow. 218
ISSN 2710 – 1673 Artificial Intelligence 2026 № 2 https://cwe.mitre.org/data/definitions/122.html 6. Cadar, C., Dunbar, D., & Engler, D. R. (2008). 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 (OSDI) (pp. 209–224). USENIX Association. 7. Shoshitaishvili, Y., Wang, R., Salls, C., Stephens, N., Polino, M., Dutcher, A., Grosen, J., Feng, S., Hauser, C., Kruegel, C., & Vigna, G. (2016). SoK: (State of) the art of war: Offensive techniques in binary analysis. In IEEE Symposium on Security and Privacy (pp. 138–157). https://doi.org/10.1109/SP.2016.17 8. Brumley, D., Jager, I., Avgerinos, T., & Schwartz, E. J. (2011). BAP: A binary analysis platform. In Computer Aided Verification (CAV) (LNCS Vol. 6806, pp. 463–469). Springer. https://doi.org/10.1007/978-3-642-22110-1_37 9. de Moura, L., & Bjørner, N. (2008). Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (LNCS Vol. 4963, pp. 337–340). Springer. https://doi.org/10.1007/978-3-540-78800-3_24 10. Barrett, C., Fontaine, P., & Tinelli, C. (2017). The SMT-LIB standard, version 2.6. Department of Computer Science, The University of Iowa. https://smtlib.org/ 11. Tao, F., Zhang, H., Liu, A., & Nee, A. Y. C. (2019). Digital twin in industry: State-of-the-art. IEEE Transactions on Industrial Informatics, 15(4), 2405– 2415. https://doi.org/10.1109/TII.2018.2873186 12. Grieves, M. (2014). Digital twin: Manufacturing excellence through virtual factory replication [White paper]. Florida Institute of Technology.
13. Kleene, S. C. (1956). Representation of events in nerve nets and finite automata. In C. E. Shannon & J. McCarthy (Eds.), Automata studies (pp. 3–42). Princeton University Press. https://doi.org/10.1515/9781400882618-002 14. Kozen, D. (1997). Kleene algebra with tests. ACM Transactions on Programming Languages and Systems, 19(3), 427–443. https://doi.org/10.1145/256167.256195 15. Thompson, K. (1968). Programming techniques: Regular expression search algorithm. Communications of the ACM, 11(6), 419–422. https://doi.org/10.1145/363347.363387 16. Symonov, D. I. (2021). Algorithm for determining the optimal flow in Supply Chains, considering multi-criteria conditions and stochastic processes. Bulletin of Taras Shevchenko National University of Kyiv. Physical and Mathematical Sciences, 2, 109–116. https://doi.org/10.17721/1812-5409.2021/2.15 17. Symonov, D., & Symonov, Y. (2024). Integration of knowledge management processes into a dynamic organizational environment. Artificial Intelligence, 29(2), 98–106. https://doi.org/10.15407/jai2024.02.098 The article has been sent to the editors 09.06.26. After processing 20.06.26. Submitted for printing 30.06.26 Copyright under license CCBY-SA4.0.
219