Глава 5. Формальная функциональная спецификация

В данной главе рассматривается второй этап процесса моделирования и верификации механизма управления доступом операционной системы, а именно разработка и верификация формальной функциональной спецификации ОО. Требования к этой работе сформулированы в компонентах доверия ADV_FSP.6 «Полная полуформальная функциональная спецификация с дополнительной формальной спецификацией» и ADV_SPM.1 «Формальная модель политики безопасности ОО»:

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

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

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

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

К сожалению, в практике промышленного программирования разработка строгих или формальных спецификаций выполняется крайне редко (хотя заметим, что разработчики микропроцессоров всегда создают как минимум строгие спецификации системы команд процессора). В случае ОС принципиальных технических трудностей для разработки спецификации системных вызовов нет. Полная формальная спецификация программного интерфейса ОС реального времени была разработана в 1994-1997 годах [48], в 2005-2010 годах были разработаны спецификации для ОС Windows [49] и для базового набора системных библиотек ОС Linux [50]. Все три проекта использовали близкие по идеологии техники спецификации, которые сводились к разработке программных контрактов в форме пред- и постусловий и/или описания ожидаемого поведения функций в форме некоторой исполнимой модели (в роли модели могла быть программа на языке спецификации или на некотором диалекте C или C#). Природа моделей, которые использовались в этих проектах, относится к классу так называемых моделей на основе состояний (state-based models). Такие модели состоят из набора операций (функций, событий), входом к которым служат некоторые данные (аргументы, фактические параметры), а выходом некоторый результат операции (значение функции). Также операции имеют доступ к некоторым глобальным структурам данных (состоянию). Результат операции зависит от состояния, в котором она вызывается. Кроме того, изменение данных состояния может быть частью результата, в таком случае говорят, в результате выполнения операции система перешла из одного состояния в другое.

По сути при разработке формальной спецификации МРОСЛ ДП-модели на Event-B мы использовали близкий подход. Таким же образом технически возможно с использованием уже известного нам инструментария разработать и формальную функциональную спецификацию системных вызовов ядра ОС Linux.

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

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

Таким образом, для доказательства соответствия между двумя спецификациями некоторой системы — между абстрактной спецификацией М1 и детальной спецификацией М2 (рис. 5.1) — достаточно показать, что между ними существует такое отношение уточнения R, что для каждого перехода между состояниями из спецификации М2, который ведет из некоторого состояния s в состояние s’, существует соответствующий переход в абстрактной спецификации М1 из абстрактного состояния \sigma в состояние \sigma' . При этом переход называется соответствующим, если выполняется соотношения R(s)=\sigma и R(s')=\sigma' .

σ σ′ s s′ Переход в абстрактной спецификации M1 Переход в детальной спецификации М2 R R

Рис. 5.1. Диаграмма отношения уточнения между абстрактной и детальной спецификациями

В общем случае доказывать требование соответствия для двух разных спецификаций одной системы достаточно трудно. По этой причине в методологиях и технологиях, которые развивали данный подход, вводились достаточно жесткие ограничения на то, как описываются новые уровни уточнения, т.е. правила детализации проектирования системы жестко ограничивались, чтобы предоставить возможность формальной проверки сохранения соответствия между более абстрактными и более детальными слоями проекта. Например, в методологии RAISE [51] нельзя было переопределять структуры данных, т. е. для каждого типа данных требовалось дать сразу полное и окончательное его описание, что для сложных и тем более развивающихся систем является очень неприятным ограничением. В Event-B нельзя изменять значения переменных, определенных ранее (на предыдущих уровнях уточнения). Хотя благодаря этому ограничению можно быть уверенным, что определенные и доказанные на прошлых уровнях инварианты будут выполняться и на всех последующих, оно существенно усложняет процесс планирования уровней уточнения при разработке спецификации.

Возвращаясь к доказательству соответствия между моделью политики безопасности и формальной функциональной спецификацией, мы должны показать существование отношения уточнения R между их состояниями и операциями, причем на уровне формальной функциональной спецификации за переход между состояниями отвечают системные вызовы, а на уровне модели политики безопасности — де-юре правила МРОСЛ ДП-модели. Однако оказывается, что в нашем случае построение соответствия является весьма непростой задачей. Если набор структур данных и пространство состояний формальной функциональной спецификации и можно рассматривать как расширение структур данных и пространства состояния МРОСЛ ДП-модели, то операции формальной функциональной спецификации — системные вызовы — не удается прямо отобразить на правила МРОСЛ ДП-модели. Далее на примере показывается, как можно решить данную проблему и построить соответствие в нашем случае.

