Валидация и верификация

Безопасная система – и в особенности система, которая используется для обеспечения безопасности – должны быть доверенной. Однако что лежит в основе этого доверия? Что придает уверенность в том, что основные компоненты системы реализованы правильно и не подведут в критический момент? В предыдущей статье, посвященной безопасной ОС, этот вопрос вскользь упоминался, и, как и обещали, мы возвращаемся этой теме.

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

• Верификация – это процесс оценки того, насколько система (программа, устройство) по итогам некоторого этапа ее разработки соответствует условиям, заданным в начале этапа.
• Валидация – процесс оценки того, насколько система (программа, устройство) соответствует требованиям по ее назначению.

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

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

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

• Свойство безопасности формулируется как недостижение системой при любом ее исполнении некоторого (небезопасного) состояния. Иными словами, свойство гарантирует, что ничего «плохого» не произойдет (NB: именно в этом значении словосочетание «свойство безопасности» и используется до конца статьи).
• Свойство живости, напротив, гарантирует, что после конечного числа шагов система придет в некоторое определенное состояние – то есть непременно случится что-то «хорошее».

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

Для формализации описанных таким образом критериев часто используется аппарат классической или темпоральной логики, а для верификации – соответствующие языки. В частности, для классических условий довольно популярен Prolog, для темпоральных – языки Promela, SPIN. Но это далеко не единственный способ. Описание формальных условий поведения компьютерных программ и верификация относительно этих правил настолько специфичная и востребованная проблема, что в 1969 году была создана специальная формальная теория – алгоритмическая логика Хоара, предназначенная для дедуктивного доказательства правильности программ и способная приблизить сухие спецификации к семантике программ на императивных языках. В настоящее время выработан еще более жизненный подход к описанию критериев – в виде контрактных спецификаций программных интерфейсов.

Другая проблема – выбор и формализация объекта верификации. И несмотря на то, что верификация, казалось бы, процедура, состоящая в точном вычислении, при этом выборе нужно ориентироваться на требуемую степень уверенности в результате.

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

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

В реальных системах дело чаще всего обстоит не так, а значит, необходимо подвергать верификации собственно программное обеспечение². Здесь снова приходится принимать не одно решение. Что подвергать верификации – высокоуровневый программный или машинный код, принимать ли во внимание влияние программного окружения и как моделировать это окружение, рассматривать ли специфические зависимости выполнения низкоуровневых операций от аппаратной платформы. Выбор снова зависит от цели верификации и от требуемой степени доверия к результатам. Предположим, нужно показать отсутствие уязвимостей определенного вида (этот пример выбран потому, что условие вероятнее всего сводится к свойству безопасности). Тестирование и статический анализ кода путем поиска типовых опасных конструкций в высокоуровневом коде обычно не относят к методам формальной верификации, т.к. как правило они не позволяют добиться полноты анализа³. Для решения такой задачи методы верификации производят над конструкциями программного кода логические вычисления, целью которых является доказательство того факта, что на графе передачи управления программы ни один из возможных исполняемых фрагментов (с учетом всех нелинейных переходов) не является уязвимым к указанному способу эксплуатации. Дело за малым – сформировать соответствующий критерий в достаточно общем виде и выполнить эффективное вычисление всем объеме кода программы.

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

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

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

Верификация программного кода «в лабораторных условиях» может вызывать нарекания в том случае, если поведение кода в большой степени определяется его окружением. Неплохо, конечно, если система построена из слабо связанных компонентов с хорошо документированными интерфейсами – однако в реальных системах достаточно сложно предсказать влияние окружения на поведение отдельно взятого компонента. В этих случаях для оценки корректности системы приходится прибегать к анализу поведения параллельно работающих компонентов. Формальная проверка того, выполняется ли заданная логическая формула на модели системы, описывается в рамках метода, известного как Model checking. Этот метод аккумулирует существующие достижения в верификации систем и широко применяется по всему миру для проверки сложных аппаратных и программных комплексов. За работы, внесшие существенный вклад в его развитие, дважды вручалась премия Тьюринга (первый раз – в 1996 году Амиру Пнуели за «плодотворную работу по внедрению темпоральной логики в вычислительные науки, и за выдающийся вклад в верификацию программ и систем», и второй в 2007 году – ученым Кларку, Эмерсону и Сифакису «за их роль в развитии проверки на модели — высокоэффективную технику верификации программ, широко применяемую при разработке как программного, так и аппаратного обеспечения»). В настоящее время методы model checking применяются и за пределами верификации технических систем, для которых этот метод был изначально разработан.

При вручении премии Тьюринга президент ACM Стьюарт Фельдман сказал и методе Model checking: «Это великий пример того, как технология, изменившая промышленность, родилась из чисто теоретических исследований». Можно с уверенностью утверждать, что если будущее во всех областях жизни от устройств бытового назначения до критических инфраструктур за развитыми, умными и безопасными во всех смыслах технологиями, то методы V&V обеспечивают путь в это будущее.

В одной статье невозможно охватить все вопросы. Для заинтересовавшихся рекомендуем прочитать:

• Статью одного из отцов-основателей метода проверки на модели Эдмунда Кларка (Edmund M. Clarke «The Birth of Model Checking»).
• Глубже погрузиться в формальные основы метода можно при помощи замечательной книги профессора Ю.Г. Карпова «Model Checking».
• Изучить вопросы, связанные с формализацией требований безопасности и живости лучше всего на основе оригинальных работ, обзор которых можно найти в статье Ekkart Kindler «Safety and Liveness Properties: A Survey».
• Монография Ж.Теля «Введение в распределенные алгоритмы» представляет потрясающий по объему и содержанию труд по формальному представлению протоколов в сложных системах и обеспечению их корректной и надежной работы.

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

²Заметим, что верификация конфигурации и верификация программного обеспечения — не взаимозаменяемые меры. Если проверка программного кода гарантирует ожидаемое поведение программных компонентов, то проверка конфигурации обеспечивает выполнение политики безопасности при работе этих компонентов. >>

³Однако они могут служить для валидации программного кода. >>