СПАРК (язык программирования)

ИСКРА
Парадигма	Мультипарадигмальность
Разработчик	Альтран и АдаКор
Стабильная версия	Сообщество 2021 / 1 июня 2021 г .; 3 года назад
Дисциплина набора текста	статический , сильный , безопасный , именительный падеж
ТЫ	Кроссплатформенность : Linux , Microsoft Windows , Mac OS X.
Лицензия	лицензия GPLv3
Веб-сайт	О СПАРК
Основные реализации
	SPARK Pro, SPARK GPL Edition, Сообщество SPARK
Под влиянием
	Ада , Эйфель

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

Первоначально существовало три версии языка SPARK (SPARK83, SPARK95, SPARK2005), основанные на Ada 83, Ada 95 и Ada 2005 соответственно.

Четвертая версия языка SPARK, SPARK 2014, основанная на Ada 2012, была выпущена 30 апреля 2014 года. SPARK 2014 представляет собой полную переработку языка и поддерживает инструменты проверки .

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

В SPARK83/95/2005 контракты закодированы в комментариях Ada и поэтому игнорируются любым стандартным компилятором Ada, но обрабатываются SPARK «Examiner» и связанными с ним инструментами.

SPARK 2014, напротив, использует встроенный в Ada 2012 «аспектный» синтаксис для выражения контрактов, перенося их в ядро языка. Основной инструмент для SPARK 2014 (GNATprove) основан на инфраструктуре GNAT/GCC и повторно использует почти весь интерфейс GNAT Ada 2012.

Технический обзор

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

Сочетание этих подходов позволяет СПАРК достичь своих целей проектирования, а именно:

логическая обоснованность
строгое формальное определение
простая семантика
безопасность
выразительная сила
проверяемость
ограниченные требования к ресурсам (пространству и времени).
минимальные системные требования к среде выполнения

Примеры контрактов

Рассмотрим спецификацию подпрограммы Ada ниже:

procedure Increment (X : in out Counter_Type);

В чистой Ada это может увеличить переменную X на одну или тысячу; или он может установить какой-то глобальный счетчик X и верните исходное значение счетчика в X; или это может совершенно ничего не сделать с X совсем.

В SPARK 2014 в код добавляются контракты, предоставляющие дополнительную информацию о том, что на самом деле делает подпрограмма. Например, мы можем изменить приведенную выше спецификацию, сказав:

procedure Increment (X : in out Counter_Type)
  with Global => null,
       Depends => (X => X);

Это указывает на то, что Increment Процедура не использует (ни обновляет, ни читает) какую-либо глобальную переменную и что единственный элемент данных, используемый при вычислении нового значения X является X сам.

В качестве альтернативы дизайнер может указать:

procedure Increment (X : in out Counter_Type)
  with Global  => (In_Out => Count),
       Depends => (Count  => (Count, X),
                   X      => null);

Это указывает на то, что Increment будет использовать глобальную переменную Count в той же упаковке, что и Increment, что экспортированная стоимость Count зависит от импортированных значений Count и X, и что экспортированная стоимость X вообще не зависит ни от каких переменных и будет получен только на основе постоянных данных.

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

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

procedure Increment (X : in out Counter_Type)
  with Global  => null,
       Depends => (X => X),
       Pre     => X < Counter_Type'Last,
       Post    => X = X'Old + 1;

Это, теперь, указывает не только на то, что X выводится только из самого себя, но также и из того, что прежде Increment называется X должно быть строго меньше последнего возможного значения своего типа (чтобы гарантировать, что результат никогда не переполнится ) и чтобы впоследствии X будет равна первоначальному значению X плюс один.

Условия проверки

GNATprove также может генерировать набор условий проверки или VC. Эти условия используются для установления того, выполняются ли определенные свойства для данной подпрограммы. Как минимум, GNATprove сгенерирует VC, чтобы установить, что все ошибки времени выполнения не могут возникнуть в подпрограмме, например:

индекс массива вне диапазона
нарушение диапазона типов
деление на ноль
числовое переполнение.

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

Под капотом GNATprove использует промежуточный языкWhy3 и генератор VC, а также средства доказательства теорем CVC4 , Z3 и Alt-Ergo для выгрузки VC. Использование других средств проверки (в том числе интерактивных средств проверки корректур) также возможно с помощью других компонентов набора инструментовWhy3.

История

Первая версия SPARK (на основе Ada 83) была создана в Университете Саутгемптона (при спонсорской поддержке Министерства обороны Великобритании ) Бернаром Карре и Тревором Дженнингсом. Название SPARK произошло от SPADE Ada Kernel , относящегося к SPADE подмножеству языка программирования Pascal . ^[1]

Впоследствии этот язык постепенно расширялся и совершенствовался сначала компанией Program Validation Limited, а затем Praxis Critical Systems Limited. В 2004 году Praxis Critical Systems Limited сменила название на Praxis High Integrity Systems Limited. В январе 2010 года компания стала Altran Praxis .

