Modern software development increasingly depends on integrating components developed by different teams, or even vendors. For security-critical applications, it is important to ensure that secrets (for example cryptographic keys) that should be contained in one component cannot be leaked to components that should have no access to the secret. In safety-critical applications, it has to be shown that the asserted safety of one component is not compromised when it is integrated with a component of a lower safety level. Chapman and Hilton present some ideas about how to analyze possible security violations, using an extension to the SPARK Examiner, a tool for information flow analysis in certain annotated Ada programs. They also show that the same techniques can be used to analyze whether integrating components at two differing safety levels compromises the safety of the whole application.

The paper starts with a short, motivating introduction. In the second section, the authors’ work is put into context, with a brief explanation of the different industry standards for secure and safe applications. The work seeks to achieve relatively high security and safety levels. The next parts of this section explain the difference between data flow analysis (direction of data flow) and information flow analysis (coupling between variables), hint very briefly at the basic ideas of two security models, present a very short overview of work on information flow analysis in Ada, and give examples of security- and safety-critical applications that were developed with the SPARK subset of Ada. The main body of the paper is section 3, where some of the technical ideas behind the extended SPARK examiner are explained, design decisions are discussed, and examples are given. This section also contains an overview of a case study conducted with a military information system, the lessons learned from this case study, and extensions of the work done so far. The last two sections contain issues for further research, and a short conclusion.

The major fault of this paper is its shortness; several ideas are only hinted at. There is barely enough information to see that the work is interesting and relevant. For a certain subset of the Ada community, this may be sufficient, but for users of other languages, or the general computer science public, too much information is missing. This could have been a very interesting paper, if the authors had managed to explain their ideas in a much more language-independent and general way, with more detail. As it is, the paper is of interest mostly to users of Ada, and even they will probably need correspondence with the authors to fill in the missing details, if they want to apply the ideas presented. There isn’t even information on how to obtain the extension to the SPARK examiner discussed in the paper.