First order logic to set requirements for secure code execution
https://doi.org/10.15514/ISPRAS-2017-29(5)-8
Abstract
Currently the problem of information security during designing and exploiting the objects of critical information infrastructure is paid special attention to. One of the most common approaches to providing information security, processed on the objects, is creating isolated programming environment. The environment security is determined by its invariability. However, the evolutional development of data processing systems gives rise to the necessity of implementing the new components and software in this environment under condition that security requirements are satisfied. The most important requirement consists in trust in the new programming code. The given paper is devoted to developing formal logical language of description of functional requirements for programming code, allowing to make further demands at the stage of static analysis and to control their implementation in dynamics.
About the Author
A. V. Kozachok
The Academy of the Federal Guard Service of the Russian Federation
Russian Federation
Russian Federation
References
1. Federal law draft no. 9198-P10 "On the security of the critical information infrastructure of the Russian Federation". URL: http://asozd2.duma.gov.ru/main.nsf/ (SpravkaNew)/OpenAgent&RN=47571-7&02 (in Russian).
2. Kozachok A.V., Kochetkov E.V, Tatarinov A.M. Construction Heuristic Malware Detection Mechanism Based on Static Executable File Analysis Possibility Proof. Vestnik komp'juternyh i informacionnyh tehnologij [Herald of Computer and Information Technologies], 2017, no. 3, pp. 50-56. DOI: 10.14489/vkit.2017.03. pp. 050-056 (in Russian).
3. Kozachok A.V., Kochetkov E.V. Using program verification for detecting malware. Voprosy kiberbezopasnosti [Cybersecurity issues], 2016, no. 3, vol. 16, pp. 25-32 (in Russian).
4. Kinder J. et al. Detecting malicious code by model checking. International Conference on Detection of Intrusions and Malware and Vulnerability Assessment. Springer Berlin Heidelberg, 2005, pp. 174-187.
5. Song F., Touili T. Efficient malware detection using model-checking. International Symposium on Formal Methods. Springer Berlin Heidelberg, 2012, pp. 418-433.
6. Song F., Touili T. PoMMaDe: pushdown model-checking for malware detection. Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering. ACM, 2013, pp. 607-610.
7. Jasiul B., Szpyrka M., Śliwa J. Formal Specification of Malware Models in the Form of Colored Petri Nets. Computer Science and its Applications. Springer Berlin Heidelberg, 2015, pp. 475-482.
8. Schneider F.B. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), 2000, vol. 3, no. 1, pp. 30-50.
9. Feng H.H. et al. Formalizing sensitivity in static analysis for intrusion detection. Proc. IEEE Symposium on Security and Privacy, 2004, pp. 194-208.
10. Basin D. et al. Enforceable security policies revisited. ACM Transactions on Information and System Security (TISSEC), 2013, vol. 16, no. 1, pp. 3-8.
11. Feng H.H. et al. Anomaly detection using call stack information. Proc. IEEE Symposium on Security and Privacy, 2003, pp. 62-75.
12. Basin D., Klaedtke F., Zălinescu E. Algorithms for monitoring real-time properties. International Conference on Runtime Verification. Springer Berlin Heidelberg, 2011, pp. 260-275.
13. Klark Je., Gramberg O., Peled D. Program models verification: Model Checking. Moscow, MCNMO, 2002, 416 p (in Russian).
14. Vel'der S.Je., Lukin M.A., Shalyto A.A., Jaminov B.R. Automata program verififcation. St. Petersburg, Nauka, 2011, 244 p (in Russian).
15. Russinovich M. E., Solomon D. A., Ionescu A. Windows internals. Pearson Education, 2012, 800 p.
16. Gordeev A.V. Operating systems. Izdatel'skij dom “Piter”, 2009, 412 p (in Russian).
17. Korotkov M.A., Stepanov E.O Fundamentals of formal logical languages. St. Petersburg, SPb GITMO (TU), 2003, 84 p (in Russian).
18. Hafer T., Thomas W. Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree. International Colloquium on Automata, Languages and Programming. Springer Berlin Heidelberg, 1987, pp. 269-279.
19. Federal Service for Technical and Export Control. Information security threats database. URL: http://bdu.fstec.ru (in Russian).
Review
For citations:
Kozachok A.V. First order logic to set requirements for secure code execution. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(5):135-148. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(5)-8
Email this article 