Abstract
Presently, a special attention is paid to the problem of information security when designing and using objects of critical information infrastructure. One of the most common approaches used to secure the information processed on these objects is the creation of an isolated program environment (sandbox). The security of the environment is determined by its invariability. However, the evolutionary development of data processing systems makes it necessary to implement new components and software in this environment on the condition that the security requirements are met. In this case, the most important requirement is trust in a new program code. This paper is devoted to developing a formal logical language to describe functional requirements for program code that allows one to impose further constraints at the stage of static analysis, as well as to control their fulfillment in dynamics.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Draft Federal Law no. 47571-7 “On the Security of the Critical Information Infrastructure of the Russian Federation.” http://asozd2.duma.gov.ru/main.nsf/(Spravka)?OpenAgent&RN=47571-7.
Kozachok, A.V., Kochetkov, E.V., and Tatarinov, A.M., Substantiation of the possibility to construct a heuristic mechanism for malware recognition based on static analysis of executable files, Vestn. Komp’yut. Inf. Tekhnol., 2017, no. 3, pp. 50–56.
Kozachok, A.V. and Kochetkov, E.V., Substantiation of the possibility to apply program verification to malicious code detection, Vopr. Kiberbezopasnosti, 2016, vol. 16, no. 3, pp. 25–32.
Kinder, J., et al., Detecting malicious code by model checking, Proc. Int. Conf. Detection of Intrusions and Malware and Vulnerability Assessment, Berlin: Springer, 2005, pp. 174–187.
Song, F. and Touili, T., Efficient malware detection using model-checking, Proc. Int. Symp. Formal Methods, Berlin: Springer, 2012, pp. 418–433.
Song, F. and Touili, T., PoMMaDe: Pushdown modelchecking for malware detection, Proc. 9th Joint Meeting on Foundations of Software Engineering, ACM, 2013, pp. 607–610.
Jasiul, B., Szpyrka, M., and Sliwa, J., Formal specification of malware models in the form of colored Petri nets, in Computer Science and its Applications, Springer, 2015, pp. 475–482.
Schneider, F.B., Enforceable security policies, ACM Trans. Inf. Syst. Secur. (TISSEC), 2000, vol. 3, no. 1, pp. 30–50.
Feng, H.H., et al., Formalizing sensitivity in static analysis for intrusion detection, Proc. IEEE Symp. Security and Privacy, 2004, pp. 194–208.
Basin, D., et al., Enforceable security policies revisited, ACM Trans. Inf. Syst. Secur. (TISSEC), 2013, vol. 16, no. 1, pp. 3–8.
Feng, H.H., et al., Anomaly detection using call stack information, Proc. IEEE Symp. Security and Privacy, 2003, pp. 62–75.
Basin, D., Klaedtke, F., and Zalinescu, E., Algorithms for monitoring real-time properties, Proc. Int. Conf. Runtime Verification, Berlin: Springer, 2011, pp. 260–275.
Clarke, E.M., Grumberg, O., and Peled, D., Model Checking, MIT Press, 1999.
Vel’der, S.E., Lukin, M.A., Shalyto, A.A., and Yaminov, B.R., Verifikatsiya avtomatnykh programm (Verification of Automata-Based Programs), St. Petersburg: Nauka, 2011.
Russinovich, M.E. and Solomon, D.A., Windows Internals, Microsoft Press, 2012, 6th ed.
Gordeev, A.V., Operatsionnye sistemy (Operating systems), St. Petersburg: Piter, 2009.
Korotkov, M.A. and Stepanov, E.O., Osnovy formal’nykh logicheskikh yazykov (Basics of Formal Logic Languages), St. Petersburg: State Inst. Precision Mech. Opt. (Tech. Univ.), 2003.
Hafer, T. and Thomas, W., Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, Proc. Int. Colloq. Automata, Languages and Programming, Berlin: Springer, 1987, pp. 269–279.
Databank of Information Security Threats. http://www.bdu.fstec.ru.
Author information
Authors and Affiliations
Corresponding author
Additional information
Original Russian Text © A.V. Kozachok, 2017, published in Trudy Instituta Sistemnogo Programmirovaniya, 2017, Vol. 1, No. 2, pp. 3–4.
Rights and permissions
About this article
Cite this article
Kozachok, A.V. Formal logical language to set requirements for secure code execution. Program Comput Soft 43, 314–319 (2017). https://doi.org/10.1134/S036176881705005X
Received:
Published:
Issue Date:
DOI: https://doi.org/10.1134/S036176881705005X