«Мы гарантируем, что наше программное обеспечение в течение 90 дней со дня получения будет выполнять свои основные функции в соответствии с сопроводительными материалами, несмотря на возможные ошибки в программах и процедуре установки» — так выглядит типичная гарантия на программные продукты, которая совершенно бесполезна. Для других продуктов обычно гарантируется «пригодность к использованию по назначению», но к продуктам программным это не относится. Как ни странно, при отсутствии надлежащей гарантии на программное средство таковую может иметь компакт-диск с дистрибутивом — если он сильно поцарапан или имеет другие дефекты, поставщик заменит его бесплатно.
Директор информационной службы General Motors Тони Скотт ежегодно тратит на ИТ более 3 млрд. долл. Он говорит, что корпорация давно бы разорилась, если бы продавала автомобили так, как продают программы. В интервью еженедельнику eWeek Скотт призывает поставщиков программных продуктов предоставлять гарантию, ограждающую потребителей от любых ошибок, которые могли бы нанести ущерб их организациям. В таком случае поставщик будет нести ответственность за поставку программы с известными ошибками, например, в системе безопасности, которые впоследствии приведут к отказу компьютеров потребителя или причинению вреда его продуктам.
Для производителей программных продуктов ошибки стали неприятным фактом: они не могут гарантировать отсутствие ошибок, потому что не в состоянии в этом убедиться. Цена ошибок неимоверно велика. По данным NIST, ошибки в программном обеспечении обходятся экономике США в 60 млрд. долл. в год. Чтобы оценить убытки в мировом масштабе, достаточно утроить это число, и мы получим сумму, превышающую стоимость ежегодного валового национального продукта многих стран.
Как изменить ситуацию к лучшему? Можно ли ожидать появления программных продуктов с гарантией пригодности к использованию по назначению?
С появлением подходящих компьютерных инструментальных средств широкое использование формальных методов преобразует практику программной инженерии. Международное сообщество обязалось решить эту проблему в течение следующих 15-20 лет.
ПОЧЕМУ ИМЕННО СЕЙЧАС?
Теоретическая информатика стала зрелой научной дисциплиной, пожалуй, после публикации 75 лет назад теоремы Курта Геделя о неполноте. В то время единственными компьютерами общего назначения были машины Тьюринга, а электроника находилась в младенческом состоянии. Теории разработки программного обеспечения — широко изучавшиеся как формальные методы программной инженерии — опирались на фундаментальные результаты в теории вычислений, анализе алгоритмов и семантике языков программирования. Разработчики используют формальные методы для точного документирования назначения программного обеспечения и прогнозирования его поведения на практике. Они также используют эти методы для документирования интерфейса к программной системе или компонент в качестве контракта между заказчиком и поставщиком. Эта документация поддается формальному анализу.
Формальные методы дают возможность экспериментировать с моделями в попытках найти наилучший способ структурирования абстрактных описаний сложных систем. В случае успеха удается яснее сформулировать назначение системы. Это, в свою очередь, ведет к более ясной архитектуре, которая облегчает заказчику понимание и использование системы.
В качестве примера рассмотрим проект Microsoft Static Device Verifier (SDV). Одно время флагманский продукт Microsoft — операционная система Windows «славилась» своими частыми отказами. SDV составляет малую, но интересную часть большой работы по повышению надежности Windows. Анализ показал, что 85% всех аварий Windows XP являются следствием отказов драйверов устройств. Овладение API для программирования драйверов — задача непростая, а сторонние разработчики, которые пишут большинство из них, не являются экспертами по ядру Windows.
Чтобы с помощью SDV проверить правильность обращения к функциям API в драйвере устройства, небольшая часть кода драйвера преобразуется в логическую программу (boolean program), в которой логические переменные отражают важные правила применения интерфейса. Затем производится символическая проверка соответствия модели абстрактному понятию корректного использования API. Как только Microsoft сделает SDV доступным для третьих фирм, он станет простым и удобным инструментом, вобравшим в себя большое количество знаний из предметной области.
SDV является хорошим примером сложной теории, скрытой от программистов в готовом к применению инструменте. Драйвер устройства может отказать по многим причинам, и SDV не пытается найти их все. В частности, не проверяется выход за границы массива и не осуществляется оценка производительности. В результате получается сфокусированный аналитический инструмент, который устраняет некоторый класс ошибок и напоминает продвинутую разновидность проверки типов.
ГРАНДИОЗНЫЙ ВЫЗОВ
Решение проблемы верифицированного программного обеспечения превратилось в амбициозную международную долгосрочную исследовательскую программу, направленную на получение существенных объемов полезного кода, формально проверенного в соответствии с самыми высокими стандартами строгости и точности. Эту программу инициировал Энтони Хоар, обратив внимание ИТ-сообщества на «грандиозный вызов» — необходимость разработки целостного автоматизированного набора инструментов для проверки корректности программного обеспечения. В феврале 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 и используют хорошо известные алгоритмы и структуры данных; это позволяет надеяться, что небольшая группа сумеет завершить работу над проектом за два года. Далее, поскольку большая часть электронных данных хранится в файловых системах, корректность этих систем имеет большое значение при использовании компьютеров. Существует множество открытых источников документации по современным файловым системам. Наконец, исследователи могут подходить к проекту с разных сторон: можно проектировать новую файловую систему на пустом месте, используя уточнение, или верифицировать существующую файловую систему с открытым исходным кодом. В равной степени применимы как проверка модели, так и доказательство теорем.
Задача состоит в том, чтобы получить следующие результаты: формальная поведенческая спецификация функциональных возможностей файловой системы; список предположений относительно основообразующих аппаратных средства; набор инвариантов, утверждений и свойств, касающихся ключевых структур данных и алгоритмов реализации.
В POSIX на неформальном уровне тщательно описано поведение таких функций, как создание, открытие, чтение и запись. Таким образом, первой задачей экспериментального проекта станет составление формальных спецификаций соответствующих частей стандарта. Существует несколько частичных формализаций, например Z-спецификация файловой системы Unix в [1] и спецификация файловой системы Synergy в [2]. Эти работы могли бы стать полезными отправными точками для развития более полной спецификации.
Создание строгого формального описания свойств файловой системы, особенно ее устойчивости по отношению к отказам питания, требует опоры на некоторые предположения о поведении основообразующего оборудования. Чтобы сделать файловую систему полезной, исследователи должны достаточно обоснованно выдвигать предположения относительно типовых аппаратных средств, таких как накопители на жестких дисках или флэш-память. В идеале файловая система должна быть пригодна к использованию с различными типами аппаратных средств, возможно, обеспечивая различные гарантии надежности. Вопросы производительности диктуют применение кэш-памяти и буферов записи, которые повышают опасность несогласованностей в условиях параллельного доступа из программных потоков и неожиданных отказов питания.
Доказательством корректности реализации станут формальные описания свойств проекта, такие как инварианты структуры данных, аннотации, описывающие защиту данных с блокировкой, а также пред- и постусловия для библиотечных функций. В популярных файловых системах широко используются стандартные структуры данных, такие как хеш-таблицы, связанные списки и деревья поиска. Доказательство корректности файловой системы повлечет за собой разработку библиотек формально описанных свойств и обоснование корректности структур данных, которые будут полезны в дальнейших работах по верификации. Они также станут полезным вкладом в репозитарий.
Джоши и Хольцман работают над долгосрочной задачей построения надежного программного обеспечения с использованием автоматизированных инструментов верификации, отказавшись от традиционных процессов разработки, специально подбираемых для каждого конкретного случая. Частью этой задачи является построение надежной файловой системы с использованием флэш-памяти в качестве энергонезависимого хранилища на борту будущих космических кораблей. Флэш-память удобна для этой цели, поскольку не имеет движущихся частей, потребляет мало энергии, легко доступна и уже использовалось в нескольких последних миссиях НАСА, таких как Mars Exploration Rover и Deep Impact. Однако построение надежной файловой системы для флэш-памяти является нетривиальной задачей.
Эту задачу осложняют некоторые недостатки, с которыми нужно справляться, например случайное инвертирование битов, неожиданный выход блока из строя и ограниченный срок его службы (обычно 100 тыс. использований). Кроме того, файловая система, предназначенная для использования на космическом корабле, должна удовлетворять дополнительным ограничениям; например, бортовым программам после инициализации обычно не разрешается запрашивать дополнительную память.
В отрасли растет понимание того, что с надежностью программного обеспечения надо что-то делать. Билл Джой, один из основателей компании Sun Microsystems, сказал: «Есть еще несколько вещей, которые я хочу осуществить. Я по-прежнему считаю, что наши инструменты совершенно неадекватны проблеме построения надежных программ». Документ The International Technology Roadmap for Semiconductors, в котором дается оценка отраслевых технологических требований, призван способствовать непрерывному повышению производительности интегральных схем. В его выпуске от 2005 года утверждается, что «без крупных прорывов верификация останется непреодолимым барьером на пути прогресса в индустрии полупроводников».
Есть ли признаки внимания к этой проблеме со стороны гигантов программной индустрии? Билл Гейтс описал продвижение своей компании в этом направлении, выступая на конференции WinHec в 2002 году: «Верификация программного обеспечения… была чашей святого Грааля информатики в течение многих десятилетий; но теперь в некоторых ключевых областях, например в области верификации драйверов, мы производим инструменты, способные на практике доказать работоспособность программного обеспечения, чтобы гарантировать его надежность».
- C. Morgan, B. Sufrin. Specification of the Unix Filing System. IEEE Trans. Software Eng., Feb. 1984.
- W.R. Bevier, R. Cohen, J. Turner, A Specification for the Synergy File System. Tech. report TR-120, Computational Logic Inc., 1995.
Джим Вудкок (jim@cs.york.ac.uk) — преподаватель программной инженерии Университета Йорка.
Jim Woodcock, First Steps in the Verified Software Grand Challenge, IEEE Computer, October 2006, IEEE Computer Society, 2006, All rights reserved. Reprinted with permission.
