SPARK Conference Papers

Where indicated, PDF downloads of these publications are available for download here. Where PDF is not available, please contact us for how to obtain hardcopies.

2006

"Engineering the Tokeneer Enclave Protection Software"
Janet Barnes, Rod Chapman: Praxis High Integrity Systems. Randy Johnson, James Widmaier: National Security Agency. David Cooper: River River Limited. Bill Everett: SPRE Inc.
Proceedings of the IEEE International Symposium on Secure Software Engineering (ISSSE) 2006.

Abstract. The Tokeneer ID Station (TIS) project, carried out by Praxis High Integrity Systems in conjunction with SPRE Inc. under the direction of NSA, has shown that it is possible to produce high quality, low defect systems conforming to the Common Criteria requirements for Evaluation Assurance Level 5 (EAL5). We state the seven guiding principles we used to achieve this, and relate each one to examples from the TIS development. The systems development industry in general has viewed conformance with the Common Criteria higher levels as too difficult, too expensive, and generally not economical. The experience of Praxis High Integrity Systems, however, is that the levels of EAL5 and beyond (including EAL7) are achievable in a cost-effective manner. This TIS project was commissioned as a demonstration vehicle, to show exactly how the development approach adopted by Praxis matches up to EAL5, and to measure its actual productivity and defect rates under controlled conditions.

2005

"Modeling SPARK systems with UML"
Xavier Sautejeau - Sodius
Proceedings of the ACM SIGAda Annual International Conference (SIGAda 2005), November 2005
Abstract
In this paper, we will consider two aspects of UML in order to assess how well suited it is for modeling SPARK systems. The first aspect is the ability to represent SPARK in UML from a theoretical perspective. The second aspect is more from a hands-on perspective and evaluates what makes a UML CASE-tool more suitable for modeling SPARK systems than another.

"Optimizing the SPARK program slicer"
Ricky E. Sward, Leemon C. Baird, Department of Computer Science, US Air Force Academy, CO
Proceedings of the ACM SIGAda Annual International Conference (SIGAda 2005), November 2005
Abstract
Recent trends in software re-engineering have included tools to extract program slices from existing Ada procedures. One such tool has already been developed that extracts program slices from SPARK procedures along with a proof that the functionality of the original procedure is equivalent to the functionality of the collection of resulting slices. This paper extends this work by showing how assumptions in the proof can cause inefficiencies in SPARKSlicer and by presenting alternatives that optimize out the inefficiencies. The original proof is modified to show that the SPARK program slicer still produces functionally equivalent program slices from SPARK procedures with these optimizations.

"Experiences using SPARK in an Undergraduate CS Course"
Dr Anthony S Ruocco, Roger Williams University
Proceedings of the ACM SIGAda Annual International Conference (SIGAda 2005), November 2005
Abstract
This paper describes experiences garnered while teaching a course on high integrity software using SPARK to a mix of junior and senior level undergraduates. The paper describes the impact of pre-requisites, course layout and execution, and lessons learned by students and the instructor. The course used the SPARK toolset provide by Praxis High Integrity Systems, and the Gnat Programming System (GPS) provided by AdaCore Technologies (ACT) under the Ada Academic Initiative Program. Details about using these tools is integrated through out the paper.

"The Affordable Application of Formal Methods to Software Engineering"
James F Davis, University of Maryland University College
Proceedings of the ACM SIGAda Annual International Conference (SIGAda 2005), November 2005
Abstract
The purpose of this research paper is to examine (1) why formal methods are required for software systems today; (2) the Praxis High Integrity Systems' Correctness by Contruction methodolgy; and (3) an affordable application of a formal methods methodology to software engineering.

Languages, Ambiguity, and Verification
SPARK team
Verified Software: Theories, Tools, Experiments, ETH Zürich 10-13 October 2005
Abstract
This position paper is based on presentations given at the Grand Challenge workshops held at Gresham College in March 2004 and in Newcastle in July 2005. It reports some of our experience from building the SPARK lan-guage and its verification tools. We argue that the provision of an unambiguous semantics for a programming language is crucial if the verification framework is to be sound, deep and efficient. Secondly, we offer some reflections on the (mostly non-technical) barriers that we encounter in trying to deploy SPARK within organizations. Finally, we try to set some goals for future.

