SPARK (język programowania) - SPARK (programming language)

ISKRA
Izabela.jpg
Paradygmat Wieloparadygmat
Deweloper Altran i AdaCore
Wersja stabilna
Wspólnota 2021 / 1 czerwca 2021 ; 4 miesiące temu ( 2021-06-01 )
Dyscyplina pisania statyczny , mocny , bezpieczny , mianownik
OS Wieloplatformowy : Linux , Microsoft Windows , Mac OS X
Licencja GPLv3
Strona internetowa O SPARK
Główne wdrożenia
SPARK Pro, SPARK GPL Edition, Społeczność SPARK
Wpływem
Ada , Eiffel

SPARK to formalnie zdefiniowany język programowania komputerowego oparty na języku programowania Ada , przeznaczony do tworzenia oprogramowania o wysokiej integralności stosowanego w systemach, w których kluczowe znaczenie ma przewidywalne i wysoce niezawodne działanie. Ułatwia tworzenie aplikacji wymagających bezpieczeństwa, ochrony lub integralności biznesowej.

Pierwotnie istniały trzy wersje języka SPARK (SPARK83, SPARK95, SPARK2005) oparte odpowiednio na Ada 83, Ada 95 i Ada 2005.

Czwarta wersja języka SPARK, SPARK 2014, oparta na Ada 2012, została wydana 30 kwietnia 2014 r. SPARK 2014 to całkowite przeprojektowanie języka i wspierające narzędzia weryfikacyjne .

Język SPARK składa się z dobrze zdefiniowanego podzbioru języka Ada, który używa kontraktów do opisywania specyfikacji komponentów w formie, która jest odpowiednia zarówno do weryfikacji statycznej, jak i dynamicznej.

W SPARK83/95/2005 kontrakty są kodowane w komentarzach Ady i dlatego są ignorowane przez każdy standardowy kompilator Ada, ale są przetwarzane przez SPARK „Examiner” i powiązane z nim narzędzia.

W przeciwieństwie do tego SPARK 2014 wykorzystuje wbudowaną składnię „aspektową” Ada 2012 do wyrażania umów, przenosząc je do rdzenia języka. Główne narzędzie SPARK 2014 (GNATprove) opiera się na infrastrukturze GNAT/GCC i wykorzystuje prawie cały front-end GNAT Ada 2012.

Przegląd techniczny

SPARK wykorzystuje mocne strony Ady, starając się wyeliminować wszystkie jej potencjalne niejasności i niepewne konstrukcje. Programy SPARK są z założenia jednoznaczne, a na ich zachowanie nie ma wpływu wybór kompilatora Ada . Cele te są osiągane częściowo przez pominięcie niektórych bardziej problematycznych funkcji Ady (takich jak nieograniczone równoległe wykonywanie zadań ), a częściowo poprzez wprowadzenie kontraktów, które kodują intencje projektanta aplikacji i wymagania dotyczące określonych składników programu.

Połączenie tych podejść pozwala SPARK osiągnąć swoje cele projektowe, którymi są:

  • logiczny rozsądek
  • rygorystyczna definicja formalna
  • prosta semantyka
  • bezpieczeństwo
  • siła wyrazu
  • Sprawdzalność
  • ograniczone wymagania dotyczące zasobów (miejsca i czasu).
  • minimalne wymagania systemowe środowiska uruchomieniowego

Przykłady umów

Rozważ poniższą specyfikację podprogramu Ada:

procedure Increment (X : in out Counter_Type);

W czystej Adzie może to zwiększyć zmienną Xo jeden lub tysiąc; lub może ustawić jakiś globalny licznik na Xi zwrócić oryginalną wartość licznika w X; albo może w ogóle nic nie robić X.

W SPARK 2014 do kodu są dodawane kontrakty, aby zapewnić dodatkowe informacje dotyczące tego, co faktycznie robi podprogram. Na przykład możemy zmienić powyższą specyfikację, aby powiedzieć:

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

Określa to, że Incrementprocedura nie używa (ani aktualizuje, ani nie odczytuje) żadnej zmiennej globalnej i że jedynym elementem danych używanym do obliczania nowej wartości Xjest ona Xsama.

Alternatywnie projektant może określić:

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

Oznacza to, że Incrementużyje zmiennej globalnej Countw tym samym pakiecie co Increment, że eksportowana wartość Countzależy od importowanych wartości Counti Xoraz że eksportowana wartość Xnie zależy w ogóle od żadnej zmiennej i będzie wyprowadzona tylko z danych stałych .

Jeśli GNATprove zostanie następnie uruchomiony na specyfikacji i odpowiadającej jej treści podprogramu, przeanalizuje treść podprogramu, aby zbudować model przepływu informacji. Ten model jest następnie porównywany z modelem, który został określony przez adnotacje i wszelkie rozbieżności zgłoszone użytkownikowi.

Specyfikacje te mogą być dalej rozszerzone przez zapewnienie różnych właściwości, które albo muszą być zachowane, gdy podprogram jest wywoływany ( warunki wstępne ), albo które będą zachowane po zakończeniu wykonywania podprogramu (warunki końcowe ). Na przykład moglibyśmy powiedzieć, co następuje:

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

