Описание основ сертификации и верификации программного обеспечения

ГРАНДИОЗНЫЙ ВЫЗОВ

Решение проблемы верифицированного программного обеспечения превратилось в амбициозную международную долгосрочную исследовательскую программу, направленную на получение существенных объемов полезного кода, формально проверенного в соответствии с самыми высокими стандартами строгости и точности. Эту программу инициировал Энтони Хоар, обратив внимание ИТ-сообщества на «грандиозный вызов» — необходимость разработки целостного автоматизированного набора инструментов для проверки корректности программного обеспечения. В феврале 2005 года в Менло-Парке (Калифорния) был проведен симпозиум по верифицированному программному обеспечению, а в октябре того же года в Цюрихе состоялась конференция IFIP «Верифицированное программное обеспечение: теории, инструменты и эксперименты». Программа исследований рассчитана на 15 лет и призвана продемонстрировать применимость формальной технологии верификации при промышленной разработке программного обеспечения. У нее три основные цели:

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

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

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

ОБЪЕДИНЕННЫЙ ПЛАН ИССЛЕДОВАНИЙ

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

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

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

РЕПОЗИТАРИЙ ВЕРИФИЦИРОВАННЫХ ПРОГРАММ

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

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

Репозитарий будет играть роль оси, вокруг которой вращается колесо проекта. Именно здесь будут проводиться эксперименты, продвигающие теоретические и технологические инновации. Силой, вращающей колесо, станет сообщество исследователей, мотивируемое сложностью проблем. Несколько достойных внимания задач уже предложено, в частности верификация Web-сервера Apache, эталонных реализаций стека TCP/IP и ядра Linux.

ВЕРИФИКАЦИЯ ДЛЯ MONDEX

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

Mondex представляет собой электронный кошелек на базе смарт-карты, удовлетворяющий стандарту безопасности ITSEC уровня E6 (Information Technology Security Evaluation Criteria).

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

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

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

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

Абстрактная спецификация политики безопасности составляет примерно 20 страниц на языке Z. Детальная спецификация системы, включая n-шаговый протокол перемещения денежных средств, занимает около 60 страниц. Верификация, представленная на уровне детализации, пригодном для внешней оценки, занимает приблизительно 200 страниц доказательства уточнений плюс еще 100 страниц вывода отдельных правил уточнения, необходимых для проекта. Поскольку доказательство разрослось до нескольких сотен страниц, Степни и Куперу пришлось тщательно его структурировать, чтобы сделать понятным для всех заинтересованных лиц. Различные группы, работающие сейчас с Mondex, весьма высоко оценили эту структуру.

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

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

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

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

За решение проблемы Mondex взялись несколько групп. Они предложили использовать следующие формализмы: Alloy (Массачусетский технологический институт); Event-B (Университет Саутгемптона); Object Constraint Language (Бременский университет); Perfect Developer (компания Escher Technologies); Rigorous approach to industrial software engineering, или Raise (Университет ООН в Maкao и Датский технический университет); а также Z (Университет Йорка). Члены групп согласились в течение одного года работать без финансирования. Отдельная группа в Университете Аугсбурга работала над верификацией, используя верификатор KIV (Karlsruhe interactive verifier) и абстрактные конечные автоматы (abstract state machine, ASM).

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

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

Z в Йорке

В Университете Йорка над проблемой Mondex мы работали, используя программу автоматического доказательства теорем Z/Eves. Наша главная цель как археологов состояла в том, чтобы автоматизировать все доказательства при максимальном сохранении исходной формализации.

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

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

Доказательство корректности описания протоколов Mondex требует доказательства приблизительно 140 условий верификации, и трудность этих доказательств изменяется в довольно широких пределах. Для доказательства каждого условия верификации требуется в среднем около пяти шагов. Поскольку программа Z/Eves имеет множество встроенных средств автоматизации, некоторые шаги не требуют особого вмешательства в ее работу. Другие части доказательств повторяют шаги из предыдущих доказательств, которые с некоторым трудом могут быть вынесены в леммы общего характера. Для некоторых промежуточных шагов необходимо знакомство с внутренними механизмами Z/Eves, в то время как другие требуют творческого отношения и знания предметной области, например создания экземпляров квантифицированных переменных. Наконец, процесс нуждается в некоторых общетеоретических результатах, затрагивающих конструкции языка (главным образом касающихся cходимости), которые иногда трудно доказать. В целом понадобилось приблизительно 200 тривиальных шагов, 400 шагов средней сложности и 100 шагов, требующих творческого подхода.

Работа позволила выявить несколько дефектов.

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

