NIST Report Shows SPARK Most Suitable Language for Secure Programming

SPARK language shown to have fewest vulnerabilities

SAN JOSE, Calif., NEW YORK and PARIS, May 2, 2011 – Embedded Systems Conference – AdaCore, a leading supplier of Ada development tools and support services, today announced that the SPARK language's immunity to many vulnerabilities found in other languages has been corroborated by a recent report published by the National Institute of Standards and Technology (NIST). This report – Source Code Security Analysis Tool Functional Specification Version 1.1 (NIST Special Publication 500-268 v1.1) – examines software assurance tools as a fundamental resource to improve quality in today’s software applications. It looks at the behavior of one class of software assurance tool: the source code security analyzer. Because many software security weaknesses are introduced at the implementation phase, using a source code security analyzer should help reduce the number of security vulnerabilities in software.

The report defines a minimum capability to help software professionals understand how a tool can help meet their software security assurance needs. The example languages studied are C, C++, Java and SPARK. SPARK, originally designed by Praxis, is a subset of Ada augmented with annotations (“contracts”) that assist in automated proof of program properties, such as freedom from exceptions. The NIST report identifies the languages’ vulnerabilities.

VulnerabilityApplicable to SPARK
Range Errors
   Stack OverflowNo vulnerability in SPARK
   Heap OverflowNo vulnerability in SPARK
   Format String VulnerabilityNo vulnerability in SPARK
   Improper Null TerminationNo vulnerability in SPARK
API Abuse
   Heap InspectionNo vulnerability in SPARK
   Often Misused: String ManagementNo vulnerability in SPARK
Time and State
   Unchecked Error ConditionNo vulnerability in SPARK
Code Quality
   Memory LeakNo vulnerability in SPARK
   Double FreeNo vulnerability in SPARK
   Use After FreeNo vulnerability in SPARK
   Uninitialized VariableNo vulnerability in SPARK
   Unintentional Pointer ScalingNo vulnerability in SPARK
   Null DereferenceNo vulnerability in SPARK

SPARK was designed to aid in safe and secure programming. By preventing vulnerabilities it reduces the cost of developing safe and secure software applications, by reducing the time spent in finding errors and testing to meet top safety and security standards. Such reductions are hard to quantify, but this report from NIST helps identify the types of security flaws that can be guaranteed to be prevented when SPARK is used.

The full report, Source Code Security Analysis Tool Functional Specification Version 1.1 (NIST Special Publication 500-268 v1.1), is available on the web via the following link: A detailed study on the SPARK language and vulnerabilities will be published shortly in a separate report, "Software Vulnerabilities Precluded by SPARK," by Dr. Joyce L Tokar and co-authors. This paper will be presented at the High Confidence Software and Systems (HCSS) 11th Annual Conference. See:

SPARK Pro, an open source tool set for SPARK, is available from AdaCore. See: for more information.

About Altran Praxis
Altran Praxis is a specialist systems and software house, focused on the engineering of systems with demanding safety, security or innovation requirements. Altran Praxis leads the world in specific areas of advanced systems engineering and innovation such as: ultra low defect software engineering, Human Machine Interface (HMI), safety engineering for complex or novel systems and tools (such as SPARK) /methods for systems engineering. It offers clients a range of services including turnkey systems development, consultancy, training and R&D. Key market sectors are aerospace and defense, rail, nuclear, air traffic management, automotive, medical and security. The company operates globally with active projects in the US, Asia and Europe. The headquarters of Altran Praxis are in Bath (UK) with offices in Sophia Antipolis, London, Paris, Loughborough and Bangalore. Altran Praxis is an expertise centre within, and wholly owned by, Altran which is a global leader in innovation engineering and employs 17,000 staff across the world.

About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see for further information.

Ada and GNAT Pro continue to see a growing usage in high-integrity and safety-certified applications, including commercial aircraft avionics, military systems, air traffic management/control, railroad systems, and medical devices, and in security-sensitive domains such as financial services.

AdaCore has North American headquarters in New York and European headquarters in Paris.

Press Contacts