AdaCore Blog

Joffrey Huguet

Joffrey is a graduate student at ISAE-SUPAERO in Toulouse, France. He wrote SPARK By Example during a previous internship and is currently at AdaCore doing a 6 months internship on SPARK libraries.

1 entries written by Joffrey Huguet

by Joffrey Huguet

Using SPARK to prove 255-bit Integer Arithmetic from Curve25519

In 2014, Adam Langley, a well-known cryptographer from Google, wrote a post on his personal blog, in which he tried to prove functions from curve25519-donna, one of his projects, using various verification tools: SPARK, Frama-C, Isabelle... He describes this attempt as "disappointing", because he could not manage to prove "simple" things, like absence of runtime errors. I will show in this blogpost that today, it is possible to prove what he wanted to prove, and even more.

#SPARK    #Formal Verification    #Cryptography