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.

2 entries written by Joffrey Huguet

by Joffrey Huguet, Johannes Kanig

Proving a simple program doing I/O ... with SPARK

The functionality of many security-critical programs is directly related to Input/Output (I/O). This includes command-line utilities such as gzip, which might process untrusted data downloaded from the internet, but also any servers that are directly connected to the internet, such as webservers, DNS servers and so on. In this blog post we show an approach that deals with error handling and reasoning about content, and demonstrate the approach using the cat command line utility.

#Formal Verification    #SPARK   

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