code-tweetnacl.tex 2.64 KB
 Benoit Viguier committed Jan 14, 2020 1 \section{The complete X25519 code from TweetNaCl}  Benoit Viguier committed Aug 06, 2019 2 \label{verified-C-and-diff}  Peter Schwabe committed Jun 20, 2019 3   Benoit Viguier committed Jun 21, 2019 4 5 \subheading{Verified C Code} We provide below the code we verified.  Benoit Viguier committed Jan 15, 2020 6 \lstinputlisting[linerange={2-5,8-9,266-317,333-380,393-438},language=Ctweetnacl]{../proofs/vst/c/tweetnaclVerifiableC.c}  benoit committed Jan 19, 2021 7 ~  Benoit Viguier committed Jun 21, 2019 8   Benoit Viguier committed Aug 01, 2019 9 \subheading{Diff from TweetNaCl} We provide below the diff between the original code of TweetNaCl and the code we verified.  Benoit Viguier committed Jun 21, 2019 10 11  \lstinputlisting[language=diff]{tweetnacl.diff}  Benoit Viguier committed Feb 04, 2020 12   Peter Schwabe committed Feb 09, 2021 13 In the following, we provide the explanations of the above changes to TweetNaCl's code.  Benoit Viguier committed Feb 04, 2020 14 15  \begin{itemize}  Benoit Viguier committed Feb 15, 2020 16  \item lines 7-8: We tell VST that \TNaCle{long long} are  Benoit Viguier committed Feb 04, 2020 17  aligned on 8 bytes.  Benoit Viguier committed Feb 04, 2020 18   Benoit Viguier committed Feb 15, 2020 19  \item lines 16-23: We remove the the undefined behavior as explained in \sref{sec:Conclusion}.  Benoit Viguier committed Feb 04, 2020 20   Benoit Viguier committed Feb 15, 2020 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 committed Feb 04, 2020 22   Benoit Viguier committed Feb 15, 2020 23  \item lines 39 \& 41: We initialize \TNaCle{m} with \TNaCle{0}.  Benoit Viguier committed Feb 04, 2020 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 committed Feb 04, 2020 27   Benoit Viguier committed Feb 15, 2020 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 committed Feb 04, 2020 29   Benoit Viguier committed Feb 15, 2020 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 committed Feb 04, 2020 31   Benoit Viguier committed Feb 15, 2020 32  % \item lines 60-62: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.  Benoit Viguier committed Feb 04, 2020 33   Benoit Viguier committed Feb 15, 2020 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 committed Feb 04, 2020 35   Benoit Viguier committed Feb 15, 2020 36  \item lines 79-82: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.\\  Benoit Viguier committed Feb 04, 2020 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 committed Feb 04, 2020 38   benoit committed Jan 19, 2021 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 committed Feb 04, 2020 40   Benoit Viguier committed Feb 04, 2020 41 \end{itemize}