УДК 004.056.57

ФОРМАЛЬНАЯ МОДЕЛЬ ФУНКЦИОНИРОВАНИЯ ПРОЦЕССА В ОПЕРАЦИОННОЙ СИСТЕМЕ

А.В. Козачок, Е.В. Кочетков

Аннотация


В статье представлена формальная модель функционирования процесса в операционной системе, построенная на основе применения субъектно-объектного подхода к разделению основных элементов операционной системы. Особенностью представленной модели является высокоуровневая абстракция описания взаимодействия процесса с ресурсами операционной системы, что позволяет применить полученные на ее основе результаты к широкому классу аналогичных систем. Применение данной модели необходимо для совершения перехода от реального процесса к его формальной модели, позволяющей учитывать значимые свойства поведения процесса как на статическом этапе анализа бинарного исполняемого файла, так и на динамическом этапе контроля за его выполнением. Предложена структура системы безопасного исполнения программного кода, являющаяся расширенной композицией таких подходов к обнаружению вредоносного программного обеспечения, как применение метода формальной верификации «Model checking» и использования автомата безопасности для контроля за выполнением исследуемой программы. Применение данной системы позволит использовать в корпоративных информационно-вычислительных сетях только программное обеспечение, уровень доверия к которому подтверждается формальным математическим доказательством и непрерывным контролем за его функционированием.

Ключевые слова


формальная модель процесса; model checking; вредоносное программное обеспечение

Полный текст:

PDF

Литература


  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.


Александр Васильевич Козачок - к-т техн. наук, сотрудник, Академия Федеральной службы охраны Российской Федерации.
Область научных интересов: информационная безопасность, защита от несанкционированного доступа, математическая криптография, теоретические проблемы информатики.
Число научных публикаций: 80.

Адрес (E-mail): alex.totrin@gmail.com
Почтовый адрес: Приборостроительная, 35, Орел, 302034
Телефон: +7(486) 254-99-33


Евгений Викторович Кочетков - сотрудник, Академия Федеральной службы охраны Российской Федерации.
Область научных интересов: информационная безопасность, защита от несанкционированного доступа, защита от вредоносных программ, теоретические проблемы информатики.
Число научных публикаций: 10.

Адрес (E-mail): mr.Koch91@mail.ru
Почтовый адрес: Приборостроительная, 35, Орел, 302034
Телефон: +7(486) 254-99-33




DOI: http://dx.doi.org/10.15622/sp.51.4