AdaCore Blog

SPARKNaCl - Two Years of Optimizing Crypto Code in SPARK (and counting)

by Yannick Moy

SPARKNaCl is a SPARK ver­sion of the Tweet­Na­Cl cryp­to­graph­ic 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.

Rod Chapman - SPARKNaCl: a verified, fast re-implementation of TweetNaCl

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:

  1. Proving properties of constant-time crypto code in SPARKNaCl
  2. Performance analysis and tuning of SPARKNaCl
  3. Doubling the Performance of SPARKNaCl (again...)
  4. SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance

Makes for nice reading over Christmas!

Posted in #SPARK    #Cryptography    #Formal Verification   

About Yannick Moy

Yannick Moy

Yannick Moy is Static Analysis Lead at AdaCore. Yannick leads 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 Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.