Логико-аналитические методы контроля безопасности программ
При проведении анализа безопасности с помощью логико-аналитических методов (см. рис.2.5) строится модель программы и формально доказывается эквивалентность модели исследуемой программы и модели РПС. В простейшем случае в качестве модели программы может выступать ее битовый образ, в качестве моделей вирусов множество их сигнатур, а доказательство эквивалентности состоит в поиске сигнатур вирусов в программе. Более сложные методы используют формальные модели, основанные на совокупности признаков, свойственных той или иной группе РПС.
Формальная постановка задачи анализа безопасности логико-аналитическими методами может быть сформулирована следующим образом.
Рис.2.4. Схема анализа безопасности ПО с помощью контрольно-испытательных методов
Рис. 2.5. Схема анализа безопасности ПО с помощью логико-аналитических методов
Выбирается некоторая система моделирования программ, представленная множеством моделей всех программ - Z. В выбранной системе исследуемая программа представляется своей моделью М, принадлежащей множеству Z. Должно быть задано множество моделей РПС V={vi|i=1,...,N}, полученное либо путем построения моделей всех известных РПС, либо путем порождения множества моделей всех возможных (в рамках данной модели) РПС. Множество V является подмножеством множества Z. Кроме того, должно быть задано отношение эквивалентности определяющее наличие РПС в модели программы, обозначим его Е(x,y). Это отношение выражает тождественность программы x и РПС y, где x - модель программы, y - модель РПС, и y принадлежит множеству V.
Тогда задача анализа безопасности сводится к доказательству того, что модель исследуемой программы М принадлежит отношению E(M,v), где v принадлежит множеству V.
Для проведения логико-аналитического анализа безопасности про-граммы необходимо, во-первых, выбрать способ представления и получения моделей программы и РПС. После этого необходимо построить модель исследуемой программы и попытаться доказать ее принадлежность к отношению эквивалентности, задающему множество РПС.
На основании полученных результатов можно сделать заключение о степени безопасности программы. Ключевыми понятиями здесь являются "способ представления" и "модель программы". Дело в том, что на ком-пьютерную программу можно смотреть с очень многих точек зрения - это и алгоритм, который она реализует, и последовательность команд процессора, и файл, содержащий последовательность байтов и т.д. Все эти понятия образуют иерархию моделей компьютерных программ. Можно вы-брать модель любого уровня модели и способ ее представления, необхо-димо только чтобы модель РПС и программы были заданы одним и тем же способом, с использованием понятий одного уровня. Другой серьезной проблемой является создание формальных моделей программ, или хотя бы определенных классов РПС. Механизм задания отношения между программой и РПС определяется способом представления модели. Наиболее перспективным здесь представляется использование семантических графов и объектно-ориентированных моделей.
В целом полный процесс анализа ПО включает в себя три вида анали-за:
лексический верификационный анализ;
синтаксический верификационный анализ;
семантический анализ программ.
Каждый из видов анализа представляет собой законченное исследование программ согласно своей специализации.
Результаты исследования могут иметь как самостоятельное значение, так и коррелироваться с результатами полного процесса анализа.
Лексический верификационный анализ предполагает поиск распознавания и классификацию различных лексем объекта исследования (программа), представленного в исполняемых кодах. При этом лексемами являются сигнатуры. В данном случае осуществляется поиск сигнатур следующих классов:
сигнатуры вирусов;
сигнатуры элементов РПС;
сигнатуры (лексемы) "подозрительных функций";
сигнатуры штатных процедур использования системных ресурсов и внешних устройств.
Поиск лексем (сигнатур) реализуется с помощью специальных про-грамм-сканеров.
Синтаксический верификационный анализ предполагает поиск, распознавание и классификацию синтаксических структур РПС, а также по-строение структурно-алгоритмической модели самой программы.
Решение задач поиска и распознавания синтаксических структур РПС имеет самостоятельное значение для верификационного анализа программ, поскольку позволяет осуществлять поиск элементов РПС, не имеющих сигнатуры. Структурно-алгоритмическая модель программы необходима для реализации следующего вида анализа - семантического.
Семантический анализ предполагает исследование программы изучения смысла составляющих ее функций (процедур) в аспекте операционной среды компьютерной системы. В отличие от предыдущих видов анализа, основанных на статическом исследовании, семантический анализ нацелен на изучение динамики программы - ее взаимодействия с окружающей средой. Процесс исследования осуществляется в виртуальной операционной среде с полным контролем действий программы и отслеживанием алгоритма ее работы по структурно-алгоритмической модели.
Семантический анализ является наиболее эффективным видом анализа, но и самым трудоемким. По этой причине методика сочетает в себе три перечисленных выше анализа. Выработанные критерии позволяют разумно сочетать различные виды анализа, существенно сокращая время исследования, не снижая его качества.
