6_conclusion.tex 3.7 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 28 \item \textbf{CompCert}. The formally proven compiler. We trust that the Clight Benoit Viguier committed Sep 02, 2019 29 model captures correctly the C17 standard. Benoit Viguier committed Jul 10, 2019 30 Our proof also assumes that the TweetNaCl code will behave as expected if Benoit Viguier committed Sep 02, 2019 31 32 compiled under CompCert. % We do not provide guarantees for other C compilers such as Clang or GCC. Benoit Viguier committed Jul 10, 2019 33 34 35 36 37 38 39 40 41 42 \item \textbf{\texttt{clightgen}}. The tool making the translation from \textbf{C} to \textbf{Clight}. It is the first step of the compilation. 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 Peter Schwabe committed Sep 29, 2019 49 \item Last but not the least, 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 Sep 02, 2019 55 \subheading{Corrections in TweetNaCl.} Benoit Viguier committed Aug 17, 2019 56 As a result of this verification, we removed superfluous code. Benoit Viguier committed Sep 02, 2019 57 58 59 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 60 61 Peter Wu and Jason A. Donenfeld brought to our attention that the original Benoit Viguier committed Oct 01, 2019 62 \TNaCle{car25519} function carried a risk of undefined behavior if \texttt{c} Benoit Viguier committed Aug 17, 2019 63 64 65 66 67 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 68 69 We replaced this statement with a logical \texttt{and}, proved correctness, and thus solved this problem. Benoit Viguier committed Aug 17, 2019 70 71 72 \begin{lstlisting}[language=Ctweetnacl] o[i]&=0xffff; \end{lstlisting} Benoit Viguier committed Aug 12, 2019 73 Benoit Viguier committed Aug 17, 2019 74 75 We believe that the type change of the loop index (\TNaCle{int} instead of \TNaCle{i64}) does not impact the trust of our proof. Benoit Viguier committed Aug 12, 2019 76 Benoit Viguier committed Sep 02, 2019 77 \subheading{A complete proof.} Benoit Viguier committed Sep 21, 2019 78 79 80 81 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 82 In a second step we extended the Coq library for elliptic curves \cite{BartziaS14} Benoit Viguier committed Sep 02, 2019 83 by Bartzia and Strub to support Montgomery curves. Using this extension we Benoit Viguier committed Sep 27, 2019 84 proved that the X25519 from the RFC and therefore its implementation in TweetNaCl matches Benoit Viguier committed Sep 21, 2019 85 the mathematical definitions as given in~\cite[Sec.~2]{Ber06}.