January 10, 2012 -- In part one of this two-part article, we summarized the basic issues with software security and explained how the programming language choice can affect the ease or difficulty of demonstrating that a system meets security requirements such as those defined in the Common Criteria. General-purpose languages including C, C++, Ada, and Java are too complex to satisfy the reliability and analyzability requirements at the highest security levels; sub-setting is needed. In part two, we describe one such language subset — SPARK — and explain how it can be used to develop high-security systems cost-effectively.

By Benjamin M. Brosgol. (Brosgol is a senior member of the technical staff of AdaCore.)