4-lowlevel.tex 1.21 KB
Newer Older
1
\section{Proving equivalence of X25519 in C and Coq}
Benoit Viguier's avatar
Benoit Viguier committed
2
\label{sec:C-Coq}
Benoit Viguier's avatar
Benoit Viguier committed
3

4
5
In this section we prove the following theorem:
% In this section we outline the structure of our proofs of the following theorem:
Benoit Viguier's avatar
Benoit Viguier committed
6

Benoit Viguier's avatar
Benoit Viguier committed
7
\begin{informaltheorem}
8
9
  The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches
  the specifications of RFC~7748~\cite{rfc7748} (\Coqe{RFC}).
Benoit Viguier's avatar
Benoit Viguier committed
10
11
\end{informaltheorem}

Benoit Viguier's avatar
Benoit Viguier committed
12
13
14
15
16
More formally:
\begin{lstlisting}[language=Coq]
Theorem body_crypto_scalarmult:
  (* VST boiler plate. *)
  semax_body
17
    (* Clight translation of TweetNaCl.  *)
Benoit Viguier's avatar
Benoit Viguier committed
18
    Vprog
Benoit Viguier's avatar
Benoit Viguier committed
19
    (* Hoare triples for fct calls. *)
Benoit Viguier's avatar
Benoit Viguier committed
20
21
22
    Gprog
    (* fct we verify. *)
    f_crypto_scalarmult_curve25519_tweet
Benoit Viguier's avatar
Benoit Viguier committed
23
    (* Our Hoare triple, see below. *)
Benoit Viguier's avatar
Benoit Viguier committed
24
25
    crypto_scalarmult_spec.
\end{lstlisting}
26

27
% We first describe the global structure of our proof (\ref{subsec:proof-structure}).
Benoit Viguier's avatar
Benoit Viguier committed
28
Using our formalization of RFC~7748 (\sref{sec:Coq-RFC}) we specify the Hoare
Benoit Viguier's avatar
Benoit Viguier committed
29
triple before proving its correctness with VST (\ref{subsec:with-VST}).
30
We provide an example of equivalence of operations over different number
Benoit Viguier's avatar
Benoit Viguier committed
31
representations (\ref{subsec:num-repr-rfc}).
32
% Then, we describe efficient techniques used in some of our more complex proofs (\ref{subsec:inversions-reflections}).