5.1. Построение соответствия между системными вызовами и правилами МРОСЛ ДП-модели

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

Рассмотрим системный вызов open. Этот системный вызов реализуется функцией int open(const char *pathname, int flags), которая выполняет действия, необходимые для открытия файла. У функции open два параметра: строка pathname содержит путь до открываемого файла, а flags определяет вид доступа, который требуется получить — на чтение, на запись или на чтение и на запись одновременно. За это отвечают флаги O_RDONLY, O_WRONLY, O_RDWR. flags также может содержать дополнительные, необязательные флаги. Функция возвращает ассоциированный с файлом файловый дескриптор, который затем может использоваться в последующих системных вызовах (например, в read, write, lseek, fcntl).

Рассмотрим частный случай вызова open, при котором файл из параметра pathname не существует, а параметр flags содержит флаг O_WRONLY, что означает открытие файла на запись, и дополнительный флаг O_CREAT, что позволит создать файл. Если процесс, от имени которого вызывается open, обладает всеми нужным правами доступа, то open должен выполнить следующую цепочку действий:

  • разбор значений параметров;

  • проверка наличия необходимых для создания файла прав доступа — в рассматриваемом частном случае проверка проходит успешно;

  • получение доступа на запись к каталогу, в котором будет создан файл;

  • создание файла;

  • получение права доступа на запись к созданному файлу;

  • получение доступов к созданному файлу;

  • возвращение файлового дескриптора созданного и открытого на запись файла.

Каждое из этих действий определенным образом изменяет состояние формальной функциональной спецификации (ФСП). Например, действие «возврат файлового дескриптора» изменяет множество всех открытых данным процессом файловых дескрипторов. Можно заметить, что три действия — а именно действия «получение доступа на запись», «получение права доступа на запись» и «создание файла» — прямо соответствуют правилам перехода между состояниями МРОСЛ ДП-модели access_write, grant_rights и create_object. Если рассматривать состояние ФСП как расширение состояния МРОСЛ ДП-модели, то данные действия изменяют исключительно ту ее часть, которая является общей с состоянием МРОСЛ ДП-модели. Для доказательства соответствия и непротиворечивости достаточно показать, что данные действия не нарушают определенных в МРОСЛ ДП-модели инвариантов через доказательство наличия отношения уточнения между действиями системного вызова open и правилами МРОСЛ ДП-модели. Остальные действия (назовем их вспомогательными) изменяют исключительно переменные из расширенного, дополненного состояния, т.е. те переменные, аналогов которых нет в состоянии МРОСЛ ДП-модели, так что они никак не влияют на существование отношения уточнения. Для демонстрации непротиворечивости таких действий относительно МРОСЛ ДП-модели следует сформулировать инварианты, которые свяжут значения переменных дополненного состояния формальной функциональной спецификации и переменных общего с МРОСЛ ДП-моделью состояния, и затем показать их выполнимость. Например, в данном случае следует сформулировать инвариант, который свяжет файловый дескриптор, открытый на запись (переменная дополненного состояния), с полученным доступом на запись (переменная общего с МРОСЛ ДП-моделью состояния).

Конкретный путь выполнения, или конкретная последовательность действий, которая будет выполнена в результате вызова системного вызова open, зависит от контекста, в котором происходит вызов, а именно от текущего состояния ОС и значений параметров вызова. Если описать все возможные пути выполнения для каждого системного вызова, то доказательство того, что ФСП является непротиворечивой относительно МРОСЛ ДП-модели, может быть достигнуто за счет доказательства выполнимости инвариантов МРОСЛ ДП-модели и дополнительных связующих инвариантов при любом выполняемом внутри системного вызова действии. А для доказательства того, что ФСП является полной относительно МРОСЛ ДП-модели, необходимо показать, что каждое правило перехода системы из состояния в состояние МРОСЛ ДП-модели связано хотя бы с одним действием функциональной спецификации.

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

Разбор параметров pathname и flags Проверка наличия нужных прав доступа — права имеются Получение доступа на запись к родительскому каталогу Создание файла Получение прав доступа к созданному файлу Получение требуемого доступа Возвращение дескриптора файл не существует файл существует

Рис. 5.2. Графовая модель небольшого подмножества цепочек действий системного вызова open

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

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

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

5.2. Пример формализации функциональной спецификации

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