Raise в Макао и в Датском техническом университете

Крис Джордж из Университета ООН в Макао и Энн Акстаузен из Датского технического университета использовали метод Raise и его язык спецификаций RSL, которые сложились под влиянием метода разработки Vienna и языков CSP (Communicating Sequential Processes) и ACT-ONE. Разработчики использовали RSL для описания абстрактных спецификаций высокого уровня и низкоуровневых проектов, включая явные управляющие конструкции императивного программирования типа циклов. Для верификации спецификаций RSL их транслировали в систему верификации прототипов (prototype verification system, PVS).

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

Текущая спецификация является десятым вариантом, она содержит около 2200 строк RSL в 13 файлах с 366 доказательствами, половина из которых была выполнена автоматически. Некоторые доказательства были особенно трудны. Типичное доказательство инварианта для детального уровня содержит приблизительно 300 команд программы автоматического доказательства (имеются 11 из этих доказательств). Доказательство того, что инвариант на детальном уровне заключает в себе абстрактный инвариант, было достаточно сложным (150 команд). Вызвало затруднения также доказательство конечности некоторых множеств, заданных свойствами своих элементов. Со схожими проблемами столкнулась и группа Z/Eves.

Большое количество переделок в моделях было обусловлено особенностями исходного проекта Mondex. Начиная заново, группа RSL не воспользовалась деталями, тщательно проработанными в первоначальном проекте.

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

В моделях RSL есть много объемных доказательств со сходными структурами, и это наводит на мысль о вынесении их в общие леммы. На первый взгляд, кажется целесообразным обобщить типичное доказательство, но выработать хороший план многократного использования доказательств довольно трудно. Одна опрометчивая команда grind в PVS в конечном счете генерирует 1580 подцелей.

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

Perfect Developer компании Escher Technologies

Английская компания Escher Technologies предпочла использовать Perfect Developer (PD), инструмент для строгой разработки компьютерных программ, начиная с формальной спецификации и уточняя ее до уровня кода. PD поддерживает парадигму структурной корректности (correctness-by-construction), в которой интерфейсы компонентов проверяются с помощью статического анализа, что гарантирует их строгое соответствие своим контрактам во время выполнения. В этой работе использовался язык Perfect Specification Language, который имеет объектно-ориентированный стиль и генерирует код на Java и C++.

Дэвид Крокер из компании Escher хотел полностью в автоматическом режиме провести доказательство корректности проекта Mondex и получить его реализацию на языке Java. Кроме того, он намеревался разобраться, как в Perfect Developer лучше всего представить спецификации на системном уровне, и преодолеть возможные ограничения программы автоматического доказательства. Такие намерения определенно характеризуют его как технолога, хотя и заметно, что спецификации для Perfect Developer получены путем перевода исходных Z-спецификаций. Тем не менее модель получилась вполне адекватной. Поскольку доказательства в PD полностью автоматизированы, то их подробности скрыты от пользователя, и, следовательно, они могут не совпадать с доказательствами в исходном проекте.

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

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

В настоящее время PD генерирует 213 условий верификации и автоматически доказывает 191 из них. Некоторые из 22 недоказанных условий верификации фактически являются требованиями к среде; другие возникают из-за ограничений программы доказательства. Описание модели составляет около 550 строк на языке Perfect Specification Language, и доказательство занимает приблизительно шесть часов. PD проверяет все результативные условия верификации меньше чем за шесть минут. На работу над проектом группа затратила около 60 часов.

KIV в Аугсбурге

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

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

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

Наличие почти корректного отношения уточнения помогло закончить работу за четыре недели. Обычно поиск инвариантов и последовательное уточнение отношений отнимает больше времени, чем проверка корректности решения. С другой стороны, группа уверена в том, что применение конечных автоматов в уточнении сократило бы время верификации. Основные доказательства уточнения данных для Mondex состоят из 1839 шагов с 372 взаимодействиями.

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

СЛЕДУЮЩИЕ ШАГИ

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

За ним последует ряд более сложных и разносторонних экспериментальных проектов. Идеальный экспериментальный проект имеет ряд характерных черт.

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