Smart Certification Of Mixed Criticality Systems
Peter Amey, Rod Chapman, Neil White, Praxis High Integrity Systems
AdaEurope 2005
Abstract
High integrity applications, such as those performing safety or security critical functions, are usually built to conform to standards such RTCA DO- 178B [1] or UK Def Stan 00-55 [2]. Typically such standards define ascending levels of criticality each of which requires a different and increasingly onerous level of verification. It is very common to find that real systems contain code of multiple criticality levels. For example, a critical control system may generate a non-critical usage log. Unless segregation can be demonstrated to a very high degree of confidence, there is usually no alternative to verifying all the software components to the standard required by the most critical element, leading to an increase in overall cost. This paper describes the novel use of static analysis to provide a robust segregation of differing criticality levels, thus allowing appropriate verification techniques to be applied at the subprogram level. We call this fine-grained matching of verification level to subprogram criticality smart certification.

2004

Enforcing Security and Safety Models with an Information Flow Analysis Tool
Rod Chapman and Adrian Hilton, Praxis High Integrity Systems
SIGAda 2004

"High-Integrity Ada in a UML and C World" (PDF 876kb)
© Springer-Verlag
Peter Amey and Neil White, Praxis,
Lecture Notes in Computer Science 3063
A. Llamosi, A. Strohmeier (Eds.):
Reliable Software Technologies – Ada-Europe 2004
9th Ada-Europe International Conference, La Palma de Mallorca, June 2004, pp. 225-236.
Abstract
The dictates of fashion and the desire to use "hot" technology not only affects software developers but also influences potential customers. Where once a client was just content to accept something that worked (actually, would be delighted to have something that worked) now they are concerned about the means by which it was constructed; not just in the sense of was it well-enough constructed but in the more malign sense of was fashionable technology used. This paper shows how the customer's desire to use de facto standards such as UML and their wish to use language such as C—perhaps to support a small or unusual processor; to integrate with other subsystems; for the perceived comfort of future portability; or for other, non-technical reasons—can be aligned with the professional engineer's need to use those tools and languages which are truly appropriate for rigorous software development.

"High-Integrity Interfacing to Programmable Logic with Ada" (PDF 318kb)
© Springer-Verlag
Adrian J Hilton, Praxis and
Jon G Hall, Open University.
Lecture Notes in Computer Science 3063
A. Llamosi, A. Strohmeier (Eds.):
Reliable Software Technologies – Ada-Europe 2004
9th Ada-Europe International Conference, La Palma de Mallorca, Spain, June 2004, pp. 249-260.
Abstract
Programmable Logic Devices (PLDs) are now common components of safety-critical systems, and are increasingly used for safety-related or safety-critical functionality. Recent safety standards demand similar rigour in PLD specification, design and verification to that in critical software design. Existing PLD development tools and techniques are inadequate for the higher integrity levels. In this paper we examine the use of Ada as a design language for PLDs. We analyse earlier work on Ada-to-HDL compilation and identify where it could be improved. We show how program fragments written in the SPARK Ada subset can be efficiently and rigorously translated into PLD programs, and how a SPARK Ada program can be effectively interfaced to a PLD program. The techniques discussed are then applied to a substantial case study and some preliminary conclusions are drawn from the results.

"An Integration of Program Analysis and Automated Theorem Proving"
Bill J. Ellis and Andrew Ireland, Heriot-Watt University
Integrated Formal Methods: 4th International Conference, IFM 2004,
Abstract
Finding tractable methods for program reasoning remains a major research challenge. Here we address this challenge using an integrated approach to tackle a niche program reasoning application. The application is proving exception freedom, i.e. proving that a program is free from run-time exceptions. Exception freedom proofs are a significant task in the development of high integrity software, such as safety and security critical applications. The SPARK approach for the development of high integrity software provides a significant degree of automation in proving exception freedom. However, when the automation fails, user interaction is required. We build upon the SPARK approach to increase the amount of automation available. Our approach involves the integration of two static analysis techniques. We extend the proof planning paradigm with program analysis.

"Invariant Patterns for Program Reasoning"
Andrew Ireland, Bill J. Ellis and Tommy Ingulfsen, Heriot-Watt University
MICAI 2004: Advances in Artificial Intelligence: Third Mexican International Conference on Artificial Intelligence
Abstract
We address the problem of integrating standard techniques for automatic invariant generation within the context of program reasoning. We propose the use of invariant patterns which enable us to associate common patterns of program code and specifications with invariant schemas. This allows crucial decisions relating to the development of invariants to be delayed until a proof is attempted. Moreover, it allows patterns within the program to be exploited in patching failed proof attempts.

