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.
| Vulnerability | Applicable to SPARK |
|---|---|
| Range Errors | |
| Stack Overflow | No vulnerability in SPARK |
| Heap Overflow | No vulnerability in SPARK |
| Format String Vulnerability | No vulnerability in SPARK |
| Improper Null Termination | No vulnerability in SPARK |
| API Abuse | |
| Heap Inspection | No vulnerability in SPARK |
| Often Misused: String Management | No vulnerability in SPARK |
| Time and State | |
| Unchecked Error Condition | No vulnerability in SPARK |
| Code Quality | |
| Memory Leak | No vulnerability in SPARK |
| Double Free | No vulnerability in SPARK |
| Use After Free | No vulnerability in SPARK |
| Uninitialized Variable | No vulnerability in SPARK |
| Unintentional Pointer Scaling | No vulnerability in SPARK |
| Null Dereference | No 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: http://samate.nist.gov/docs/source_code_security_analysis_spec_SP500-268_v1.1.pdf 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: http://hcss-cps.org/hcssc.html.
SPARK Pro, an open source tool set for SPARK, is available from AdaCore. See: http://www.adacore.com/home/products/sparkpro 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. www.altran-praxis.com
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 http://www.adacore.com/home/company/customers/ 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. www.adacore.com
Press Contacts
press@adacore.com