Proceedings of ISP RAS

Verified program code execution system prototype

Kozachok A.V. (FSO Academy, Orel, Russia)
Kochetkov E.V. (FSO Academy, Orel, Russia)


The article represented the technical implementation of the system of verified program code execution. The functional purpose of this system is to investigate arbitrary executable files of the operating system in the absence of source codes in order to provide the ability to control the execution of the program code within the specified functional requirements. The prerequisites for the creation of such a system are described, the user's operating procedure is given according to two typical usage scenarios. A general description of the architecture of the system and the software used for its implementation, the mechanism of interaction of the elements of the system are presented. The model example of implementation this system is presented. Demonstrating the flexible set of functional constraints, based on temporal attribute process action. At the end of the article given a brief comparison with the closest analogues.


formal verification, security automata, controlled execution, malware


Proceedings of the Institute for System Programming, vol. 29, issue 6, 2017, pp. 7-24.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(6)-1

Full text of the paper in pdf (in Russian) Back to the contents of the volume