Формальные методы анализа систем

Для лучшего понимания принципов, используемых при создании формальных политик безопасности, рассмотрим основные математические методы, применяемые при формальном анализе и формальном описании политик безопасности систем. При анализе функционирования систем, область применения которых является критичной , желательно рассмотреть все возможные поведения системы, то есть ее реакции на все возможные входные данные.

Хотя количество "всех возможных" реакций системы слишком велико для исследования, существует два метода, позволяющих уменьшить количество реакций, которые необходимо рассмотреть.

Один из методов заключается в доказательстве того, что система всегда "работает корректно", тогда как другой заключается в демонстрации того, что система никогда не выполняет неверных действий.

При использовании первого метода используется комбинация анализа и эмпирического тестирования для определения таких реакций системы, которые могут привести к серьезным сбоям - например функционирование системы при граничных условиях или при условиях, не оговоренных в качестве возможных для компонентов системы. В качестве примера можно привести требование описания поведения системы в ответ на входное воздействие "выключение питания".

Основной идеей второго метода является гипотеза о том, что система делает что-то некорректное, поэтому ведется анализ реакций системы с выявлением состояний, в которых возможно проявление данной некорректности. Доказательство корректности работы системы сводится к демонстрации того, что данные состояния недостижимы, то есть к доказательству от противного.

Свойство, характерное как для одной, так и для другой техники анализа безопасности системы, выражается следующим образом: данные техники анализа обеспечивают пути группирования "схожих" реакций системы так, что для рассмотрения всех возможных реакций системы необходимо рассмотреть лишь небольшое количество входных воздействий.

К сожалению, данные методы анализа безопасности систем пригодны в основном для систем, основывающихся на механических, электрических и других компонентах, то есть компонентах, основанных на физических принципах действия. В системах, основанных на физических принципах, отношения между входными и выходными данными являются «непрерывными», то есть незначительные изменения во входных данных влекут незначительные изменения в выходных данных. Это позволяет проанализировать (протестировать) поведение системы, основанной на физических законах конечным количеством тестов, так как непрерывный характер правил функционирования системы позволяет заключить, что отклик системы на непротестированное значение входной величины будет схожим с соответствующими протестированными случаями.

Таким образом, можно сделать вывод о том, что метод непосредственного тестирования хотя и необходимо применять к системам критического назначения, но он способен детектировать только примитивные ошибки в программном обеспечении. Вследствие сложности современных программных систем и вытекающего из этого многообразия реакций системы на входной поток данных, описанная выше техника не достаточна для анализа сложной программной системы.

Сложность программной системы определяется большим количеством дискретных решений, принимаемых системой при исполнении программного обеспечения. Таким образом, при определении взаимоотношений между входом и выходом системы (входным и выходным потоками данных), в случае анализа программной системы, реакцию системы на входное воздействие нельзя рассматривать как непрерывную функцию, так как она является дискретной: небольшие изменения во входных данных системы могут радикально изменить поведение всей системы в целом. Это является главным отличием современных программных систем от систем, основанных на физических процессах.

Отклонение от непрерывности ведет к катастрофическому росту количества возможных реакций системы на изменения во входных данных. Таким образом, в случае с программными системами метод непосредственного тестирования с последующими выводами о свойствах системы (то есть описание всех возможных реакций системы на входной поток данных) не дает должной уверенности вследствие дискреционного характера отношений между входными данными и выходной реакцией системы (нельзя сказать, что небольшие изменения во входных данных системы приведут к сходной ее реакции). При непосредственном тестировании систем, содержащих программное обеспечение, можно говорить только о вероятностных, но не определенных результатах тестирования.

Исходя из описанных выше недостатков использования непосредственного тестирования при анализе сложных программных систем, выясняется необходимость применения другой техники анализа, то есть формальных методов.

В области программного обеспечения, в отличие от анализа систем, использующих физические принципы, вместо дифференциальных уравнений используются понятия дискретной математики, такие как "множества", "графы", "частичный порядок", "машина конечных состояний" и т.д. "Вычисления" при описании данных систем базируются на методах формальной логики, а не на численном анализе. Это происходит потому, что результаты, интересующие при анализе системы, являются логическими свойствами. Математическая логика обеспечивает методы доказательства свойств больших или бесконечных множеств связанных сущностей на конечный манер на основе методов, сходных с методом математической индукции.

При формальном анализе системы, для того чтобы сделать выводы о ее логических свойствах, исходя из определенных структур дискретной математики, необходимо начать с аксиом, описывающих данные структуры, и правил манипуляции символами, соответствующими данным структурам. Процесс манипулирования символами называется формальной дедукцией, так как корректность процесса зависит от формы символических выражений, но не от их семантического смысла.

Практическое значение применения формальных методов при анализе систем заключается в возможности анализа всех реакций сложной программной системы. Рассмотрим причины, по которым возможно сделать вышеприведенное заключение.

Прежде всего, необходимо отметить, что в случае формального анализа мы имеем дело не просто с реакцией системы на некоторые группы входных данных, а с внутренней реализацией системы. Таким образом, возникает возможность "декомпозиции" возможных реакций системы на реакции ее компонентов (с помощью анализа формальных спецификаций компонентов) с последующей их композицией, что дает возможность описания всех реакций системы.

С другой стороны, формальные методы позволяют провести логическое вычисление причин корректности систем с программным обеспечением. Данное утверждение можно пояснить следующим образом. Программное обеспечение пишется для того, чтобы система выполняла некоторую полезную работу, то есть достигала какой-то цели (желаемая реакция системы). Если можно записать данную цель, то возможно сконструировать аргументы, поясняющие уверенность в том, что система с программным обеспечением функционирует корректно. Формальные методы позволяют уменьшить количество аргументов, необходимых для логического вычисления утверждения о корректности работы системы.

Для автоматизации процесса доказательства свойств системы используются "доказатели теорем" - программное обеспечение, проводящее формальную дедукцию на основе комбинации эвристик и непосредственного поиска. Другим видом программного обеспечения, используемого при формальном анализе систем, являются "контроллеры доказательств", программы, предоставляющие пользователю проводить последовательность шагов в процессе логических выводов о свойствах системы, но проверяющие корректность каждого шага.

Естественно, самыми эффективными средствами формального анализа являются средства, сочетающие в себе свойства двух приведенных выше видов программного обеспечения.

Описанные выше принципы применения формальных методов для анализа систем, содержащих программное обеспечение, имеют недостаток, присущий всем методам моделирования: формальные методы имеют дело не с самой системой, а с ее моделью. Это означает, что модель может не отражать реальность или отражать ее некорректно.

Данная проблема может возникнуть вследствие использования модели, учитывающей не все факторы, оказывающие влияние на реальную систему. С другой стороны, излишняя подробность описания системы ведет к резкому росту временных затрат на проведение формального анализа, что может привести к неэффективности применения данного метода. К модели безопасности должны предъявляться требования, общие для всех моделей:

— адекватность;

— способность к предсказанию;

— общность.

Таким образом, возникает задача корректного выбора уровня абстракции в описании модели безопасности. Под уровнем абстракции понимается множество требований к реальной системе, которые должны найти свое отражение в модели, для корректного отображения моделируемой системы.