Here’s my talk (including the Q&A session) about SPARKNaCl from FOSDEM yesterday…

FOSDEM 2022 SPARKNaCl

Last week, I was able to visit the University of Bristol CyberSecurity CDT and Cryptography groups to give a long-overdue seminar about SPARKNaCl. The talk goes into the motivation for development SPARKNaCl in the first place, the formal verification of the code, and the subsequent performance optimization work. The CDT staff were able to record the seminar and it’s now available here.

New  Third phase of performance analysis, improvement, and porting the library to GNAT and SPARK Community 2021 is written up here.

Second phase of performance analysis is now written up here.

I’m pleased to say that I’ve finished the first phase of performance analysis and tuning of the SPARKNaCl library. This has been something of a marathon, and touched on all sorts of interesting topics with SPARK, proof, language design, compiler internals, and the details of the RISC-V ISA and its implementation.

The write-up is on AdaCore’s blog as before. This is the most nerdy/technical thing I’ve worked on and written for ages, but please have a look. TL;DR version: formal is fast!

You can see all the updates and tagged snapshots of the code as I worked on it on SPARKNaCl’s GitHub Repo.

An update for SPARKNaCl in the ALIRE package manager will follow shortly.

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… 🙂

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

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.