New paper: Sanitizing sensitive data: how to get it right (or at least less wrong…)

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.

Think you know C? Think again…

There’s a great article in the latest issue of ACM Queue about the effects of uninitialized variables in C by Robert Seacord.  See here https://queue.acm.org/app/

Robert is a noted expert and was the principal author of the CERT C Coding Standard, so he really does know what he’s on about.  The good news: the article is the most complete and up-to-date treatment of this topic that I know of – I certainly learned lots from it, especially with regard to what C’11 has to say.  The bad news: it’s worse, much worse, than you think…

Question: would it be possible to define a subset of C which is both useful and guarantees sound data-flow analysis in P-Time? I fear the answer is “no”…  ho hum… I’ll stick to SPARK thanks… 🙂

 

Short talk about High Integrity Agile

For a while now, I’ve been working with my colleagues at Altran on “High Integrity Agile” – basically trying to work out how we can combine the best bits of the Agile Manifesto with what we already know from Lean, Formal Methods, Correctness-by-Construction, TSP and so on. The other week I gave a short talk on the subject at the invitation of Chris Hills from Phaedrus Systems. This covers a few of the issues we’ve encountered so far.  Chris has posted a lightly-edited video of the talk, and I’m pleased to say that I didn’t appear to say anything overtly stupid or embarrassing, so here it is…

Many thanks to Altran UK for supporting this work, and approval to post the video.

New SPARK 2014 Book Published

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.

SCSC Agile Development for Safety Systems conference

I was lucky enough to attend and speak at this event in London on 25th June. I was talking about recent work I’ve been doing for a client on “High Integrity Agile” – basically trying to find the right combination of Lean, Agile, and Formal approaches for a high integrity project.

The speakers also included Felix Redmill, speaking about his experience with “Evolutionary Development” in the 1980s that led to his excellent (and recently re-published) book on the subject.

The key-note speaker was Professor Bertrand Meyer, whose recent book “Agile: The Good, the Hype and the Ugly” has caused something of a stir. The book is a plain-speaking critique of the Agile approach and doesn’t pull its punches. There’s also an on-demand version of a recent ACM webinar that Bertrand gave on the same subject which is worth a look.

Slides from the SCSC event are now available here.

Update: a short video shot at the event is now available here.

Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK

For a long time at Praxis/Altran, we tried to publish results from projects,
particularly those using SPARK. Sometimes we succeeded, but more often than
not the projects or clients weren’t happy with the idea, so the projects
and their results remain pretty much invisible.

I wanted to write a review paper going over all the projects for a while,
and the opportunity finally arose with this year’s Interactive Theorem Proving
Conference (ITP 2014) in Vienna, where I was asked to deliver some sort of keynote.

So…we sat down and tried to write a “life and times of theorem proving
with SPARK”, starting with the SHOLIS project in 1995, and (finally!)
closing with some data from the NATS iFACTS project and some other more
recent efforts. We also decided to alternate the project stories with
the technical developments in the language and toolset, so the story
closes with a preview of SPARK 2014, which is basically a complete
reboot of the language and toolset.

In the Summer, I was in the middle of setting up Protean Code and doing
a few other things, so I couldn’t attend the conference in the end, but
Florian Schanda from SPARK team was able to go in my place, and did a great
job presenting the story.

Having actually read Springer’s copyright assignment form for the N’th
time, I realised that I could put it up here for those that don’t have
access to LNCS online.

The full reference is

“Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK”
Proc Interactive Theorem Proving 2014. July 2014. Springer-Verlag LNCS, vol 8558, pp. 17 – 26.
DOI: 10.1007/978-3-319-08970-6_2

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-319-08970-6_2

A (short) talk about PSP…

At the recent TVS Intelligent Testing event in Bristol, I was asked to give a 20-minute talk about PSP. This seemed like a challenge, so I went for it…is it possible to say something useful in such a short time? How fast can I actually talk? Did any of the jokes work? The slides and audio track are now on-line, thanks to the folks at TVS. Click here to see what happened.