"Dear Sir, Yours Faithfully: an Everyday Story of Formality" (PDF 120kb)
Peter Amey, Praxis High Integrity Systems,
Invited keynote address, in "Practical Elements of Safety", Proceedings of the Twelfth Safety-critical Systems Symposium, Birmingham, UK, February 2004. Copyright Spinger-Verlag 2004. ISBN 1-85233-800-8.
Abstract
This paper seeks a perspective on the reality of formal methods in industry today. What has worked; what has not; and what might the future bring? We show that where formality has been adopted it has largely been beneficial. We show that formality takes many forms, not all of them obviously "Formal Methods".

2003

"Static Verification and Extreme Programming" (PDF 252kb) Peter Amey and Roderick Chapman. Proceedings of the ACM SIGAda Conference, December 2003.
Abstract
At first glance, the worlds of high-integrity software engineering and Extreme Programming (XP) seem to have little in common. Somewhat surprisingly, we have found the reverse to be the case – indeed it seems that many practices advocated by the XP community are familiar to us from many years' of experience in building safety – and security-critical systems. This paper discusses our experiences in applying some XP practices in critical projects. Secondly, we discuss how static verification can augment XP, particularly in the Pairwise Programming and Refactoring practices.

"On the Principled Design of Object-Oriented Programming Languages for High-Integrity Systems" (PDF 225kb) Roderick Chapman, Janet Barnes, and Brian Dobbing. Submitted as a position paper to the 2nd NASA/FAA Object Oriented Technology in Aviation Workshop.
Abstract
This paper describes the key properties and design principles that make a programming language suitable for the construction of high-integrity systems, with particular emphasis on object-oriented language features, such as inheritance and dynamic-dispatch. The paper goes on to describe how these principles have been applied in the design of SPARK, which was recently extended to include a subset of Ada95's tagged types facility. The central thesis of the paper is that the ability to statically analyse the behaviour of software should be a strong guiding principle in the selection of language features for high-integrity systems development – features that defy static analysis and complicate verification should be excluded.

"High Integrity Ravenscar" (PDF 53kb)
Peter Amey and Brian Dobbing, 2003. From Proceedings of Reliable Software Technologies – Ada Europe 2003.
Lecture Notes in Computer Science Volume 2655
(c) Springer-Verlag 2003.
Abstract
The Ravenscar Profile is an exciting development for the Ada community since it provides, for the first time in the history of our industry, support for deterministic, multi-tasking programming as an integral part of a standardized language. Despite its many advantages, the profile leaves several areas where behaviour is implementation defined and can result in run-time errors; this is unfortunate in a profile aimed clearly at the critical systems market. The SPARK language is a well-established sequential Ada subset that avoids ambiguity and allows all language rule violations to be detected prior to execution. The authors show how the principles of SPARK have been successfully extended to encompass the Ravencar Profile thereby statically eliminating the profile’s problematic areas. The result should allow concurrent Ada programs to be constructed with the same degree of rigour that is now possible using sequential SPARK.