Раджив Джоши и Джерард Хольцман из Лаборатории реактивного движения НАСА в качестве следующего экспериментального проекта предложили поддающееся верификации хранилище файлов. Эта проблема имеет все признаки идеального экспериментального проекта. Действительно, многие широко используемые и тщательно проверенные файловые системы все еще содержат серьезные ошибки, которые могут привести к тяжелым последствиям, вплоть до удаления корневого каталога. Кроме того, большинство современных файловых систем соответствуют стандарту POSIX и используют хорошо известные алгоритмы и структуры данных; это позволяет надеяться, что небольшая группа сумеет завершить работу над проектом за два года. Далее, поскольку большая часть электронных данных хранится в файловых системах, корректность этих систем имеет большое значение при использовании компьютеров. Существует множество открытых источников документации по современным файловым системам. Наконец, исследователи могут подходить к проекту с разных сторон: можно проектировать новую файловую систему на пустом месте, используя уточнение, или верифицировать существующую файловую систему с открытым исходным кодом. В равной степени применимы как проверка модели, так и доказательство теорем.

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

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

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

Джоши и Хольцман работают над долгосрочной задачей построения надежного программного обеспечения с использованием автоматизированных инструментов верификации, отказавшись от традиционных процессов разработки, специально подбираемых для каждого конкретного случая. Частью этой задачи является построение надежной файловой системы с использованием флэш-памяти в качестве энергонезависимого хранилища на борту будущих космических кораблей. Флэш-память удобна для этой цели, поскольку не имеет движущихся частей, потребляет мало энергии, легко доступна и уже использовалось в нескольких последних миссиях НАСА, таких как Mars Exploration Rover и Deep Impact. Однако построение надежной файловой системы для флэш-памяти является нетривиальной задачей.

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

В отрасли растет понимание того, что с надежностью программного обеспечения надо что-то делать. Билл Джой, один из основателей компании Sun Microsystems, сказал: «Есть еще несколько вещей, которые я хочу осуществить. Я по-прежнему считаю, что наши инструменты совершенно неадекватны проблеме построения надежных программ». Документ The International Technology Roadmap for Semiconductors, в котором дается оценка отраслевых технологических требований, призван способствовать непрерывному повышению производительности интегральных схем. В его выпуске от 2005 года утверждается, что «без крупных прорывов верификация останется непреодолимым барьером на пути прогресса в индустрии полупроводников».

Технологии и инструменты

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

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

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

Инструментов тестирования так же много, как и языков программирования. В табл. 1 приведены основные средства тестирования для первой десятки наиболее популярных языков программирования (согласно рейтингу Tiobe).

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

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

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

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

Средства непрерывной верификации и валидации. Принцип непрерывного обеспечения качества предполагает тесную интеграцию процессов верификации и валидации на всех этапах разработки. Типичный пример — разработка с ориентацией на тестирование: плановые показатели качества задаются еще до разработки ПО. С учетом преимуществ непрерывной интеграции, одной из основ DevOps, все большее значение придается инструментам, помогающим не только автоматизировать верификацию и валидацию, но и интегрировать эти процессы в цикл разработки. Перечисленные в табл. 6 инструменты позволяют проверять характеристики качества в рамках сред непрерывной интеграции Jenkins, Travis CI, Bamboo, GoCD, Ansible и т. Требуется встроить валидацию и верификацию в жизненный цикл ПО, обеспечив автоматическое, прозрачное для разработчиков выполнение соответствующих процессов. Представленные в табл. 6 инструменты проверяют несколько характеристик качества и позволяют получить данные для глобальной оценки и визуализации. В рамках процессов непрерывной верификации и валидации также могут применяться инструменты модульного тестирования, фиксации и замены и статического анализа.

Для управления действиями, выполняемыми при помощи всех перечисленных видов инструментов, и контроля над процессом верификации и валидации в целом, применяются средства управления тестовыми случаями: Test Link, Test Rail, Microfocus Quality Center, VSTS, IBM Rational Quality Manager, XStudio и др.

Перспективы

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

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

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

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

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

Аристотель говорил: «Совершенство — это не действие, а привычка». Широкий выбор инструментов — это важно, но главное — создание культуры обеспечения качества ПО и приобретение соответствующих навыков.

Fitzgerald, K. Stol. Continuous software engineering: A roadmap and agenda // J. Syst. Softw. — 2017 (Jan). — Vol. 123. — P. 176–189.

Как проводится сертификация?

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

