Secure code execution system operation algorithm
https://doi.org/10.15514/ISPRAS-2017-29(3)-2
Abstract
The article presented a set of algorithms that form the basis of the safe code execution system. The functional purpose of it 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 set of algorithms presented in this work includes: the algorithm for the functioning of a system for the safe execution of the program code; the algorithm for constructing a program model suitable for verification, which accurately preserves the properties of the source program.
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. Kozachok A.V., Bochkov M.V., Fatkieva R.R, Tuan L.M. Analytical Model for Protecting Documentary File Formats from Unauthorized Access. SPIIRAS Proceedings, vol. 43, no. 6, 2015, pp. 228-252 (in Russian)
2. Anti-Virus Comparative Summary Report. 2017. URL: https://www.avcomparatives.org/wp-content/uploads/2017/02/avc_sum_201612_en.pdf
3. Kozachok A.V. Detection of malicious software based on hidden Markov models: PhD thesis. Oryol, 2012, 209 p. (in Russian)
4. Kozachok A.V., Kochetkov E.V. Using Program Verification for Detecting Malware. Cybersecurity issues, vol. 16, no. 3, 2016, pp. 25-32 (in Russian)
5. Kozachok A.V., Kochetkov E.V. Formal model of functioning process in the operating system. SPIIRAS Proceedings, vol. 51, no. 2,. 2017, pp. 78-96 (in Russian)
6. Clarke Edmund M, Grumberg Orna, Peled Doron Model checking. MIT press, 1999.
7. Kinder Johannes, Katzenbeisser Stefan, Schallhart Christian, Veith Helmut Detecting malicious code by model checking. International Conference on Detection of Intrusions and Malware, and Vulnerability Assessment. Springer. 2005, pp. 174-187.
8. Song Fu, Touili Tayssir Pushdown model checking for malware detection. International Journal on Software Tools for Technology Transfer, vol. 16, no. 2, 2014, pp. 147-173.
9. Song Fu, Touili Tayssir Efficient malware detection using model-checking. International Symposium on Formal Methods. Springer, 2012, pp. 418-433
10. Song Fu, Touili Tayssir PoMMaDe: pushdown model-checking for malware detection. Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 2013, pp. 607-610.
11. Beaucamps Philippe, Gnaedig Isabelle, Marion Jean-Yves Abstraction-based malware analysis using rewriting and model checking. European Symposium on Research in Computer Security. Springer. 2012, pp. 806-823.
12. Holzer Andreas, Kinder Johannes, Veith Helmut Using verification technology to specify and detect malware. Computer Aided Systems Theory-EUROCAST. 2007, pp. 497-504.
13. Kozachok A.V., Bochkov M.V., Tuan L.M., Kochetkov E.V. First Order Logic For Program Code Functional Requirements Description. Cybersecurity issues, vol. 21, no. 3, 2017, pp. 2-7.
14. Schneider Fred B Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), vol. 3, no. 1, 2000, pp. 30-50.
15. Jesse Hertz Project Triforce: Run AFL on Everything! 2016. URL: https: //www.nccgroup.trust/us/about-us/newsroom-and-events/blog/2016/june/project-triforce-run-afl-on-everything/
Review
For citations:
Kozachok A.V., Kochetkov E.V. Secure code execution system operation algorithm. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(3):17-30. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(3)-2
Email this article 