Логика первого порядка для задания требований к безопасному программному коду
Автор: Козачок А.В.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 5 т.29, 2017 года.
Бесплатный доступ
В настоящее время вопросу защиты информации при проектировании и эксплуатации объектов критической информационной инфраструктуры уделяется особое внимание. Одним из распространенных подходов к обеспечению безопасности информации, обрабатываемой на объектах, при этом является создание изолированной программной среды. Безопасность среды обуславливается ее неизменностью. Однако эволюционное развитие систем обработки информации порождает необходимость запуска в данной среде новых компонентов и программного обеспечения при условии выполнения требований по безопасности. Наиболее важным при этом является вопрос доверия к новому программному коду. Данная работа посвящена разработке формального логического языка описания функциональных требований к программному коду, который позволит в дальнейшем предъявлять требования на этапе статического анализа и контролировать их выполнение в динамике.
Формальный логический язык, моделирование, процесс, вредоносная программа, проверка моделей, автомат безопасности
Короткий адрес: https://sciup.org/14916469
IDR: 14916469 | DOI: 10.15514/ISPRAS-2017-29(5)-8
Список литературы Логика первого порядка для задания требований к безопасному программному коду
- 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.
- 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 , 2017, no. 3, pp. 50-56. pp. 050-056 DOI: 10.14489/vkit.2017.03
- Kozachok A.V., Kochetkov E.V. Using program verification for detecting malware. Voprosy kiberbezopasnosti , 2016, no. 3, vol. 16, pp. 25-32.
- 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.
- Song F., Touili T. Efficient malware detection using model-checking. International Symposium on Formal Methods. Springer Berlin Heidelberg, 2012, pp. 418-433.
- 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.
- 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.
- Schneider F.B. Enforceable security policies. ACM Transactions on Information and System Security (TISSEC), 2000, vol. 3, no. 1, pp. 30-50.
- Feng H.H. et al. Formalizing sensitivity in static analysis for intrusion detection. Proc. IEEE Symposium on Security and Privacy, 2004, pp. 194-208.
- Basin D. et al. Enforceable security policies revisited. ACM Transactions on Information and System Security (TISSEC), 2013, vol. 16, no. 1, pp. 3-8.
- Feng H.H. et al. Anomaly detection using call stack information. Proc. IEEE Symposium on Security and Privacy, 2003, pp. 62-75.
- 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.
- Klark Je., Gramberg O., Peled D. Program models verification: Model Checking. Moscow, MCNMO, 2002, 416 p.
- Vel'der S.Je., Lukin M.A., Shalyto A.A., Jaminov B.R. Automata program verififcation. St. Petersburg, Nauka, 2011, 244 p.
- Russinovich M. E., Solomon D. A., Ionescu A. Windows internals. Pearson Education, 2012, 800 p.
- Gordeev A.V. Operating systems. Izdatel'skij dom "Piter", 2009, 412 p.
- Korotkov M.A., Stepanov E.O Fundamentals of formal logical languages. St. Petersburg, SPb GITMO (TU), 2003, 84 p.
- 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.
- Federal Service for Technical and Export Control. Information security threats database. URL: http://bdu.fstec.ru.
