Verified program code execution system prototype
https://doi.org/10.15514/ISPRAS-2017-29(6)-1
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.
About the Authors
A. V. Kozachok
Academy of Federal Guard Service
Russian Federation
Russian Federation
E. V. Kochetkov
Academy of Federal Guard Service
Russian Federation
Russian Federation
References
1. Ukaz Prezidenta Rossijskoj Federatsii ot 05.12.2016 № 646 «Ob utverzhdenii Doktriny informatsionnoj bezopasnosti Rossijskoj Federatsii» [Decree of the President of the Russian Federation of 05.12.2016 No. 646 «On Approving the Doctrine of Information Security of the Russian Federation»].
2. Garbuk S.V., Komarov A.A., Salov E.I. Overview of incidents of information security of SCADA of foreign countries: Analytical report. Zashhita informatsii. Insajd [Data protection. Inside], no. 6, 2010, pp. 50-58.
3. Yaremchuk S. APT: Reality or Paranoia. Sistemnyj administrator [System Administrator], no. 7-8, pp. 52-56.
4. Dovgolenko A.A. Social engineering in the Internet. Informatsionnaya bezopasnost' i voprosy profilaktiki kiberehkstremizma sredi molodezhi Materialy vnutrivuzovskoj konferentsii. Pod redaktsiej G.N. CHusavitinoj, E.V. CHernovoj, O.L. Kolobovoj [Proc. of Information security and issues of the prevention of cyber extremism among young people Materials of the intra-university conference]. 2015. pp. 183-191.
5. Kozachok A.V. Detection of malicious software based on hidden Markov models: PhD thesis. Oryol, 2012, 209 p. (in Russian)
6. Kozachok A.V., Kochetkov E.V. Using Program Verification for Detecting Malware. Cybersecurity issues, vol. 16, no. 3, 2016, pp. 25-32 (in Russian)
7. Cimitile A. et al. Model checking for mobile Android malware evolution. Formal Methods in Software Engineering (FormaliSE), 2017 IEEE. ACM 5th International FME Workshop on., 2017, pp. 24-30, IEEE
8. Kozachok A.V., Kochetkov E.V. Formal model of functioning process in the operating system. SPIIRAS Proceedings, vol. 51, issue 2, 2017, pp. 78-96 (in Russian).
9. Kozachok A., Bochkov M., Lai Minh T., Kochetkov E. First order logic for program code functional requirements description. Cybersecurity issues, vol. 3, issue 21, 2017, pp 2-7.
10. Jesse Hertz. Project Triforce: Run AFL on Everything! (online) Available at: https://www.nccgroup.trust/us/about-us/newsroom-and-events/blog/2016/june/projecttri force-run-afl-on-everything/, accessed 01.11.17
11. Ivannikov Institute for System Programming of the RAS. Source Repository of the «Qemu». (online) Available at: https://github.com/ispras/qemu, accessed 05.09.17
12. Documentation/QMP - QEMU. QEMU Machine Protocol. (online) Available at: https://wiki.qemu.org/Documentation/QMP, accessed 15.10.17
Review
For citations:
Kozachok A.V., Kochetkov E.V. Verified program code execution system prototype. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(6):7-24. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(6)-1
Email this article 