Here’s some new software that I’ve been working on in my spare time over the last few months. I’ve decided to make the code freely available under the simplified BSD licence.

SPARKNaCl is a SPARK 2014 implemenation of the NaCl cryptographic library, based on the minimalistic TweetNaCl code from Daniel J. Bernstein and his colleagues.

SPARKNaCl has been verified “type-safe” (aka “no runtime errors”) by the SPARK toolset, and the proof is fully “auto-active” meaning the standard set of provers discharge every single verification condition, with no interactive proof at all, based solely on the contracts in the code and nothing else. In addition, some interesting correctness properties have been verified en-passant.

This was all something of a challenge – cryptographic code like TweetNaCl sets some particularly difficult challenges for both the human brain and for automated verification tools alike. Read all about it here.

Here’s the video from a talk that Neil White and I gave at BrisTech 2018 just before Christmas. BrisTech has grown into a great event in the last few years, with a big audience, a great venue, and a lot of competition for speaking slots.

Neil is Director of the Intelligent Systems Expertise Centre at Altran UK in Bath – the business that we used to call “Praxis” back in the day. He opens the talk by setting the scene and what makes critical software development so different, before I dive into the technical stuff regarding SPARK, static verification, and so on.

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.