SPARK — a state-of-the-practice approach to the Common Criteria implementation requirements
Roderick Chapman · 2001
The Common Criteria (CC) require the use of programming languages whose statements have an "unambiguous meaning." This presentation considers SPARK[1]: a widely-used language that is perhaps unique in actually meeting this requirement. While SPARK has its roots in security research, it is currently most widely used in the aerospace and rail industries, and has a well-established track record in meeting the most demanding standards in these domains, such as UK Def. Stan. 00-55 (for military systems) and DO-178B (for civil aviation). SPARK has recently proven, though, to be ideally suited to the development of secure systems.