NIST Report Shows SPARK Most Suitable Language for Secure Programming
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|
|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|
|Heap Inspection||No vulnerability in SPARK|
|Often Misused: String Management||No vulnerability in SPARK|
|Time and State|
|Unchecked Error Condition||No vulnerability in SPARK|
|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.