• Заявитель (разработчик либо другая компания, заинтересованная в проведении сертификации) подает в федеральный орган (ФСБ, ФСТЭК или Минобороны) по сертификации заявку на проведение сертификационных испытаний некоторого продукта.
• Федеральный орган определяет аккредитованную испытательную лабораторию и орган по сертификации.
• Испытательная лаборатория совместно с заявителем проводит сертификационные испытания. Если в процессе испытаний выявляются те или иные несоответствия заявленным требованиям, то они могут быть устранены заявителем в рабочем порядке, что и происходит в большинстве случаев, либо может быть принято решение об изменении требований к продукту, например о снижении класса защищенности. Возможен вариант, когда сертификационные испытания завершаются с отрицательным результатом. Наиболее нашумевшим в прессе примером можно назвать случай, когда испытательная лаборатория НИИ ВМФ после года проверок выдала отрицательное сертификационное заключение на программные изделия специального назначения. Известны как минимум пять случаев, когда определенные версии ОС и СУБД не смогли получить сертификат на отсутствие недекларированных возможностей по причине потери части исходного кода старых модулей. Если посмотреть реестр ФСТЭК, то можно заметить, что ряд программных систем защиты (например, СУБД Oracle и система безопасности приложений IBM Guardium) получили сертификаты лишь на соответствие ТУ, а не на соответствие руководящему документу Гостехкомиссии — это значит, что орган по сертификации посчитал, что не все требования руководящего документа подтверждены при испытаниях.
• Материалы испытаний передаются в орган по сертификации, который проводит их независимую экспертизу. Как правило, в экспертизе участвуют не менее двух экспертов, которые независимо друг от друга подтверждают корректность и полноту проведения испытаний.
• Федеральный орган по сертификации на основании заключения органа по сертификации оформляет сертификат соответствия. Надо сказать, что в случае выявления каких-либо несоответствий федеральный орган может провести дополнительную экспертизу с привлечением экспертов из различных аккредитованных лабораторий и органов.

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

Системы сертификации и требования

Деятельность российских систем сертификации в РФ регламентируется Федеральным законом № 184 «О техническом регулировании». Сертификация средств защиты информации может быть добровольной или обязательной — проводимой главным образом в рамках Минобороны, ФСБ и ФСТЭК. Для большинства коммерческих компаний термин «сертификация» является синонимом понятий «сертификация в системе ФСБ» для криптографических средств защиты и «сертификация в системе ФСТЭК» для всех остальных продуктов. Однако необходимо иметь в виду, что, помимо криптографии, к компетенции ФСБ относятся средства защиты информации, применяемые в высших органах государственной власти. Система сертификации средств защиты информации Минобороны, в свою очередь, ориентирована на программные изделия, применяемые на объектах военного назначения.

Добровольные системы сертификации средств защиты информации на сегодняшний день пока еще не получили широкого распространения. Единственной сколь бы то ни было заметной из такого рода систем является «АйТи-Сертифика». К сожалению, несмотря на то что в добровольных системах можно получить сертификат на соответствие любому нормативному документу по защите конфиденциальной информации, при аттестации объектов информатизации такие сертификаты ФСТЭК России не признаются.

Что касается документов, на соответствие которым проводятся сертификационные испытания, то они практически идентичны во всех системах сертификации. Существуют два основных подхода к сертификации – и соответственно два типа нормативных документов.

• Функциональное тестирование средств защиты информации, позволяющее убедиться в том, что продукт действительно реализует заявленные функции. Это тестирование чаще всего проводится на соответствие конкретному нормативному документу – например, одному из руководящих документов Гостехкомиссии России. Такие документы установлены, например, для межсетевых экранов и средств защиты от несанкционированного доступа. Если же не существует документа, которому сертифицируемый продукт соответствовал бы в полной мере, то функциональные требования могут быть сформулированы в явном виде – например, в технических условиях, или в виде задания по безопасности (в соответствии с положениями стандарта ГОСТ Р 15408).
• Структурное тестирование программного кода на отсутствие недекларированных возможностей. Классическим примером недекларированных возможностей являются программные закладки, которые при возникновении определенных условий инициируют выполнение не описанных в документации функций, позволяющих осуществлять несанкционированные воздействия на информацию (по ГОСТ Р 51275-99). Выявление недекларированных возможностей предполагает проведение серии тестов исходных текстов программ, предоставление которых является необходимым условием для возможности проведения сертификационных испытаний.

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

Мифология вокруг сертификации

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

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

Миф №2: сертификацию проводят государственные органы. Безусловно, федеральные органы всех обязательных систем сертификации являются государственными, однако испытательные лаборатории и органы по сертификации могут иметь любую форму собственности, и на практике большинство из них – коммерческие организации.

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

Миф № 4: сертификация нужна только госструктурам. На самом деле конечного заказчика интересует аттестация объекта информатизации – формальное подтверждение того, что автоматизированная система является защищенной. В большинстве случаев для успешного прохождения аттестации система должна строиться с использованием исключительно сертифицированных средств защиты – это справедливо не только для систем, относящихся к государственному информационному ресурсу, но и для систем, связанных с обработкой персональных данных. Можно встретить требования по обязательной сертификации программной продукции даже независимо от вида защищаемых тайн; например, такие требования имеются для систем, работающих с кредитными историями граждан, игровых систем в случаях предоставлении доступа к ресурсам из сетей международного обмена и др.