В соответствии с предлагаемым методом узлы графов системных вызовов, которые соответствуют правилам МРОСЛ ДП-модели (узел создания файла в open является правилом перехода системы из состояния в состояние create_object МРОСЛ ДП-модели), будут представлены в ФСП как уточнения описывающих эти правила Event-B событий. Оставшиеся вспомогательные узлы (такие как разбор параметров pathname и flags системного вызова open) будут представлены как вспомогательные события, изменяющие исключительно дополненное состояние ФСП, которое затем будет связано инвариантами с состоянием Event-B спецификации МРОСЛ ДП-модели. Используя средства языка Event-B, данные события затем будут объединены в виде цепочек, где цепочка является одним из возможных путей в представляющем системный вызов графе.

Покажем как это будет выглядеть на примере рассмотренного ранее частного случая обращения к системному вызову open, при котором файл с именем pathname не существует, параметр flags содержит флаги O_WRONLY и O_CREAT и у процесса, от имени которого вызывается open, есть все необходимые права доступа. Этому случаю в ФСП на Event-B будет соответствовать цепочка из восьми событий: open\_start \rightarrow open\_check\_p \rightarrow open\_write\_p \rightarrow open\_create \rightarrow open\_grant \rightarrow open\_check \rightarrow open\_write \rightarrow open\_finish , где:

  • в событии open_start находятся предусловия, описывающие разбор параметров системного вызова open и принимается решение, какое событие должно произойти следующим. В рассматриваемом частном случае открываемый файл не существует, так что следующим событием будет open_check_p. Если бы файл существовал, то следующим событием был бы open_check и в целом цепочка событий была бы другой;
  • в событии open_check_p осуществляется проверка наличия требуемых прав доступа — в данном примере у вызывающего open процесса все нужные права доступа имеются;
  • событие open_write является уточнением события access_write_entity Event-B спецификации МРОСЛ ДП-модели, которое описывает получение доступа на запись. В данном событии получается доступ на запись к каталогу, в котором будет создан файл;
  • событие open_create является уточнением события create_object из Event-B спецификации МРОСЛ ДП-модели, которое описывает создание нового объекта (файла);
  • событие open_grant является уточнением события grant_rights Event-B спецификации МРОСЛ ДП-модели, которое описывает получение прав доступа;
  • в событии open_check осуществляется проверка наличия требуемых прав доступа и принимается решение, какое событие должно произойти следующим. В данном случае требуется получить доступ на запись к созданному файлу, следовательно, следующим событием будет open_write;
  • событие open_write является уточнением события access_write_entity Event-B спецификации МРОСЛ ДП-модели, которое описывает получение доступа на запись;
  • событие open_finish в своем постусловии возвращает запрашиваемый файловый дескриптор.

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

fig53 open_start open_start open_check_p open_check_p open_start->open_check_p open_check open_check open_start->open_check open_finish open_finish open_start->open_finish open_error open_error open_start->open_error open_check_p->open_error open_write_p open_write_p access_write_entity open_check_p->open_write_p open_check->open_error open_read open_read access_read_entity open_check->open_read open_write open_write access_write_entity open_check->open_write open_write_p->open_error open_create open_create create_object open_write_p->open_create open_create->open_error open_grant open_grant grant_rights open_create->open_grant open_grant->open_check open_grant->open_error open_read->open_finish open_read->open_error open_read->open_write open_write->open_finish open_write->open_error

Рис. 5.3. Граф Event-B событий нескольких частных случаев системного вызова open

События ФСП, представляющие граф системного вызова open, изображены прямоугольниками; если событие вспомогательное, то в прямоугольнике показано только его имя, если же событие соответствует событию Event-B спецификации МРОСЛ ДП-модели, то в его прямоугольнике снизу показано имя уточняемого события.

Если формализовать все оставшиеся частные случаи, то полученный граф будет являться формальной спецификацией поведения системного вызова open. При этом благодаря использованию уточнения данная спецификация будет корректна по построению и полностью соответствовать правилам МРОСЛ ДП-модели, что в свою очередь будет означать, что при любом сочетании параметров и состояния системы выполнение системного вызова open сохранит все установленные в МРОСЛ ДП-модели требования и свойства. После этого останется только доказать выполнимость инвариантов, которые связывают дополненное состояние и состояние МРОСЛ ДП-модели. В результате формализации подобным образом всех системных вызовов будет получена формальная функциональная спецификация с доказанными свойствами непротиворечивости и полноты.