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: 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.