Логика первого порядка для задания требований к безопасному программному коду
https://doi.org/10.15514/ISPRAS-2017-29(5)-8
Аннотация
В настоящее время вопросу защиты информации при проектировании и эксплуатации объектов критической информационной инфраструктуры уделяется особое внимание. Одним из распространенных подходов к обеспечению безопасности информации, обрабатываемой на объектах, при этом является создание изолированной программной среды. Безопасность среды обуславливается ее неизменностью. Однако эволюционное развитие систем обработки информации порождает необходимость запуска в данной среде новых компонентов и программного обеспечения при условии выполнения требований по безопасности. Наиболее важным при этом является вопрос доверия к новому программному коду. Данная работа посвящена разработке формального логического языка описания функциональных требований к программному коду, который позволит в дальнейшем предъявлять требования на этапе статического анализа и контролировать их выполнение в динамике.
Список литературы
1. Проект федерального закона от 06.12.2016 № 9198-П10 "О безопасности критической информационной инфраструктуры Российской Федерации". URL: http://asozd2.duma.gov.ru/main.nsf/(SpravkaNew)?OpenAgent&RN=47571-7&02 (дата обращения 14.03.2017).
2. Козачок А.В., Кочетков Е.В., Татаринов А.М. Обоснование возможности построения эвристического механизма распознавания вредоносных программ на основе статического анализа исполняемых файлов. Вестник компьютерных и информационных технологий, 2017, №. 3, c. 50-56. DOI: 10.14489/vkit.2017.03. pp.050-056.
3. Козачок А.В., Кочетков Е.В. Обоснование возможности применения верификации программ для обнаружения вредоносного кода. Вопросы кибербезопасности. 2016. № 3 (16). С. 25-32.
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. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Москва, 2002, изд-во МЦНМО, 416 с.
14. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ. Санкт-Петербург, 2011, изд-во Наука, 244 с.
15. Руссинович М., Соломон Д. Внутреннее устройство Microsoft Windows. 6-е изд. Санкт-Петербург, 2013, изд-во Питер, 800 с.
16. Гордеев А.В. Операционные системы: по направлению подгот. "Информатика и вычисл. техника". Санкт-Петербург, 2009, изд-во Питер, 416 с.
17. Коротков М.А., Степанов Е.О Основы формальных логических языков. Санкт-Петербург, 2003, изд-во СПб ГИТМО (ТУ), 84 с.
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. ФСТЭК "Банк данных угроз безопасности информации" URL: http://bdu.fstec.ru/ (дата обращения: 14.03.17).
Рецензия
Для цитирования:
Козачок А.В. Логика первого порядка для задания требований к безопасному программному коду. Труды Института системного программирования РАН. 2017;29(5):135-148. https://doi.org/10.15514/ISPRAS-2017-29(5)-8
For citation:
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
Послать статью по эл. почте 