Формальная модель функционирования процесса в операционной системе

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