AdaCore Blog

Roderick Chapman

Roderick Chapman

Rod is Director of Protean Code Limited. He specializes in the design, implementation and verification of high-integrity software systems. For many years, Rod led the SPARK design team at Praxis and Altran in the UK, and continues to work closely with the SPARK team at AdaCore.

4 entries written by Roderick Chapman

by Roderick Chapman

SPARKNaCl with GNAT and SPARK Community 2021: Port, Proof and Performance

This post continues our adventures with SPARKNaCl - our verified SPARK version of the TweetNaCl cryptographic library. This time, we'll be looking at yet more performance improvement via proof-driven "operator narrowing", porting the library to GNAT Community 2021, and the effect that has on proof and performance of the code.

#SPARK #Cryptography #Formal Verification #Code generation #RISC-V #Security

by Roderick Chapman

Doubling the Performance of SPARKNaCl (again...)

Following my last blog entry, further experiments show how the performance of SPARKNaCl can be doubled (again), plus analysis of worst-case stack usage and code size at all optimization levels.

#SPARK #Cryptography #Formal Verification #Code generation #RISC-V #Security

by Roderick Chapman

Performance analysis and tuning of SPARKNaCl

This blog goes into the details of both measuring and improving the runtime performance of SPARKNaCl on a real "bare metal" embedded target, and comparing results with those for the original "TweetNaCl" C implementation.

#SPARK #Cryptography #Formal Verification #Code generation #RISC-V #Security

by Roderick Chapman

Proving properties of constant-time crypto code in SPARKNaCl

Over the last few months, I developed a SPARK version of the TweetNaCl cryptographic library. This was made public on GitHub in February 2020, under the 2-clause BSD licence. This blog entry goes into a bit more technical detail on one particular aspect of the project: the challenge of re-writing and verifying "constant time" algorithms using SPARK.

#SPARK #Cryptography #Formal Verification