Enhance Security with Ada
Security is an increasingly critical requirement in software these days. Sometimes this can be addressed simply by verifying user-supplied input data, regardless of the language that the software is written in. But more generally — and especially at the higher levels of security — ensuring the correctness of the security-related functions and the absence of application vulnerabilities requires careful analysis, and the programming language choice makes a difference. Ada offers a number of advantages (such as strong typing, scalar subranges) and has a successful track record in the high-security domain.
This section collects a number of articles on creating secure systems with Ada. Closely related is the creation of high-integrity software; articles on that topic are collected in Ada Helps Build Safe Systems.
  • Current AdaIC articles
    This is the AdaIC archive site; for newer articles on safety, click the link above, then the "Security" tag (found in the upper right corner of the page).
  • NSA case study on zero-defect software uses Ada
    The NSA funded a case study showing that cost-effective zero-defect software development is possible using Ada (via the SPARK subset).
  • Safety and Security: Certification Issues and Technologies
    A Crosstalk article discussing language-related issues that occur meeting higher levels of safety and security standards when developing software. The article constrasts Ada with various other languages.
  • Need Secure Software?
    An article from Application Software Developer describes how Ada is a good match for the "Common Criteria" for developing secure systems.
  • Praxis HIS Produces Secure Software for NSA
    The NSA commissioned ARA member Praxis to develop secure software for an experimental biometric access control system to meet or exceed Evaluation Assurance Level 5 (out of 7) in the Common Criteria.
  • SPARK is featured in the article Mathematical Approaches to Managing Defects on The Register's developer site. It discusses ways to replace testing with proof of correctness. (SPARK is an Ada subset dedicated to program correctness.)
  • The NSA has certified the Janus cryptographic engine by Rockwell Collins (press release). This is a SPARK project using the GNAT Ada compiler.