SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)
by Yannick Moy –
SPARKNaCl is a SPARK version of the TweetNaCl cryptographic library, developed by formal methods and security expert Rod Chapman. For two years now, Rod has been developing and optimizing this open-source cryptographic library while preserving the automatic type-safety proof across code changes and tool updates. He has recently given a talk about this experience that I highly recommend.
In case you'd like to know more, but you're not yet ready to jump into the code on GitHub, you can check out the blog series that Rod has posted over the last two years about the project:
- Proving properties of constant-time crypto code in SPARKNaCl
- Performance analysis and tuning of SPARKNaCl
- Doubling the Performance of SPARKNaCl (again...)
- SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance
Makes for nice reading over Christmas!
About Yannick Moy
Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.