Введение
Язык программирования, язык программирования SPARK – это формально определенный язык программирования, основанный на языке программирования Ada и предназначенный для разработки программного обеспечения с высокой степенью надежности, используемого в системах, где требуется предсказуемая и безотказная работа. Он упрощает разработку приложений, требующих безопасности, защиты или деловой целостности. Изначально существовало три версии языка SPARK (SPARK83, SPARK95, SPARK2005), основанные соответственно на Ada 83, Ada 95 и Ada 2005. 30 апреля 2014 года была выпущена четвертая версия языка SPARK – SPARK 2014, основанная на Ada 2012. SPARK 2014 представляет собой полную переработку языка и инструментов, поддерживающих верификацию. Язык SPARK состоит из четко определенного подмножества языка Ada, использующего контракты для описания спецификаций компонентов в форме, подходящей как для статической, так и для динамической верификации. В SPARK83/95/2005 контракты кодируются в комментариях Ada и, следовательно, игнорируются любым стандартным компилятором Ada, но обрабатываются SPARK "Examiner" и сопутствующими инструментами. В отличие от этого, SPARK 2014 использует встроенный синтаксис "аспектов" Ada 2012 для выражения контрактов, интегрируя их в ядро языка. Основной инструмент SPARK 2014 (GNATprove) основан на инфраструктуре GNAT/GCC и повторно использует почти весь фронтенд GNAT Ada 2012.
the programming language
SPARK is a formally defined computer programming language based on the Ada programming language, intended for the development of high integrity software used in systems where predictable and highly reliable operation is essential. It facilitates the development of applications that demand safety, security, or business integrity. Originally, there were three versions of the SPARK language (SPARK83, SPARK95, SPARK2005) based on Ada 83, Ada 95 and Ada 2005 respectively. A fourth version of the SPARK language, SPARK 2014, based on Ada 2012, was released on April 30, 2014. SPARK 2014 is a complete re design of the language and supporting verification tools. The SPARK language consists of a well defined subset of the Ada language that uses contracts to describe the specification of components in a form that is suitable for both static and dynamic verification. In SPARK83/95/2005, the contracts are encoded in Ada comments and so are ignored by any standard Ada compiler, but are processed by the SPARK "Examiner" and its associated tools. SPARK 2014, in contrast, uses Ada 2012's built in "aspect" syntax to express contracts, bringing them into the core of the language. The main tool for SPARK 2014 (GNATprove) is based on the GNAT/GCC infrastructure, and re uses almost the entirety of the GNAT Ada 2012 front end.
История
Первая версия SPARK (на основе Ada 83) была разработана в Университете Саутгемптона (при поддержке Министерства обороны Великобритании) Бернардом Карре и Тревором Дженнингсом. Название SPARK произошло от SPADE Ada Kernel, отсылая к подмножеству SPADE языка программирования Pascal. Впоследствии язык последовательно расширялся и совершенствовался, сначала компанией 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 года Altran Praxis объявила, что язык программирования SPARK будет использоваться в программном обеспечении американского лунного проекта CubeSat, завершение которого ожидалось в 2015 году. В январе 2013 года Altran Praxis сменила название на Altran, которая в апреле 2021 года стала Capgemini Engineering (в результате слияния Altran и Capgemini). Первый Pro релиз 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 Vermont Technical College).
Системы, связанные с безопасностью
SPARK также применяется при разработке защищенных систем. Среди пользователей — Rockwell Collins (решения Turnstile и SecureOne для междоменного взаимодействия), разработка оригинального CA MULTOS, демонстрационный образец NSA Tokeneer, многоуровневая рабочая станция secunet, микроядро разделения Muen и шифратор блочных устройств Genode. В августе 2010 года Род Чепмен, ведущий инженер Altran Praxis, реализовал Skein, одного из кандидатов на SHA-3, на SPARK. Сравнивая производительность реализаций на SPARK и C и после тщательной оптимизации, ему удалось добиться того, что версия на SPARK работала всего на 5–10% медленнее, чем версия на C. Последующие улучшения промежуточного представления Ada в GCC (реализованные Эриком Ботказу из AdaCore) устранили эту разницу, и код на SPARK достиг производительности, идентичной коду на C. Компания NVIDIA также использует SPARK для реализации критически важной для безопасности прошивки. В 2020 году Род Чепмен повторно реализовал криптографическую библиотеку TweetNaCl на SPARK 2014. Версия библиотеки на SPARK имеет полное автоматическое доказательство безопасности типов, безопасности памяти и некоторых свойств корректности, а также сохраняет алгоритмы с постоянным временем выполнения. Код на SPARK также значительно быстрее, чем TweetNaCl.