Цели проекта и пути их достижения

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

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

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

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

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

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

Первой из «наших» фаз является фаза определения требований к системе. Далее также будут рассмотрены фазы проектирования (на уровне системы и на уровне подсистем и моделей) и фазы верификации и сертификации.

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

Опыты использования формальных методов в реальных программистских проектах проводятся уже около сорока лет. В целом можно сказать, что проекты удачны тогда, когда система имеет не слишком большой размер и в действительности является важной и ответственной. Самими известными относительно крупными и при этом успешными примерами применения формальных методов являются такие системы как микроядерная операционная система seL4 [1] (около 10 тыс. строк) и модель системы управления в парижском метро [2] (несколько больше 100 тыс. строк). Однако часто ответственные системы оказываются очень большими. Простейший пример ядро ОС Linux – это примерно 20 млн. строк кода на Си. Что делать в этом случае?

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

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

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

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

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



[1] Klein G. et al. seL4: Formal Verification of an OS Kernel // Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, ACM, 2009.

[2] Abrial J.-R. Modeling in Event-B: System and Software Engineering. — Cambridge University Press, 2010.

Пример многоуровневой модели

Аннотированный пример многоуровневой формальной модели