В начале 2009 года Praxis заключила партнерство с AdaCore и выпустила «SPARK Pro» на условиях GPL. За этим в июне 2009 года последовала версия SPARK GPL Edition 2009, предназначенная для FOSS и академических сообществ.

В июне 2010 года компания «Альтран-Праксис» объявила, что язык программирования SPARK будет использоваться в программном обеспечении американского лунного проекта CubeSat , завершение которого ожидается в 2015 году.

В январе 2013 года Altran-Praxis сменила название на Altran, которое в апреле 2021 года стало Capgemini Engineering (после слияния Altran с Capgemini ).

О первом профессиональном выпуске SPARK 2014 было объявлено 30 апреля 2014 года, за ним вскоре последовала версия SPARK 2014 GPL, предназначенная для FLOSS и академических сообществ.

Промышленное применение

Системы безопасности

SPARK использовался в нескольких высококлассных критически важных для безопасности системах, охватывающих коммерческую авиацию ( Rolls-Royce Trent реактивные двигатели серии , система ARINC ACAMS , Lockheed Martin C130J ), военную авиацию ( EuroFighter Typhoon , Harrier GR9 , AerMacchi M346 ), авиацию - управление дорожным движением ( UK NATS iFACTS система ), железнодорожное (многочисленные приложения сигнализации), медицинское ( желудочковое вспомогательное устройство LifeFlow ) и космическое применение ( проект CubeSat Вермонтского технического колледжа ). ^{[ нужна ссылка ]}

Системы безопасности

SPARK также использовался при разработке безопасных систем. В число пользователей входят Rockwell Collins (междоменные решения Turnstile и SecureOne), разработка оригинального MULTOS АНБ CA, демонстратор Tokeneer , многоуровневая рабочая станция secunet, ядро разделения Muen и Genode шифратор блочных устройств .

В августе 2010 года Род Чепмен, главный инженер Altran Praxis, внедрил в СПАРК Skein , одного из кандидатов на SHA-3 . Сравнивая производительность реализаций SPARK и C и после тщательной оптимизации, ему удалось добиться того, чтобы версия SPARK работала лишь примерно на 5–10 % медленнее, чем C. Позднее усовершенствование среднего уровня Ada в GCC (реализовано Эриком Ботказу из AdaCore) ) закрыл разрыв: код SPARK точно соответствует C по производительности. ^[2]

NVIDIA также внедрила SPARK для реализации критически важного для безопасности встроенного ПО. ^[3]

В 2020 году Род Чепмен повторно реализовал криптографическую библиотеку TweetNaCl в SPARK 2014. ^[4] Версия библиотеки SPARK имеет полное автоматическое подтверждение безопасности типов, безопасности памяти и некоторых свойств корректности, а также сохраняет алгоритмы постоянного времени. Код SPARK также значительно быстрее, чем TweetNaCl.

См. также

Ссылки

^ «SPARK — Ядро Ada SPADE (включая RavenSPARK)» . АдаКор . Проверено 30 июня 2021 г.
^ Хэнди, Алекс (24 августа 2010 г.). «Криптовалюта Skein, основанная на Ada, показывает SPARK» . СД Таймс . ООО «БЗ Медиа» . Проверено 31 августа 2010 г.
^ «Обеспечение безопасности и защищенности встроенного программного обеспечения в будущем» . 8 января 2020 г.
^ «СПАРКNaCl» . Гитхаб . 8 октября 2021 г.

Дальнейшее чтение

Барнс, Джон (2012). SPARK: проверенный подход к программному обеспечению высокой целостности . Альтран Праксис. ISBN 978-0-9572905-1-8 .

Маккормик, Джон В.; Чапин, Питер К. (2015). Создание приложений высокой целостности с помощью SPARK . Издательство Кембриджского университета. ISBN 978-1-107-65684-0 .

Росс, Филип Э. (сентябрь 2005 г.). «Истребители» . IEEE-спектр . 42 (9): 36–41. дои : 10.1109/MSPEC.2005.1502527 . ISSN 0018-9235 . S2CID 26369398 .

Внешние ссылки

[spark_lang_ref_manual-1] «SPARK — Ядро Ada SPADE (включая RavenSPARK)» . АдаКор . Проверено 30 июня 2021 г.

[2] Хэнди, Алекс (24 августа 2010 г.). «Криптовалюта Skein, основанная на Ada, показывает SPARK» . СД Таймс . ООО «БЗ Медиа» . Проверено 31 августа 2010 г.

[3] «Обеспечение безопасности и защищенности встроенного программного обеспечения в будущем» . 8 января 2020 г.

[4] «СПАРКNaCl» . Гитхаб . 8 октября 2021 г.

[1]

[2]

[3]

[4]