SPARK(프로그래밍 언어)
SPARK (programming language) |
 | |
| 패러다임 | 다중 패러다임 |
|---|---|
| 개발자 | Altran 및 AdaCore |
| 안정된 릴리스 | 커뮤니티 2021 / 2021년6월 , 전( |
| 타이핑 분야 | 스태틱, strong, safe, 주격 |
| OS | 크로스 플랫폼: Linux, Microsoft Windows, Mac OS X |
| 면허증. | GPLv3 |
| 웹 사이트 | SPARK에 대해서 |
| 주요 구현 | |
| SPARK Pro, SPARK GPL Edition, SPARK Community | |
| 영향을 받다 | |
| 에이다, 에펠 | |
SPARK는 Ada 프로그래밍 언어를 기반으로 공식적으로 정의된 컴퓨터 프로그래밍 언어로, 예측 가능하고 신뢰성이 높은 동작이 필수적인 시스템에서 사용되는 높은 무결성 소프트웨어 개발을 목적으로 합니다.안전, 보안 또는 비즈니스 무결성을 요구하는 애플리케이션의 개발을 촉진합니다.
원래는 Ada 83, Ada 95 및 Ada 2005를 기반으로 SPARK 83, SPARK 95, SPARK 2005의 3가지 버전이 있었습니다.
에이다 2012를 기반으로 한 SPARK 언어의 네 번째 버전인 SPARK 2014가 2014년 4월 30일에 출시되었습니다.SPARK 2014는 언어와 지원 검증 도구를 완전히 재설계한 것입니다.
SPARK 언어는 계약을 사용하여 정적 및 동적 검증에 적합한 형태로 구성 요소의 사양을 설명하는 잘 정의된 Ada 언어의 하위 집합으로 구성됩니다.
SPARK83/95/2005에서는 계약은 Ada 코멘트로 인코딩되므로 표준 Ada 컴파일러에서는 무시되지만 SPARK "Examiner" 및 관련 툴에 의해 처리됩니다.
반면 SPARK 2014는 Ada 2012에 내장된 "aspect" 구문을 사용하여 계약을 표현하고 계약 내용을 언어의 핵심으로 가져옵니다.SPARK 2014(GNATprove)의 주요 툴은 GNAT/GCC 인프라스트럭처를 기반으로 하며 GNAT Ada 2012 프런트엔드의 거의 전부를 재사용합니다.
기술 개요
SPARK는 Ada의 장점을 활용하면서 잠재적인 모호성과 안전하지 않은 구조를 모두 제거하려고 합니다.SPARK 프로그램은 모호하지 않도록 설계되었으며, 그 동작은 Ada 컴파일러의 선택에 영향을 받지 않아야 합니다.이러한 목표는 Ada의 보다 문제가 많은 기능(예: 무제한 병렬 태스크)을 생략하고 프로그램의 특정 컴포넌트에 대한 애플리케이션 설계자의 의도와 요건을 인코딩하는 계약을 도입함으로써 달성됩니다.
이러한 접근방식을 조합하면 SPARK는 다음과 같은 설계 목표를 달성할 수 있습니다.
계약 예
아래의 Ada 서브 프로그램 사양을 고려하십시오.
절차 증분(X : in out Counter_Type);
순수한 에이다에서는 이것이 변수를 증가시킬 수 있다.X1천명 또는 1천명, 또는 글로벌하게 대항할 수 있습니다.X카운터의 원래 값을 반환합니다.X또는 전혀 효과가 없을 수도 있습니다.X조금도.
SPARK 2014에서는 서브 프로그램이 실제로 수행하는 작업에 대한 추가 정보를 제공하는 계약이 코드에 추가됩니다.예를 들어, 위의 사양을 다음과 같이 변경할 수 있습니다.
Global = > null, Depends = > (X = > X)를 사용한 프로시저 증분(X : in out Counter_Type);
이 명령어는 다음과 같습니다.Increment프로시저는 글로벌 변수를 사용하지 않으며(업데이트 또는 읽기) 새로운 값 계산에 사용되는 유일한 데이터 항목입니다.X이X그 자체입니다.
또는 설계자는 다음을 지정할 수 있습니다.
글로벌 => (In_Out => Count), 의존 => (Count => (Count, X), X => null)을 사용하여 프로시저 증분(X : in out Counter_Type);
이것은, 다음과 같이 지정합니다.Increment글로벌 변수를 사용합니다.Count와 같은 패키지로Increment내보내기된 값CountImport된 값에 의존하다Count그리고.X및 내보내기된 값X는 변수에 전혀 의존하지 않으며 상수 데이터에서만 파생됩니다.
GNATprove가 하위 프로그램의 사양 및 해당 본문에서 실행되는 경우, 하위 프로그램의 본문을 분석하여 정보 흐름의 모델을 구축합니다.그런 다음 이 모델을 주석 및 사용자에게 보고된 불일치에 의해 지정된 모델과 비교합니다.
이러한 사양은 서브프로그램이 호출되었을 때(전제조건) 유지되어야 하거나 서브프로그램 실행이 완료되면(후제조건) 유지되어야 하는 다양한 속성을 주장함으로써 더욱 확장될 수 있습니다.예를 들어 다음과 같이 말할 수 있습니다.
글로벌 = > null, 종속 = > (X = > X), 사전 = > X < Counter _ 를 사용한 프로시저 증분(X : in Counter _ Type )'Last', Post => X = X'Old + 1을 입력합니다.
이것은, 이것뿐만이 아닙니다.X그 자체만으로 얻을 수 있지만, 그 이전에도Increment라고 불리고 있다X(결과가 오버플로하지 않도록 하기 위해) 그 타입의 마지막 가능한 값보다 엄밀하게 작아야 하며, 그 후에 그 값이 오버플로우하지 않도록 해야 합니다.X초기값과 같다X하나 더.
검증 조건
GNATprove는 검증 조건 또는 VC 세트를 생성할 수도 있습니다.이러한 조건은 특정 속성이 특정 서브 프로그램에 대해 유지되는지 여부를 설정하기 위해 사용됩니다.적어도 GNATprove는 VC를 생성하여 서브프로그램 내에서 다음과 같은 모든 런타임에러가 발생할 수 없음을 확인합니다.
- 배열 인덱스가 범위를 벗어남
- 형식 범위 위반
- 0으로 나누기
- 수치 오버플로
포스트 조건이나 다른 어설션이 서브 프로그램에 추가되면 GNATprove는 사용자가 서브 프로그램을 통과하는 모든 가능한 경로에 대해 이러한 속성이 유지됨을 보여줄 필요가 있는 VC도 생성합니다.
후드에서 GNATprove는 Why3 중간언어와 VC Generator, CVC4, Z3, Alt-Ergo 정리프로버를 사용하여 VC를 방전합니다.다른 프로버(인터랙티브 프루프 체커 포함)는 Why3 툴 세트의 다른 컴포넌트를 통해서도 사용할 수 있습니다.
역사
SPARK의 첫 번째 버전(Ada 83 기반)은 영국 국방부의 후원으로 Southampton 대학에서 Bernard Caré와 Trevor Jennings에 의해 제작되었습니다.SPARK라는 이름은 Pascal 프로그래밍 [1]언어의 SPADE 하위 집합에서 유래되었습니다.
그 후 Program Validation Limited와 Praxis Critical Systems Limited가 언어를 점진적으로 확장하고 개선했습니다.2004년 Praxis Critical Systems Limited는 Praxis High Integrity Systems Limited로 이름을 변경했습니다.2010년 1월에 Altran Praxis가 되었습니다.
2009년 초 Praxis는 AdaCore와 파트너십을 맺고 GPL 조건 하에 SPARK Pro를 출시했습니다.그 후 2009년 6월에 FOSS 및 학계를 대상으로 한 SPARK GPL Edition 2009가 출시되었습니다.
2010년 6월, Altran-Praxis는 2015년에 완료될 것으로 예상되는 미국 달 프로젝트 CubeSat의 소프트웨어에 SPARK 프로그래밍 언어가 사용될 것이라고 발표했습니다.
2013년 1월, Altran-Praxis는 Altran으로 이름을 변경하였고, 2021년 4월에 Capgemini Engineering이 되었다(Altran이 Capgemini와 합병함에 따라).
SPARK 2014의 첫 번째 Pro 릴리스는 2014년 4월 30일에 발표되었으며, FLOSS 및 학계를 대상으로 한 SPARK 2014 GPL 에디션으로 빠르게 이어졌습니다.
산업용 응용 프로그램
SPARK는 상업 항공(Rolls-Royce Trent 시리즈 제트 엔진, ARINC ACAMS 시스템, 록히드 마틴 C130J), 군용 항공(EuroFighter Typhon, Harrier GR9, AirMacchi M346), 항공 교통 관리(NATFacts 시스템)를 포함하는 여러 고급 안전 중요 시스템에 사용되었습니다.Dical(LifeFlow 심실 보조 장치) 및 공간 애플리케이션(버몬트 기술 대학 큐브샛 프로젝트)[citation needed]이 있습니다.
SPARK는 안전한 시스템 개발에도 사용되고 있습니다.사용자에는 Rockwell Collins(Turnstile 및 SecureOne 크로스 도메인 솔루션), 오리지널 MULTOS CA 개발, NSA Tokener 데모, secunet 멀티 레벨 워크스테이션, Muen 분리 커널 및 Genode 블록 디바이스 암호화기가 포함됩니다.
2010년 8월 Altran Praxis의 수석 엔지니어인 Rod Chapman은 SHA-3 후보 중 하나인 Skin을 SPARK에 구현했습니다.SPARK와 C의 실장 퍼포먼스를 비교하고 신중하게 최적화한 결과 SPARK 버전을 C보다 5~10% 정도 느리게 실행할 수 있었습니다.이후 GCC의 Ada 미들엔드에 대한 개선(AdaCore의 Eric Botcazou에 의해 구현됨)은 성능 면에서 [2]C와 정확히 일치하는 SPARK 코드를 사용하여 격차를 좁혔습니다.
또, NVIDIA는, 시큐러티 크리티컬한 [3]펌 웨어의 실장에 SPARK를 채용했습니다.
2020년 Rod Chapman은 SPARK [4]2014에서 TweetNaCl 암호화 라이브러리를 다시 구현했습니다.라이브러리의 SPARK 버전에는 타입 안전성, 메모리 안전성 및 일부 정확성 속성에 대한 완전한 자동 활성 증명이 있으며 일정 시간 알고리즘이 유지됩니다.SPARK 코드는 TweetNaCl보다 훨씬 빠릅니다.
「 」를 참조해 주세요.
레퍼런스
- ^ "SPARK - The SPADE Ada Kernel (including RavenSPARK)". AdaCore. Retrieved 30 June 2021.
- ^ Handy, Alex (24 August 2010). "Ada-derived Skein crypto shows SPARK". SD Times. BZ Media LLC. Retrieved 31 August 2010.
- ^ "Securing the Future of Safety and Security of Embedded Software". 8 January 2020.
- ^ "SPARKNaCl". 8 October 2021.
추가 정보
- John Barnes (2012). SPARK: The Proven Approach to High Integrity Software. Altran Praxis. ISBN 978-0-9572905-1-8.
- John W. McCormick and Peter C. Chapin (2015). Building High Integrity Applications with SPARK 2014. Cambridge University Press. ISBN 978-1-107-65684-0.
- Philip E. Ross (September 2005). "The Exterminators". IEEE Spectrum. 42 (9): 36–41. doi:10.1109/MSPEC.2005.1502527. ISSN 0018-9235. S2CID 26369398.
