В областях с повышенными требованиями к безопасности и надежности приложение обязанно быть корректным. Эта корректность обеспечивается специальными формальными процедурами. Когда дело касается безопасности, ошибка в приложении может стоить человеческой жизни или катастрофы (или просто быть очень дорогой, как, например, ошибки в управлении космическими аппаратами и ракетами). Ошибка в особо надежных приложениях может привести к компрометации национальной безопасности, утрате коммерческой репутации или просто к краже.
Приложения можно классифицировать согласно последствий от сбоя программного обеспечения. Стандарты авиационной безопасности DO-178B [1] и DO-178C [2] предлагают следующую классификацию:
Следует отметить, хотя отказ системы развлечений и относится к уровню E, но, если пилот не может выключить ее (например, чтобы сделать важное объявление), то эта ошибка повышает уровень системы развлечений до D.
Для наиболее критичных приложений, где требуется сертификации в соответствующих органах, недостаточно иметь корректную программу. Необходимо также доказать, что программа корректна, что намного тяжелее. Это требует использования формальных математических методов. Эта и стало причиной возникновения языка SPARK.
Эта глава является кратким введением в SPARK 2014. Это наиболее свежая на данный момент версия языка. В ней используется синтаксис Ада 2012 для указания контрактов, таких как пред- и пост‐условия. Таким образом, SPARK 2014 — это подмножество языка Ада 2012 с некоторыми дополнительными возможностями, облегчающими формальный анализ (эти возможности используют механизм аспектов, рассмотренный в главе «Безопасные типы данных»). Программа на Аде 2012 может иметь компоненты, написанные с использованием всех возможностей Ады, и другие компоненты на языке SPARK (которые будут иметь явную отметку об этом). Компоненты на SPARK могут быть скомпилированы стандартным Ада компилятором и будут иметь стандартную Ада семантику во время исполнения, но они лучше поддаются методам формального анализа, чем остальные компоненты.
Компоненты SPARK кроме компиляции стандартным Ада компилятором еще и анализируются с помощью инструментария SPARK. Этот инструментарий может статически удостовериться в исполнении контрактов (таких, как пред‐условия и пост‐условия), которые обычно проверяются во время исполнения. Как следствие, эти проверки времени исполнения могут быть выключены. Инструментарий SPARK, используемый в GNAT, называется GNATprove. Далее в этой главе мы предполагаем использование для анализа именно этого инструмента.
Важно отметить, что SPARK можно использовать на разных уровнях. На самом простейшем Ада программа, удовлетворяющая подмножеству SPARK, может быть проанализирована без дополнительных усилий. Но мы можем укрепить описание программы, добавив различные аспекты относительно потока информации, что позволит инструментарию провести более скрупулезный анализ программы. В конце концов, пользователь сам выбирает, добавлять или нет данные аспекты, в зависимости от характера проекта, в том числе от требований к необходимому уровню безопасности ПО и политики верификации.
Мы начнем с более подробного рассмотрения основных концепций корректности и контрактов.
Что мы подразумеваем под корректным ПО? Наверное, общим определением может быть такое — ПО, которое делает то, что предполагал его автор. Для простой одноразовой программы это может означать просто результат вычислений, в то время как для большого авиационного приложения это будет определиться текстом контракта между программистом и конечным пользователем.
Идея контрактов в области ПО далеко не нова. Если мы посмотрим на библиотеки, разработанные в начале 1960‐х, в частности, в математической области, написанные на Algol 60 (этот язык пользовался популярностью при публикации подобных материалов в уважаемых журналах, типа Communications of the ACM и Computer Journal), мы увидим подробные требования к параметрам, ограничения на диапазон их значений и прочее. Суть здесь в том, что вводится контракт между автором подпрограммы и ее пользователем. Пользователь обязуется предоставить подходящие параметры, а подпрограмма обязуется вернуть корректный результат.
Деление программы на различные части — это хорошо известный подход, а сутью процесса программирования является определение этих составных частей и, таким образом, интерфейсов между ними. Это позволяет разрабатывать отдельные части независимо друг от друга. Если мы напишем каждую часть правильно (т. е. они будут выполнять каждая свою часть контракта, определяемого интерфейсом) и если мы правильно определили интерфейсы, то мы можем быть уверены, что, собрав все части вместе, получим функционирующую правильно систему.
Горький опыт говорит нам, что в жизни все не совсем так. Две вещи могут пойти не так: с одной стороны, определения интерфейсов зачастую не являются доскональными (есть дыры в контрактах), с другой стороны, индивидуальные компоненты работают неправильно или используются неправильно (контракты нарушаются). И, конечно, контракты могут диктовать совсем не то, что мы имели ввиду.
Любопытно, что есть несколько способов указать контракты на программные компоненты. В первую очередь, и исторически SPARK настоятельно рекомендует делать так, можно указывать контракты с самого начала. Обычно это называют «корректность с помощью построения», а также «декларативная верификация», когда каждый программный модуль содержит контракт в его спецификации. Контракт можно расценивать, как явно выраженные низкоуровневые требования к программному модулю. Если контракт противоречит коду модуля, то это будет обнаружено до начала исполнения программы. Годы использования SPARK в таких областях, как авиация, банковская сфера, управление железной дорогой, позволяют убедиться, что вероятность получить корректную программу повышается и, более того, общая стоимость разработки, включая фазы тестирования и интеграции, уменьшается.
Хотя такой подход эффективен для новых проектов, его применение может быть затруднительно в случаях доработки существующего ПО. В связи с этим, SPARK поддерживает другой стиль разработки, называемый «порождающая верификация». Если код не содержит контрактов, GNATprove может синтезировать некоторые из них на основе тела модуля. Таким образом, проект может двигаться от порождающей верификации к декларативной по мере развития системы. Более того, как мы объясним далее, SPARK 2014 позволяет разработчикам комбинировать формальные методы с традиционными, основанными на тестировании.
Давайте теперь рассмотрим более подробно два вопроса, касающихся, во первых, исчерпывающего определения интерфейса, во вторых, проверки кода реализации на соответствие интерфейсу. Проще подойти к этому в терминах декларативной верификации, хотя эти же концепции также применимы к методу порождающей верификации.
В идеале, определение интерфейса должно скрывать все несущественные детали, но освещать все существенные. Другими словами, мы можем сказать, что определение интерфейса должно быть одновременно корректным и полным.
В качестве простого интерфейса рассмотрим интерфейс подпрограммы. Как мы уже упоминали, интерфейс должен описывать целиком контракт между пользователем и автором. Детали реализации нам не интересны. Чтобы различать эти два аспекта, полезно использовать два различных языка программирования. Некоторые языки представляют подпрограмму как некий неделимый кусок кода, в котором реализация не отделима от интерфейса. В этом кроется проблема. Это не только затрудняет проверку интерфейса, поскольку компилятор сразу требует код вместе с реализацией, но и поощряет программиста писать код одновременно с формулированием интерфейса, что вносит путаницу в процесс разработки.
Структура программы на Аде разделяет интерфейс (спецификацию) от реализации. Это верно как для отдельных подпрограмм, так и для их групп, объединенных в пакеты. Это главная причина того, почему Ада так хорошо подходит как основа для SPARK.
Как упоминалось ранее, иногда очень удобно, когда только часть программы написана на SPARK, а другие части на Аде. Части SPARK отмечаются с помощью аспекта SPARK_Mode. Он может указываться для отдельных подпрограмм, но удобнее указывать его для всего пакета. Например:
package P with SPARK_Mode is ...
В добавок к этому, этот режим можно включить при помощи директивы компилятору. Это удобно, если необходимо указать режим для всей программы (используя файл конфигурации gnat.adc):
pragma SPARK_Mode;
Дополнительную информацию об интерфейсе в SPARK можно передать при помощи механизма аспектов Ада 2012. Главная цель использования этих аспектов — увеличить количество информации об интерфейсе без предоставления лишних деталей о реализации. На самом деле, SPARK позволяет использовать информацию разного уровня детализации в зависимости от потребностей приложения.
Рассмотрим информацию предоставляемую следующей спецификацией:
procedure Add(X: in Integer);
Откровенно говоря, здесь ее совсем мало. Извесно только то, что процедура Add принимает единственный параметр типа Integer. Этого достаточно, чтобы компилятор имел возможность создать код для вызова процедуры. Но при этом совершенно ничего не известно о том, что процедура делает. Она может делать все, что угодно. Она вообще может не использовать значение X. Она может, к примеру, находить разность двух глобальных переменных и печатать результат в некоторый файл. Но теперь рассмотрим, что случиться, если если мы добавим SPARK‐конструкцию, определяющую, как используются глобальные переменные. Мы предполагаем, что процедура определена в пакете, для которого включен режим SPARK_Mode. Спецификация могла бы быть такой:
procedure Add(X: in Integer) with Global => (In_Out => Total);
Аспект Global указывает, что единственной переменной, доступной в этой процедуре, является Total. Кроме того, идентификатор In_Out говорит, что мы будем использовать начальное значение Total и вычислим ее новое значение. В SPARK есть дополнительные правила для параметров подпрограмм. Хотя в Аде мы вправе не использовать параметр X вообще, в SPARK параметры с режимом in должны быть использованы в теле подпрограммы. В противном случае мы получим предупреждение.
Теперь мы знаем намного больше. Вызов Add вычислит новое значение Total, использовав для этого начальное значение Total и значение X. Также известно, то Add не может изменить что‐либо еще. Определенно, она не может ничего печатать или иметь другие побочные эффекты. (Анализатор обнаружит и отвергнет программу, если эти условия нарушаются.)
Безусловно, такой контракт нельзя считать завершенным, поскольку из него не следует, что используется операция сложения, чтобы получить новое значение Total. Указать это можно с помощью пост‐условия:
procedure Add (X: in Integer) with Global => (In_Out => Total), Post => (Total = Total'Old + X);
Пост‐условие однозначно определяет, что новое значение Total равно сумме начального значения (обозначенного как 'Old) и значения X. Теперь спецификация завершена.
Также есть возможность указать пред‐условие. Мы можем потребовать, чтобы X было положительным и при сложении не возникло переполнение. Это можно сделать следующим образом:
Pre => X > 0 and then Total <= Integer'Last - X
(Ограничение на положительные значения X лучше было бы выразить, использовав тип Positive в объявлении параметра X. Мы включили это в предусловие лишь в демонстрационных целях.)
Пред- и пост‐условия, как и все аспекты SPARK, не являются обязательными. Если они не указаны явно, предполагается значение True.
Еще один аспект, который можно указать, это Depends. Он определяет зависимости между начальными значениями параметров и переменных и их конечными значениями. В случае с Add это выглядит так:
Depends => (Total => (Total, X))
Здесь просто сказано, что конечное значение Total зависит от его начального значения и значения X. Однако, в этом случае, это и так можно узнать из режима параметра и глобальной переменной, поэтому это не дает нам новой информации.
Как мы уже говорили, все SPARK‐аспекты являются необязательными. Но, если они указаны, то будут статически верифицированы при анализе тела подпрограммы.
В случае с пред- и пост‐условием будет сделана попытка доказать следующее:
Если предусловие истинно, то (1) не произойдет ошибок времени исполнения и (2) если подпрограмма завершится, то постусловие будет выполнено.
Если контракт не будет верифицирован (например, GNATProve не сможет доказать истинность пред- и пост‐условий), то анализатор отвергнет модуль, но компилятор Ада все еще может скомпилировать его, превратив пред- и пост‐условия в проверки времени исполнения (если Assertion_Policy равна Check). Таким образом, использование общего синтаксиса для Ада 2012 и SPARK 2014 предоставляет значительную гибкость. Например, разработчик сначала может применять проверки во время исполнения, а затем, когда код и контракт будут отлажены, перейти к статической верификации.
Для критических систем данная статическая верификация очень важна. В этой области нарушение контракта во время исполнения недопустимо. Узнать, что условие не выполнено только в момент исполнения, это не то, что нам нужно. Допустим, у нас есть пред‐условие для посадки самолета:
procedure Touchdown(...) with Pre => Undercarriage_Down; -- шасси выпущено
Узнать о том, что шасси не выпущено только в момент посадки самолета будет слишком поздно. На самом деле, мы хотим быть уверены, что программа была проанализирована заранее и гарантируется, что такая ситуация не возникнет.
Это подводит нас к следующему вопросу гарантий того, что реализация корректно исполняет интерфейсный контракт. Иногда это называют отладкой. Вообще есть четыре способа обнаружить ошибку:
Первый тип, на самом деле, должен быть расширен, чтобы обозначать «до начала исполнения программы». Таким образом, он включает сквозной контроль программы и другие рецензирующие методы, в том числе статический анализ инструментарием типа GNATprove.
Очевидно, что эти четыре способа указаны в порядке возрастания трудности. Ошибки тем легче локализовать и исправить, чем раньше они обнаружены. Хорошие средства программирования позволяют переместить ошибки из категории с большим номером в категорию с меньшим. Хороший язык программирования предоставляет средства, позволяющие оградить себя от ошибок, которые трудно найти. Язык Ада хорош благодаря строгой типизации и проверкам времени исполнения. Например, правильное использование перечислимых типов превращает сложные ошибки типа 3 в простые ошибки типа 1, как мы продемонстрировали в главе «Безопасные типы данных».
Главная цель языка SPARK состоит в том, чтобы за счет усиления определения интерфейса (контрактов) переместить все ошибки из других категорий, в идеале, в категорию 1, для того, чтобы обнаружить их до момента запуска приложения. Например, аспект Globals предотвращает случайное изменение глобальных переменных. Аналогично, обнаружение потенциальных нарушений пред- и пост‐условий выливается в ошибки 1‐го типа. Однако, проверка, что такие нарушения невозможны, требует математических доказательств. Это не всегда просто, но GNATprove способен автоматизировать большую часть процесса доказательства.
Ада — это довольно сложный язык программирования и использование всех его возможностей затрудняет полный анализ программы. Соответственно, подмножество языка Ада, используемое в SPARK, ограничивает набор доступных средств. В основном, это касается поведения во время исполнения. Например, отсутствуют ссылочные типы (а следовательно и динамическое распределение памяти) и обработка исключений.
Многозадачность, в ее полном варианте, имеет очень сложную семантику исполнения. Но при использовании Ravenscar‐профиля она все же подлежит формальному анализу. Ravenscar вошел в версию SPARK 2005 и его планируется добавить в следующую версию SPARK 2014 (к моменту перевода брошуры уже добавлен).
Вот список некоторых ограничений, вводимых SPARK 2014:
В дополнение к этим ограничениям, SPARK предписывает более строгую политику инициализации, чем Ада. Объект, передаваемый через in или in out параметр, должен быть полностью инициализирован до вызова процедуры, а out параметр — до возвращения из нее.
Несмотря на эти ограничения, подмножество языка, поддерживаемое SPARK, все еще довольно велико. Оно включает типы с дискриминантами (но без ссылочных дискриминантов), теговые типы и диспетчеризацию, типы с динамическими границами, отрезки массивов и конкатенацию, статические предикаты, условные и кванторные выражения, функции‐выражения, настраиваемые модули, дочерние модули и субмодули. Рекурсия допускается, а стандартная библиотека контейнеров может быть использована для создания сложных структур данных в условиях отсутствия ссылочных типов и динамического распределения памяти. SPARK также предлагает средства взаимодействия с внешним окружением при помощи аспектов, касающихся «изменчивых» (volatile) переменных (т. е. переменных, подверженных асинхронному чтению и записи).
В критических областях, где использование таких средств, как динамическое распределение памяти нежелательно, ранние версии языка SPARK доказали свою исключительную полезность. Теперь же SPARK 2014 существенно расширил набор разрешенных возможностей языка.
В этой главе мы мы коротко подытожим некоторые аспекты механизма формального анализа, используемого инструментарием SPARK.
Во первых, есть две формы потокового анализа:
Потоковый анализ не требует от пользователя больших усилий, чем указания аспектов глобальных переменных и аспектов зависимостей, и, разумеется, учета правил языка SPARK. Добавления этих аспектов позволяет провести более подробный потоковый анализ и обнаружить больше ошибок на ранней стадии.
Важной возможностью потокового анализа является обнаружение неинициализированных переменных. Чтобы воспользоваться этим, необходимо избегать задавать «мусорные» начальные значения по умолчанию, просто «на всякий случай», как мы уже оговаривали это в главе «Безопасный запуск», поскольку это затруднит нахождение ошибок потоковым анализом.
Далее, существуют формальные процессы верификации, касающиеся доказательств:
В случае с функциональными свойствами, которые кроме пред- и пост‐условий включают в себя инварианты циклов и утверждения, касающиеся типов, анализатор генерирует предположения, которые необходимо доказать для гарантирования корректности программы. Эти предположения известны, как условия верификации (verification conditions, VC). А доказательство их называют исполнением условий верификации. За последние годы произошел значительный прогресс в области автоматического доказательства теорем, благодаря чему GNATprove способен автоматически исполнять множество условий верификации. На момент написания этого текста используются технологии Alt-Ergo и CVC4, но можно использовать и другие системы доказательств теорем.
Важно отметить, что даже в отсутствии пред- и пост‐условий анализатор способен генерировать предположения, соответствующие проверкам времени исполнения языка, таким как проверка диапазона. Как мы демонстрировали в главе «Безопасные типы данных», подобные проверки автоматически вставляются, чтобы гарантировать, что переменная не получит значений вне диапазона значений согласно ее объявлению. Аналогичные проверки контролируют попытки чтения/записи элементов за границами массива. Доказательство этих предположений демонстрирует, что условия не нарушаются и программа не содержит ошибок, приводящих к возбуждению исключений в момент исполнения.
Заметим, что использование доказательств не является обязательным. SPARK и соответствующий инструментарий можно использовать на разных уровнях. Для некоторых приложений достаточно использовать потоковый анализ. Но для других может быть экономически целесообразно также провести и доказательство корректности. На самом деле, различные уровни анализа могут быть использованы для различных частей программы. Этого можно добиться, используя различные варианты аспекта SPARK_Mode.
Проведение формальной верификации для всего кода программы может быть нецелесообразно по следующим причинам:
Следующие инструменты для поддержки такого рода «гибридной верификации» входят в состав GNAT технологии.
В качестве примера, рассмотрим версию стека с указанием потоковых зависимостей (аспект Depends) без использования пред- и пост‐условий:
package Stacks with Spark_Mode is type Stack is private; function Is_Empty(S: Stack) return Boolean; function Is_Full(S: Stack) return Boolean; procedure Clear(S: out Stack) with Depends => (S => null); procedure Push(S: in out Stack; X: in Float) with Depends => (S => (S, X)); procedure Pop(S: in out Stack; X: out Float) with Depends => (S => S, X => S); private Max: constant := 100; type Top_Range is range 0 .. Max; subtype Index_Range is Top_Range range 1 .. Max; type Vector is array (Index_Range) of Float; type Stack is record A: Vector; Top: Top_Range; end record; end Stacks;
Мы добавили функции Is_Full и Is_Empty, которые просто считывают состояние стека. Они не имеют аспектов.
Для остальных подпрограмм мы добавили аспекты Depends. Они позволяют указать, от каких аргументов зависит данный результат. Например, для Push указано (S => (S, X)), что означает, что конечное значение S зависит от начального значения S и начального значения X, что, в данном примере, можно вывести из режимов параметров. Но избыточность — это один из ключей достижения надежности. Если аспекты и режимы параметров противоречат друг другу, то это будет обнаружено автоматически при анализе, что, возможно, позволит найти ошибку в спецификации.
Объявления в приватной части были изменены, чтобы дать имена всем используемым подтипам, хотя это и не является обязательным в SPARK 2014.
На этом уровне не нужно вносить каких‐либо изменений в тело пакета, поскольку контракты не требуются. Это подчеркивает тот факт, что SPARK касается в основном улучшения качества описания интерфейса.
Отличия появились также в том, что мы не присвоили начальное значение компоненте Top, а взамен требуем явного вызова Clear. При анализе клиентского SPARK‐кода с помощью GNATprove будет проведен потоковый анализ, гарантирующий, что нет вызова процедур Push или Pop до вызова процедуры Clear. Этот анализ выполняется без исполнения программы. Если GNATprove не может доказать это, то в программе возможна ошибка. С другой стороны, если будет обнаружен вызов Push или Pop перед Clear, то это означает, что ошибка присутствует наверняка.
В таком коротком обзоре, как этот, невозможно привести какой‐либо сложный пример анализа. Но мы приведем тривиальный пример, чтобы продемонстрировать идею. Следующий код:
procedure Exchange(X,Y: in out Float) with Depends => (X => Y, Y => X), Post => (X = Y'Old and Y = X'Old);
демонстрирует спецификацию процедуры, предназначенной для обмена значений двух параметров. Тело может выглядеть так:
procedure Exchange(X,Y: in out Float) is T: Float; begin T := X; X := Y; Y := T; end Exchange;
При анализе GNATprove создает условия верификации, выполнение которых необходимо доказать. В данном примере доказательство тривиально и выполняется автоматически. (Читатель может заметить, что доказательство сводится к проверке условия (x=x and y=y), которое, очевидно, истинно). В более сложных ситуациях GNATprove может не справиться с доказательством, тогда пользователь может предложить промежуточные утверждения, либо воспользоваться другим инструментарием для дальнейшего анализа.
Как было продемонстрировано в предыдущих главах, Ада — это превосходный язык для написания надежного ПО. Ада позволяет программисту обнаруживать ошибки на ранних стадиях процесса разработки. Еще больше ошибок можно выявить, используя SPARK даже без применения процедуры тестирования. Тестирование остается обязательным этапом разработки, несмотря на то, что это сложный и чреватый ошибками процесс.
В областях, где действуют наивысшие требования к безопасности и надежности, недостаточно иметь правильно работающую программу. Необходимо еще доказать, что она является таковой. Этот процесс доказательства называется сертификацией и выполняется согласно процедурам соответствующего органа сертификации. Примерами таких органов на территории США являются FAA в области безопасности и NSA в области надежности. SPARK обладает огромной ценностью в процессе разработки программ, подлежащих сертификации.
Может возникнуть впечатление, что использование SPARK увеличивает стоимость разработки. Однако, исследования систем, переданных в NSA, демонстрируют, что использование SPARK делает процесс разработки более дешевым по сравнению с обычными методами разработки. Несмотря на то, что необходимо потратить некоторые усилия на формулирование контрактов, это, в итоге, окупается за счет сокращения затрат на тестирование и исправление ошибок.
На момент написания этого текста две значительные разработки еще не завершены. Первая касается поддержки профиля Ravenscar в SPARK многозадачности. Вторая — это возможность указать уровни целостности различных компонент программы, которая позволит гарантировать, что поток информации удовлетворяет требованиям указанных уровней безопасности и надежности.
Узнать текущее состояние дел и получить всестороннюю документацию SPARK 2014 можно на сайте www.spark-2014.org/.