Миф № 5: зарубежный продукт нельзя сертифицировать. В действительности продукты таких разработчиков, как Microsoft, IBM, SAP, Symantec, Trend Micro и т. , успешно проходят сертификационные испытания, в том числе и на отсутствие недекларированных возможностей.

Как правило, зарубежные компании не передают исходные тексты в Россию, поэтому испытания проводятся с выездом к разработчику. Разумеется, программные коды предоставляются под абсолютным контролем служб безопасности разработчиков, исключающих какую-либо утечку. Проведение работ в таком режиме является довольно сложным и требует высокой квалификации специалистов, поэтому не каждая испытательная лаборатория готова предложить такие услуги. Однако число зарубежных продуктов, проходящих сертификацию в России, с каждым годом увеличивается. Сегодня около 20 зарубежных компаний, в том числе Microsoft, IBM, Oracle и SAP, предоставили исходные коды своих продуктов для сертификационных испытаний. В этом отношении примечательна инициатива корпорации Microsoft — Government Security Program, согласно которой базовый код всех продуктов компании передан на территорию России для исследования. За последние пять лет почти 40 зарубежных продуктов получили сертификаты на отсутствие недекларированных возможностей.

Миф № 6: сертифицирован – значит защищен. Это не совсем так. Правильной была бы формулировка: продукт сертифицирован – значит соответствует тем или иным требованиям. При этом потребитель должен четко понимать, на соответствие чему именно сертифицировано средство защиты, чтобы убедиться, действительно ли в ходе проведения испытаний проверялись характеристики продукта, которые интересуют заказчика.

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

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

Миф № 7: при сертификации ничего не находят. Независимо от требований нормативных документов, сегодня сложилось негласное правило, по которому в рамках сертификационных испытаний эксперты тщательно инспектируют исходный код (в случае его предоставления), а также проводят различные варианты нагрузочного тестирования. Кроме того, эксперты изучают различные бюллетени по безопасности продуктов и сред их функционирования. В результате этого опытная лаборатория получает список критических уязвимостей, которые заявитель должен исправить или описать в документации. Например, при сертификации выявляются такие уязвимости, как встроенные пароли и алгоритмы их генерации, архитектурные ошибки (некорректная реализация дискретного и мандатного принципов доступа и т. ), некорректности программирования (уязвимости к переполнению буфера, ошибки операторов логики и времени, гонки, возможность загрузки недоверенных файлов и др. ), а также ошибки обработки данных приложений (SQL-инъекции, кросс-сайтовый скриптинг), реализация которых может существенно снизить уровень безопасности системы. Согласно нашей практике, в 70% проверенного коммуникационного оборудования обнаруживались встроенные мастер-пароли, а почти в 30% проверяемых операционных систем были выявлены ошибки реализации системы разграничения доступом. Зафиксированы также случаи, когда в продуктах присутствовали даже логические временные бомбы.

Миф № 8: продукт сертифицирован на отсутствие недекларированных возможностей – значит в нем нет уязвимостей. На сегодняшний день нет методов гарантированного выявления всех возможных уязвимостей программного обеспечения — успешное прохождение сертификации на отсутствие недекларированных возможностей гарантирует обнаружение лишь определенного класса уязвимостей, выявляемых с использованием конкретных методов. С другой стороны, прохождение сертификации на отсутствие недекларированных возможностей гарантирует наличие у разработчика системы качества производства программ, то есть найдены и зафиксированы все реальные исходные тексты и компиляционная среда, компиляция и сборка могут быть гарантировано повторены, а также имеется русскоязычная документация.

Миф № 9: требования по анализу исходного кода существуют только в нашей стране. Часто можно столкнуться с критикой строгости отечественной сертификации, связанной с предоставлением исходных текстов программ. Действительно, в международной системе сертификации Common Criteria допускается проведение испытаний продукции, обрабатывающей информацию, не отнесенную к гостайне, без предоставления исходных кодов, однако в этом случае должны быть обоснованы проверки на отсутствие скрытых каналов и уязвимостей. Для систем обработки гостайны и платежных систем предусмотрен структурный анализ безопасности исходного кода. Требования по аудиту безопасности исходного кода коммерческих программных продуктов можно найти в международных стандартах PCI DSS, PA DSS и NISTIR 4909.

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

Будущее сертификации

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

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