A formal model of executive software code based on an execution graph for solving the binary morphing problem

This paper addresses the problem of developing a formal model of executable software code intended to provide a rigorous mathematical description of runtime program transformation (code morphing) processes. The relevance of the study is determined by the need to develop a mathematical framework that provides a formal justification for methods of modifying the structure of executable code without violating the functional correctness of software. The aim of the study is to develop an architecture-independent formal model of executable code that enables the identification of invariant software properties during code morphing operations and establishes the conditions required to preserve the observable behavior of a program. The proposed model integrates both static and dynamic components of executable code. The static component represents a program as a collection of basic blocks connected by a control flow graph, together with a code placement configuration in the address space and a set of control references between the blocks. The dynamic component provides a formal description of the program execution trace, the sequence of computational system states, and the observable behavior defined exclusively by externally observable execution results. The practical significance of the study lies in the development of a unified formal framework suitable for proving the correctness of executable code morphing algorithms, designing methods for their formal verification, and analyzing the security of software systems. The obtained results establish a theoretical foundation for further research in the field of dynamic executable code transformation and the development of advanced software protection technologies.