Verified program code execution system prototype

A. V. Kozachok, E. V. Kochetkov

Academy of Federal Guard Service

Abstract: 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.

Keywords: formal verification, security automata, controlled execution, malware.

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

Bibliographic databases:

•