6-conclusion.tex 4.98 KB
 Peter Schwabe committed Jun 20, 2019 1 \section{Conclusion}  Benoit Viguier committed Aug 12, 2019 2 \label{sec:Conclusion}  Peter Schwabe committed Jun 20, 2019 3   Benoit Viguier committed Jul 10, 2019 4 5 Any formal system relies on a trusted base. In this section we describe our chain of trust.  Peter Schwabe committed Jun 20, 2019 6   Benoit Viguier committed Sep 02, 2019 7 8 9 10 \subheading{Trusted Code Base of the proof.} Our proof relies on a trusted base, i.e. a foundation of definitions that must be correct. One should not be able to prove a false statement in that system, \eg, by proving an inconsistency.  Benoit Viguier committed Jul 10, 2019 11 12 13  In our case we rely on: \begin{itemize}  Benoit Viguier committed Sep 27, 2019 14  \item \textbf{Calculus of Inductive Constructions}. The intuitionistic logic  Benoit Viguier committed Jul 10, 2019 15  used by Coq must be consistent in order to trust the proofs. As an axiom,  Peter Schwabe committed Sep 29, 2019 16  we assume that the functional extensionality is also consistent with that logic.  Benoit Viguier committed Aug 16, 2019 17  $$\forall x, f(x) = g(x) \implies f = g$$  Benoit Viguier committed Jul 10, 2019 18 19 20 21 22 23 \begin{lstlisting}[language=Coq] Lemma f_ext: forall (A B:Type), forall (f g: A -> B), (forall x, f(x) = g(x)) -> f = g. \end{lstlisting}  Benoit Viguier committed Aug 01, 2019 24  \item \textbf{Verifiable Software Toolchain}. This framework developed at  Benoit Viguier committed Aug 21, 2019 25  Princeton allows a user to prove that a Clight code matches pure Coq  Benoit Viguier committed Sep 02, 2019 26  specification.  Benoit Viguier committed Jul 10, 2019 27   Freek Wiedijk committed Oct 01, 2019 28  \item \textbf{CompCert}.  Benoit Viguier committed Jan 16, 2020 29 30 31 32  When compiling with CompCert we only need to trust CompCert's {assembly} semantics, because it has been formally proven correct. However, when compiling with other C compilers like Clang or GCC, we need to trust that the CompCert's Clight semantics matches the C17 standard.  Benoit Viguier committed Jul 10, 2019 33   Freek Wiedijk committed Oct 01, 2019 34 35  \item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to {Clight}. It is the first step of the compilation.  Benoit Viguier committed Jul 10, 2019 36 37 38 39 40 41 42  VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}. This required us to rewrite the lines into: \begin{lstlisting}[language=C] aux1 = a[i]; aux2 = b[i]; o[i] = aux1 + aux2; \end{lstlisting}  Peter Schwabe committed Sep 29, 2019 43  The trust of the proof relies on the trust of a correct translation from the  Benoit Viguier committed Sep 02, 2019 44 45  initial version of \emph{TweetNaCl} to \emph{TweetNaclVerifiableC}. \texttt{clightgen} comes with \texttt{-normalize} flag which  Benoit Viguier committed Aug 17, 2019 46  factors out function calls and assignments from inside subexpressions.  Peter Schwabe committed Sep 29, 2019 47  The changes required for C code to make it verifiable are now minimal.  Benoit Viguier committed Jul 10, 2019 48   Benoit Viguier committed Jan 16, 2020 49  \item Finally, we must trust the \textbf{Coq kernel} and its  Benoit Viguier committed Jul 10, 2019 50 51 52 53  associated libraries; the \textbf{Ocaml compiler} on which we compiled Coq; the \textbf{Ocaml Runtime} and the \textbf{CPU}. Those are common to all proofs done with this architecture \cite{2015-Appel,coq-faq}. \end{itemize}  Peter Schwabe committed Jun 20, 2019 54   Benoit Viguier committed Jan 16, 2020 55 56 \todo{NEW}  Benoit Viguier committed Sep 02, 2019 57 \subheading{Corrections in TweetNaCl.}  Benoit Viguier committed Aug 17, 2019 58 As a result of this verification, we removed superfluous code.  Benoit Viguier committed Sep 02, 2019 59 60 61 Indeed indexes 17 to 79 of the \TNaCle{i64 x[80]} intermediate variable of \TNaCle{crypto_scalarmult} were adding unnecessary complexity to the code, we removed them.  Benoit Viguier committed Aug 17, 2019 62 63  Peter Wu and Jason A. Donenfeld brought to our attention that the original  Benoit Viguier committed Oct 01, 2019 64 \TNaCle{car25519} function carried a risk of undefined behavior if \texttt{c}  Benoit Viguier committed Aug 17, 2019 65 66 67 68 69 is a negative number. \begin{lstlisting}[language=Ctweetnacl] c=o[i]>>16; o[i]-=c<<16; // c < 0 = UB ! \end{lstlisting}  Peter Schwabe committed Sep 29, 2019 70 71 We replaced this statement with a logical \texttt{and}, proved correctness, and thus solved this problem.  Benoit Viguier committed Aug 17, 2019 72 73 74 \begin{lstlisting}[language=Ctweetnacl] o[i]&=0xffff; \end{lstlisting}  Benoit Viguier committed Aug 12, 2019 75   Benoit Viguier committed Jan 17, 2020 76 \todo{NEW}  Benoit Viguier committed Jan 16, 2020 77   Benoit Viguier committed Jan 17, 2020 78 79 80 81 82 83 Aside from the modications above mentionned, all subsequent alteration ---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})--- were required for VST to parse properly the code. We believe those adjustments do not impact the trust of our proof. We contacted the authors of TweetNaCl and expect that the changes above  Benoit Viguier committed Jan 16, 2020 84 85 86 87 88 89 90 91 92 mentionned will soon be integrated in a new version of the library. \subheading{Extending our work.} The high-level definition (\sref{sec:maths}) can easily be ported to any other Montgomery curves and with it the proof of the ladder's correctness assuming the same forumlas are used. In addition to the curve equation, the field \F{p} would need to be redefined as $p=2^{255}-19$ is hard-coded in order to speed up some proofs.  Benoit Viguier committed Jan 17, 2020 93 94 95 96 97 98 99 100 With respect to the C code verification (\sref{sec:C-Coq}), the extension of the verification effort to Ed25519 would makes directly use of the low level arithmetic. The ladder steps formula being different this would require a high level verification similar to \tref{thm:montgomery-ladder-correct}. The verification \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would require the adaptation of most of the low level arithmetic (mainly the multiplication, carry propagations and reductions).  Benoit Viguier committed Jan 16, 2020 101 102 103 Once the correctness and bounds of the basic operations are established, reproving the full ladder would make use of our generic definition and lower the workload.  Benoit Viguier committed Aug 12, 2019 104   Benoit Viguier committed Sep 02, 2019 105 \subheading{A complete proof.}  Benoit Viguier committed Sep 21, 2019 106 107 108 109 We provide a mechanized formal proof of the correctness of the X25519 implementation in TweetNaCl. We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq. Then we proved that TweetNaCl's implementation of X25519 matches our formalization.  Benoit Viguier committed Sep 02, 2019 110 In a second step we extended the Coq library for elliptic curves \cite{BartziaS14}  Benoit Viguier committed Sep 02, 2019 111 by Bartzia and Strub to support Montgomery curves. Using this extension we  Benoit Viguier committed Sep 27, 2019 112 proved that the X25519 from the RFC and therefore its implementation in TweetNaCl matches  Benoit Viguier committed Sep 21, 2019 113 the mathematical definitions as given in~\cite[Sec.~2]{Ber06}.