"Automation for Exception Freedom Proofs"
Bill J. Ellis and Andrew Ireland, Heriot-Watt University
18th IEEE International Conference on Automated Software Engineering (ASE'03), 2003.
Abstract
Run-time errors are typically seen as unacceptable within safety and security critical software. The SPARK approach to the development of high integrity software addresses the problem of run-time errors through the use of formal verification. Proofs are constructed to show that each run-time check will never raise an error, thus proving freedom from run-time exceptions. Here we build upon the success of the SPARK approach by increasing the level of automation that can be achieved in proving freedom from exceptions. Our approach is based upon proof planning and a form of abstract interpretation.

2002

"Closing the loop – The Influence of Code Analysis on Design" (PDF 214kb)
© Springer-Verlag
Peter Amey, Praxis,
Lecture Notes in Computer Science 2361
J. Bliebergerand A. Strohmeier (Eds.):
Reliable Software Technologies – Ada-Europe 2002
7th Ada-Europe International Conference, Vienna, June 2002
Abstract
Static code analysis originally concerned the extraction from source code of various properties of a program. Although this kind of reverse engineering approach can uncover errors that are hard to detect in other ways, it is not a very efficient use of resources because of its retrospective nature and the late error detection that results. The SPARK language and its associated Examiner tool took a different approach which emphasises error prevention ("correctness by construction") rather than error detection. Recent work with SPARK has shown that very early application of static analysis can have a beneficial influence on software architectures and designs. The paper describes the use of SPARK to
produce designs with demonstrably low coupling and high cohesion.

"Industrial Strength Exception Freedom" (PDF 231kb)
Roderick Chapman and Peter Amey, Praxis. Proceedings of ACM SigAda 2002.
Abstract
Ada is unique amongst modern high-level languages in the degree to which it allows programming errors to be trapped at the compilation stage. Using a tool like the SPARK Examiner amplifies this effect and can provide a high degree of confidence that a program is well formed before we try and verify that its behaviour is correct. Despite this progress a less tractable class of errors remain: run-time exceptions. For safety-related systems a run-time error may be just as hazardous as any other logical error. For secure systems guarding against the deliberate generation of such errors, through buffer overflow attacks for example, is vital. The paper explains how automated techniques based on formal verification or proof techniques have now matured and provide an industrial strength solution.

2001

"A Language for Systems not just Software" (PDF 271kb)
Peter Amey, Praxis, September 2001.
This paper was presented at the ACM SigAda 2001 conference, in Minneapolis, USA.

"SPARK – a state-of-the-practice approach to the Common Criteria implementation requirements" (PDF 223kb)
Rod Chapman, Praxis. Presented at the 2nd International Common Criteria Conference, Brighton, UK, July 2001
Abstract
The Common Criteria (CC) require the use of programming languages whose statements have an "unambiguous meaning". This presentation considers SPARK: 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.
The design principles of SPARK will be described, highlighting the language's suitability for meeting the requirements of secure systems development. SPARK's static analysis tool (the Examiner) will also be considered, concentrating on the types of analysis, such as information flow analysis and proof of exception freedom, that can be achieved. The strengths of the language will be illustrated with reference to the MULTOS Global Key Centre (MGKC) – the system at the heart of the MULTOS CA – which was developed by Praxis High Integrity Systems using SPARK to meet the requirements of ITSEC E6.

2000

"The SPARK Way to Correctness is via Abstraction"
John Barnes, presented at Sig-Ada 2000.
Abstraction is a key concept in the design and implementation of systems. In a good system, the various components will interact only through well-defined interfaces – in Ada, these interfaces are provided through package specifications. However, subprogram specifications do not limit the behaviour of the subprogram, they only define how the subprogram is called. The use of SPARK allows Ada specifications to be strengthened to several levels – at the simplest level, SPARK annotations will prevent unexpected side effects, while at the highest level, SPARK can lead to complete proofs of correctness.

"Cost-Effective Approaches to Safetify Safety-Critical Regulatory Requirements"
James Sutton, Lockheed Martin, Presented in workshop session at SigAda 2000.

"Industrial Experience with SPARK" (PDF 234kb)
Dr. Roderick Chapman, Praxis High Integrity Systems Limted. Presented at ACM SigAda 2000 conference.
This paper discusses three large, real-world projects (C130J, SHOLIS and the MULTOS CA) where SPARK has made a contribution to meeting stringent software engineering standards.

1999

"Re-engineering a Safety-Critical Application with SPARK95 and GNORT" (PDF 67kb)
Roderick Chapman and Robert Dewar,
Lecture Notes in Computer Science 1622
Reliable Software Technologies – Ada-Europe '99
(c) Springer-Verlag 1999.
A paper about porting the SHOLIS project software to SPARK95 using ACT's GNAT-No-Runtime (GNORT) technology. This paper was presented at the 1999 Ada Europe conference, and went on to win the conference prize for best presentation.

1995

"Breaking Through the V and V Bottleneck" (PDF 255kb)
Martin Croxford and James Sutton. Presented at Ada Europe 1995,
Published by Springer-Verlag in "Lecture Notes in Computer Science" Volume 1031, 1996.
This paper presents a method of software development aimed at "correctness by construction", which greatly attenuates problems and costs associated with the detection of errors at a late phase of the lifecycle. The process described here has been applied successfully to the development of avionic software for the C-130J aircraft.