code-tweetnacl.tex 2.64 KB
Newer Older
1
\section{The complete X25519 code from TweetNaCl}
Benoit Viguier's avatar
Benoit Viguier committed
2
\label{verified-C-and-diff}
3

4
5
\subheading{Verified C Code} We provide below the code we verified.

Benoit Viguier's avatar
Benoit Viguier committed
6
\lstinputlisting[linerange={2-5,8-9,266-317,333-380,393-438},language=Ctweetnacl]{../proofs/vst/c/tweetnaclVerifiableC.c}
benoit's avatar
benoit committed
7
~
8

Benoit Viguier's avatar
Benoit Viguier committed
9
\subheading{Diff from TweetNaCl} We provide below the diff between the original code of TweetNaCl and the code we verified.
10
11

\lstinputlisting[language=diff]{tweetnacl.diff}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
12

13
In the following, we provide the explanations of the above changes to TweetNaCl's code.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
14
15

\begin{itemize}
Benoit Viguier's avatar
Benoit Viguier committed
16
  \item lines 7-8: We tell VST that \TNaCle{long long} are
Benoit Viguier's avatar
Benoit Viguier committed
17
  aligned on 8 bytes.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
18

Benoit Viguier's avatar
Benoit Viguier committed
19
  \item lines 16-23: We remove the the undefined behavior as explained in \sref{sec:Conclusion}.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
20

Benoit Viguier's avatar
Benoit Viguier committed
21
  \item lines 29-31; lines 60-62: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
22

Benoit Viguier's avatar
bib    
Benoit Viguier committed
23
  \item lines 39 \& 41: We initialize \TNaCle{m} with \TNaCle{0}.
Benoit Viguier's avatar
Benoit Viguier committed
24
25
26
  This change allows us to prove the functional correctness of \TNaCle{pack25519} without having to deal with an array containing
  a mix of uninitialized and initialized values.
  A hand iteration over the loop trivially shows that no uninitialized values are used.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
27

Benoit Viguier's avatar
Benoit Viguier committed
28
  \item lines 40 \& 42; lines 70 \& 71: We replace the \TNaCle{FOR} loop by \TNaCle{set25519}. The code is the same once the function is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
29

Benoit Viguier's avatar
Benoit Viguier committed
30
  \item lines 50-52: VST does not allow computation in the argument before a function call. Additionally \texttt{clightgen} does not extract the computation either. We add this small step to allow VST to carry through the proof.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
31

Benoit Viguier's avatar
Benoit Viguier committed
32
  % \item lines 60-62: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
33

Benoit Viguier's avatar
Benoit Viguier committed
34
  % \item lines 70-71: We replace \TNaCle{FOR(a,16) c[a]=i[a];} by \TNaCle{set25519(c,i);}. The semantic of operation done is the same once \TNaCle{set25519} is inlined. This small change is purely cosmetic but stays in the spirit of tweetnacl: keeping a small code size while being auditable.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
35

Benoit Viguier's avatar
Benoit Viguier committed
36
  \item lines 79-82: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.\\
Benoit Viguier's avatar
Benoit Viguier committed
37
  In the function calls of \TNaCle{sel25519}, the specifications requires the use of \TNaCle{int}, the value of \TNaCle{r} being either \TNaCle{0} or \TNaCle{1}, we consider this change safe.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
38

benoit's avatar
benoit committed
39
  \item Lines 90-101: The \TNaCle{for} loop does not add any benefits to the code. By removing it we simplify the source and the verification steps as we do not need to deal with pointer arithmetic. Thus, \TNaCle{x} is limited to only 16 \TNaCle{i64}, \ie \TNaCle{gf}.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
40

Benoit Viguier's avatar
Benoit Viguier committed
41
\end{itemize}