Штучний інтелект

Анотація: 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.

Ключові слова: digital twin; vulnerability detection; Kleene algebra; AArch64; CWE; machine code; static rule; software security.

Посилання:

1. Arm Limited. (2023). Arm architecture reference manual for A-profile architecture (Arm DDI 0487). https://developer.arm.com/documentation/ddi0487/latest
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: Heap-based buffer overflow. https://cwe.mitre.org/data/definitions/122.html
6. Cadar, C., Dunbar, D., & Engler, D. R. (2008). KLEE: Unassisted and automatic generation of high-coverage 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://smt-lib.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