Формальная модель функционирования процесса в операционной системе
Ключевые слова:
формальная модель процесса, model checking, вредоносное программное обеспечениеАннотация
В статье представлена формальная модель функционирования процесса в операционной системе, построенная на основе применения субъектно-объектного подхода к разделению основных элементов операционной системы. Особенностью представленной модели является высокоуровневая абстракция описания взаимодействия процесса с ресурсами операционной системы, что позволяет применить полученные на ее основе результаты к широкому классу аналогичных систем. Применение данной модели необходимо для совершения перехода от реального процесса к его формальной модели, позволяющей учитывать значимые свойства поведения процесса как на статическом этапе анализа бинарного исполняемого файла, так и на динамическом этапе контроля за его выполнением. Предложена структура системы безопасного исполнения программного кода, являющаяся расширенной композицией таких подходов к обнаружению вредоносного программного обеспечения, как применение метода формальной верификации «Model checking» и использования автомата безопасности для контроля за выполнением исследуемой программы. Применение данной системы позволит использовать в корпоративных информационно-вычислительных сетях только программное обеспечение, уровень доверия к которому подтверждается формальным математическим доказательством и непрерывным контролем за его функционированием.Литература
1. Krombholz K., Hobel H., Huber M., Weippl E. Advanced social engineering attacks // Journal of Information Security and Applications. 2015. vol. 22. pp. 113–122.
2. Бекбосынова А.А. Тестирование и анализ эффективности и производительности антивирусов // Теория и практика современной науки. 2015. № 5(5). С. 53–56.
3. 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.
4. Song F., Touili T. Efficient malware detection using model-checking // International Symposium on Formal Methods. Springer Berlin Heidelberg. 2012. pp. 418–433.
5. 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.
6. 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.
7. Козачок А.В., Кочетков Е.В. Обоснование возможности применения верификации программ для обнаружения вредоносного кода // Вопросы кибербезопасности. 2016. № 3(16). С. 25–32.
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 // Security and Privacy, 2004. Proceedings. 2004 IEEE Symposium on. IEEE. 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.
11. Feng H.H. et al. Anomaly detection using call stack information // Security and Privacy, 2003. Proceedings. 2003 Symposium on. IEEE. 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. Anderson B. et al. Graph-based malware detection using dynamic analysis // Journal in computer Virology. 2011. vol. 7. no. 4. pp. 247–258.
14. Devesa J. et al. Automatic Behaviour-based Analysis and Classification System for Malware Detection // ICEIS. 2010. vol. 2. pp. 395–399.
15. Козачок А.В., Бочков М.В., Фаткиева Р.Р., Туан Л.М. Аналитическая модель защиты файлов документальных форматов от несанкционированного доступа // Труды СПИИРАН. 2015. Вып. 6(43). С. 228–252.
16. Zhang B. et al. Malicious codes detection based on ensemble learning // International Conference on Autonomic and Trusted Computing. Springer Berlin Heidelberg, 2007. pp. 468–477.
17. Козачок А.В., Туан Л.М. Обоснование возможности применения неразличимой обфускации для защиты исполняемых файлов // В сборнике: Перспективные информационные технологии (ПИТ 2015) труды Международной научно-технической конференции. СГАУ. 2015. С. 269–272.
18. Preda M.D. et al. A semantics-based approach to malware detection // ACM SIGPLAN Notices. 2007. vol. 42. no. 1. pp. 377–388.
19. Козачок А.В., Мацкевич А.Г. Модификация структурного метода распознавания вирусов // Информация и безопасность. 2010. Т. 13. С. 33.
20. Jacob G., Debar H., Filiol E. Behavioral detection of malware: from a survey towards an established taxonomy // Journal in computer Virology. 2008. vol. 4. no. 3. pp. 251–266.
21. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking // M.: МЦНМО. 2002.
22. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ // СПб. Наука. 2011. 244 с.
23. Рябов О.А. Моделирование процессов и систем: Учебное пособие // Красноярск. 2008. 122 с.
24. Руссинович М., Соломон Д. Внутреннее устройство Microsoft Windows. 6-е изд. // СПб.: Питер. 2013. 800 с.
25. Гордеев А.В. Операционные системы: по направлению подгот. «Информатика и вычисл. техника» // Издательский дом «Питер». 2009.
26. Бабенко Л.К., Буртыка Ф.Б., Макаревич О.Б., Трепачева А.В. Обобщенная модель системы криптографически защищенных вычислений // Известия ЮФУ. Технические науки. 2015. № 5(166). C. 77–86.
2. Бекбосынова А.А. Тестирование и анализ эффективности и производительности антивирусов // Теория и практика современной науки. 2015. № 5(5). С. 53–56.
3. 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.
4. Song F., Touili T. Efficient malware detection using model-checking // International Symposium on Formal Methods. Springer Berlin Heidelberg. 2012. pp. 418–433.
5. 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.
6. 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.
7. Козачок А.В., Кочетков Е.В. Обоснование возможности применения верификации программ для обнаружения вредоносного кода // Вопросы кибербезопасности. 2016. № 3(16). С. 25–32.
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 // Security and Privacy, 2004. Proceedings. 2004 IEEE Symposium on. IEEE. 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.
11. Feng H.H. et al. Anomaly detection using call stack information // Security and Privacy, 2003. Proceedings. 2003 Symposium on. IEEE. 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. Anderson B. et al. Graph-based malware detection using dynamic analysis // Journal in computer Virology. 2011. vol. 7. no. 4. pp. 247–258.
14. Devesa J. et al. Automatic Behaviour-based Analysis and Classification System for Malware Detection // ICEIS. 2010. vol. 2. pp. 395–399.
15. Козачок А.В., Бочков М.В., Фаткиева Р.Р., Туан Л.М. Аналитическая модель защиты файлов документальных форматов от несанкционированного доступа // Труды СПИИРАН. 2015. Вып. 6(43). С. 228–252.
16. Zhang B. et al. Malicious codes detection based on ensemble learning // International Conference on Autonomic and Trusted Computing. Springer Berlin Heidelberg, 2007. pp. 468–477.
17. Козачок А.В., Туан Л.М. Обоснование возможности применения неразличимой обфускации для защиты исполняемых файлов // В сборнике: Перспективные информационные технологии (ПИТ 2015) труды Международной научно-технической конференции. СГАУ. 2015. С. 269–272.
18. Preda M.D. et al. A semantics-based approach to malware detection // ACM SIGPLAN Notices. 2007. vol. 42. no. 1. pp. 377–388.
19. Козачок А.В., Мацкевич А.Г. Модификация структурного метода распознавания вирусов // Информация и безопасность. 2010. Т. 13. С. 33.
20. Jacob G., Debar H., Filiol E. Behavioral detection of malware: from a survey towards an established taxonomy // Journal in computer Virology. 2008. vol. 4. no. 3. pp. 251–266.
21. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking // M.: МЦНМО. 2002.
22. Вельдер С.Э., Лукин М.А., Шалыто А.А., Яминов Б.Р. Верификация автоматных программ // СПб. Наука. 2011. 244 с.
23. Рябов О.А. Моделирование процессов и систем: Учебное пособие // Красноярск. 2008. 122 с.
24. Руссинович М., Соломон Д. Внутреннее устройство Microsoft Windows. 6-е изд. // СПб.: Питер. 2013. 800 с.
25. Гордеев А.В. Операционные системы: по направлению подгот. «Информатика и вычисл. техника» // Издательский дом «Питер». 2009.
26. Бабенко Л.К., Буртыка Ф.Б., Макаревич О.Б., Трепачева А.В. Обобщенная модель системы криптографически защищенных вычислений // Известия ЮФУ. Технические науки. 2015. № 5(166). C. 77–86.
Опубликован
2017-03-31
Как цитировать
Козачок, А. В., & Кочетков, Е. В. (2017). Формальная модель функционирования процесса в операционной системе. Труды СПИИРАН, 2(51), 78-96. https://doi.org/10.15622/sp.51.4
Раздел
Информационная безопасность
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
