Prototype of a Verified Program Code Execution System

Abstract

This paper describes technical implementation of a verified program code execution system. The functional purpose of the system is to investigate arbitrary executable files of an operating system in the absence of source codes in order to control program code execution within specified functional requirements. The prerequisites for development of such a system are outlined and a user’s operating procedure with two typical usage scenarios is described. General description of the architecture of the system and software used for its implementation, including the mechanism of interaction among system elements, is presented. A model example of implementing the system is considered. A flexible set of functional constraints based on a temporal attribute of process action is described. In conclusions, a brief comparison with the closest analogs is conducted.