Аннотация:
В настоящей статье представлен комплекс алгоритмов, составляющих основу функционирования системы безопасного исполнения программного кода. Функциональным предназначением данной системы является проведение исследования произвольных исполняемых файлов операционной системы в условиях отсутствия исходных кодов с целью обеспечения возможности контроля исполнения программного кода в рамках заданных функциональных требований. Представленный в работе комплекс алгоритмов включает в себя: алгоритм функционирования системы безопасного исполнения программного кода и алгоритм построения модели программы, пригодной для проведения верификации и сохраняющей свойства исходной программы.
Ключевые слова:алгоритм, вредоносное программное обеспечение, model checking, security automata.