To teraz określa nie tylko, że Xwywodzi się z samego siebie, ale także, że przed Incrementwywołaniem Xmusi być ściśle mniejsza niż ostatnia możliwa wartość tego typu i że później Xbędzie równa początkowej wartości Xplus jeden.

Warunki weryfikacji

GNATprove może również generować zestaw warunków weryfikacji lub VC. Warunki te służą do ustalenia, czy dla danego podprogramu obowiązują pewne właściwości. Jako minimum, GNATprove wygeneruje VC w celu ustalenia, że ​​wszystkie błędy czasu wykonania nie mogą wystąpić w podprogramie, takie jak:

  • indeks tablicy poza zakresem
  • wpisz naruszenie zakresu
  • dzielenie przez zero
  • przepełnienie liczbowe.

Jeśli do podprogramu zostanie dodany warunek końcowy lub jakiekolwiek inne potwierdzenie, GNATprove wygeneruje również VC, które wymagają od użytkownika wykazania, że ​​te właściwości obowiązują dla wszystkich możliwych ścieżek w podprogramie.

Pod maską GNATprove wykorzystuje język pośredni Why3 i generator VC, a do rozładowywania VC udowodniono twierdzenia CVC4, Z3 i Alt-Ergo. Korzystanie z innych programów udowadniających (w tym interaktywnych programów sprawdzających dowody) jest również możliwe dzięki innym komponentom zestawu narzędzi Why3.

Historia

Pierwsza wersja SPARK (oparta na Ada 83) została wyprodukowana na Uniwersytecie w Southampton (przy wsparciu Ministerstwa Obrony Wielkiej Brytanii ) przez Bernarda Carré i Trevora Jenningsa. Nazwa SPARK pochodzi od jądra SPADE Ada , w odniesieniu do podzbioru SPADE języka programowania Pascal .

Następnie język był stopniowo rozszerzany i udoskonalany, najpierw przez Program Validation Limited, a następnie przez Praxis Critical Systems Limited. W 2004 roku Praxis Critical Systems Limited zmieniła nazwę na Praxis High Integrity Systems Limited. W styczniu 2010 roku firma zmieniła nazwę na Altran Praxis .

Na początku 2009 roku Praxis nawiązała współpracę z AdaCore i wydała „SPARK Pro” na warunkach GPL. Następnie w czerwcu 2009 wydano SPARK GPL Edition 2009, skierowaną do FOSS i środowisk akademickich.

W czerwcu 2010 r. Altran-Praxis ogłosił, że język programowania SPARK będzie używany w oprogramowaniu amerykańskiego projektu Lunar CubeSat , którego ukończenie ma się zakończyć w 2015 r.

W styczniu 2013 roku Altran-Praxis zmieniło nazwę na Altran.

Pierwsze wydanie PRO SPARK 2014 zostało ogłoszone 30 kwietnia 2014 r., a wkrótce potem pojawiła się edycja SPARK 2014 GPL, skierowana do społeczności FLOSS i środowisk akademickich.

Zastosowania przemysłowe

Systemy związane z bezpieczeństwem

SPARK był stosowany w kilku wysokoprofilowych systemach krytycznych dla bezpieczeństwa, obejmujących lotnictwo komercyjne ( silniki odrzutowe serii Rolls-Royce Trent , system ARINC ACAMS, Lockheed Martin C130J), lotnictwo wojskowe ( EuroFighter Typhoon , Harrier GR9, AerMacchi M346), lotnictwo -zarządzanie ruchem (system UK NATS iFACTS), koleją (liczne aplikacje sygnalizacyjne), medycyną ( urządzenie wspomagające pracę komór LifeFlow ) i zastosowaniami kosmicznymi (projekt Vermont Technical College CubeSat ).

Systemy związane z bezpieczeństwem

SPARK został również wykorzystany do tworzenia bezpiecznych systemów. Wśród użytkowników są Rockwell Collins (rozwiązania międzydomenowe Turnstile i SecureOne), rozwój oryginalnego MULTOS CA, demonstrator NSA Tokeneer, wielopoziomowa stacja robocza secunet, jądro separacji Muen i szyfrator urządzeń blokowych Genode.

W sierpniu 2010 roku Rod Chapman, główny inżynier Altran Praxis, wdrożył Skeina , jednego z kandydatów na SHA-3 , w firmie SPARK. Porównując wydajność implementacji SPARK i C i po starannej optymalizacji, udało mu się uruchomić wersję SPARK tylko o około 5 do 10% wolniej niż C. Późniejsze ulepszenie środkowej części Ady w GCC (wdrożone przez Erica Botcazou z AdaCore ) wypełnił lukę, a kod SPARK dokładnie pasował do C pod względem wydajności.

NVIDIA zastosowała również SPARK do implementacji oprogramowania układowego o znaczeniu krytycznym dla bezpieczeństwa.

W 2020 roku Rod Chapman ponownie zaimplementował bibliotekę kryptograficzną TweetNaCl w SPARK 2014. Wersja SPARK biblioteki ma pełny autoaktywny dowód bezpieczeństwa typu, bezpieczeństwa pamięci i niektórych właściwości poprawności, a także zachowuje algorytmy czasu stałego przez cały czas. Kod SPARK jest również znacznie szybszy niż TweetNaCl.

Zobacz też

Bibliografia

Dalsza lektura

Zewnętrzne linki