Safer Languages
From SAMATE
Safety or quality cannot be "tested into" programs. It must be designed in from the start. Choosing to implement with a safer or more secure language or language subset can entirely avoid whole classes of weaknesses.
Some Instances
DISCLAIMER: Certain trade names and company products are mentioned in the text or identified. In no case does such identification imply recommendation or endorsement by the National Institute of Standards and Technology (NIST), nor does it imply that the products are necessarily the best available for the purpose.
By selecting almost any of these links, you will be leaving NIST webspace. We provide these links because they may have information of interest to you. No inferences should be drawn because some sites are referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the assertions presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites.
By selecting almost any of these links, you will be leaving NIST webspace. We provide these links because they may have information of interest to you. No inferences should be drawn because some sites are referenced, or not, from this page. There may be other web sites that are more appropriate for your purpose. NIST does not necessarily endorse the views expressed, or concur with the assertions presented on these sites. Further, NIST does not endorse any commercial products that may be mentioned on these sites.
Please contact us if you think something should be included. If it
has all the characteristics of the tool, techniques, etc., we will be
happy to add it. You can contact us at
.
- SPARK is a well-defined language for high integrity applications in which many errors are impossible and which has decades of proven results. Available from AdaCore (7 Jan 2013)
- Escher C Verifier language is a subset of C and C++ based on MISRA-C, with a stronger type system and preconditions. A theorem prover, eCv, can verify such programs. Escher Technologies also has the Perfect specification language, which works with SPARK Ada, too. (9 Apr 2013)
- Fail-Safe C disallows any unsafe memory operation in "full ANSI C standard (including casts and unions)" and even supports many "dirty tricks" common in non-conforming programs. (20 Nov 2006)
- Safe-Secure C/C++ (SSCC) "is a software component that can be integrated into compilers and software analysis tools to detect and prevent buffer overflows and other common security vulnerabilities in C and C++ programs".
- CERT's Secure Coding Standards is a broad-based effort which, if followed, prevents many frequent vulnerabilities. The language-independent practices are supplemented by some particular to C, some particular to Java, and some particular to C++.
- SC 22/OWG: Vulnerabilities OWGV Project 22.24772 is preparing Guidance for Avoiding Vulnerabilities through Language Selection and Use. It will have guidance on avoiding vulnerabilities from "constructs that are undefined, imperfectly defined, implementation-dependent, or difficult to use correctly." It can also be used to "select source code evaluation tools that can discover and eliminate coding errors that lead to vulnerabilities." (19 Jul 2007)
- CCured adds a minimal number of run-time checks (in C) to C programs "to prevent all memory safety violations. The resulting program is memory safe, meaning that it will stop rather than overrun a buffer or scribble over memory that it shouldn't touch." (25 Feb 2005)