Here’s my recent keynote paper and talk from the SCSC SSS 2018 conference in York. The paper and slides are here for now. Video might follow in the near future.
Abstract: This paper reflects on the need for formality, discipline and humility in programming. Starting with the work of Turing, Dijkstra and Humphrey, this paper goes on to cover our experience with the Personal Software Process, formal programming with SPARK, and the impact of putting the two together.
The full reference is:
R. Chapman, “The Fumble Programmer” Invited Keynote Paper. Proc of the 26th Safety Critical Systems Symposium, York, UK, Feb 2018. pp. 143-154. Safety Critical Systems Club, UK. ISBN 978-1-9797-3361-8.
Last April, there was a discussion meeting at the Royal Society on “Verified trustworthy software systems.” The attendance and speakers were something of a who’s-who of the software verification community. The resulting issue of Royal Society Transactions A is now in print and on-line.
Our paper, co-authored with Neil White and Stuart Matthews from Altran UK, covers our experiences with building and applying formal verification to real-world industrial systems, and considers the incentives and barriers that seem to be holding back wider adoption of such technology. The full text is available on request from me by email.
Here’s the paper that I presented at Ada Europe this week in Vienna.
It deals with the tricky issue of how to erase or “sanitize” data in running software, so that it can’t be observed. Many coding standards and guidance documents for secure software say that we should do this for “sensitive” data such as the plaintext of passwords, cryptographic keys, and so on, but offer very little technical advice on how to do it properly. I had to implement this kind of thing for a recent development project and it turns out to be much harder to get right than you might think. The paper describes why it’s hard, what you can do about it.
Post conference note: the “further work” section proposes a special compiler switch that automatically erases local data before it goes out of scope. Recently, I have discovered that this has actually been implemented in LLVM by the team at Embecosm. See their blog entry here for details. It doesn’t look like their work has been contributed upstream to the main LLVM sources yet.
Stop press: I was awarded “Best presentation” for my talk on this work.
I’m pleased to see that the “all new” SPARK book was published this week. The book is by long-time SPARK users John McCormick and Peter Chapin. John has taught SPARK for many years as part of his real-time systems lab courses at UNI, while Peter is mainly known for his involvement in the remarkable Vermont CubeSat project, where the team used SPARK for the in-flight software.
The new book covers SPARK 2014, of course, in all its glory and the latest GPL release of the toolset. It’s aimed at an audience coming to SPARK (and Ada) for the first time, but it should also
be useful for those familiar with SPARK 2005.
The opening chapters covers the basics – SPARK’s type system, subprograms, packages and so on, before moving on to the more meaty stuff such as contracts, proof, and design issues.
The latter topic is particularly welcome – we always found that “design for verification” was a key driving force in the success (or otherwise…) of SPARK projects, but this topic was hardly touched on by other languages and design approaches.
I hope the book reaches a new audience of professors, students and engineers, raising awareness of SPARK and what it can do. A big thanks to John and Peter for their hard work in putting it together.
Here it is on amazon.co.uk.