conclusion.tex 7.59 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 \subheading{Trusted Code Base of the proof.} Our proof relies on a trusted base, i.e. a foundation of definitions that must be  Benoit Viguier committed Feb 15, 2020 9 correct. One should not be able to prove a false statement in that system, \eg by  Benoit Viguier committed Sep 02, 2019 10 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 committed Oct 01, 2020 15 16 17 18  used by Coq must be consistent in order to trust the proofs. As an axiom, we assume that the functional extensionality is also consistent with that logic. $$\forall x, f(x) = g(x) \implies f = g$$ \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]  Benoit Viguier committed Jul 10, 2019 19 20 21 22 23 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 committed Oct 01, 2020 25 26  Princeton allows a user to prove that a Clight code matches pure Coq specification.  Benoit Viguier committed Jul 10, 2019 27   Benoit Viguier committed Feb 06, 2020 28  \item \textbf{CompCert}. When compiling with CompCert we only need to trust  benoit committed Oct 01, 2020 29  CompCert's {assembly} semantics, as the compilation chain has been formally proven correct.  Peter Schwabe committed Oct 02, 2020 30 31  However, when compiling with other C compilers like Clang or GCC, the whole code base of these compilers becomes part of the TCB.  Benoit Viguier committed Jul 10, 2019 32   Peter Schwabe committed Oct 02, 2020 33  \item \textbf{\texttt{clightgen}}. The tool translating from {C} to  benoit committed Oct 01, 2020 34  {Clight}, the first step of the CompCert compilation.  Peter Schwabe committed Oct 02, 2020 35 36 37  This compilation step is not covered by the proofs of CompCert and VST requires Clight input. For example, VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}, which \texttt{clightgen} translates to  benoit committed Oct 01, 2020 38  \begin{lstlisting}[language=Ctweetnacl,stepnumber=0,belowskip=-0.5 \baselineskip]  Benoit Viguier committed Feb 06, 2020 39 aux1 = a[i]; aux2 = b[i];  Benoit Viguier committed Jul 10, 2019 40 41 o[i] = aux1 + aux2; \end{lstlisting}  benoit committed Oct 01, 2020 42 43 44 45 46  The \texttt{-normalize} flag is taking care of this rewriting and factors out assignments from inside subexpressions. % The trust of the proof relies on a correct translation from the % initial version of \emph{TweetNaCl} to \emph{TweetNaClVerifiableC}. % The changes required for C code to make it verifiable are now minimal.  Benoit Viguier committed Jul 10, 2019 47   Benoit Viguier committed Jan 16, 2020 48  \item Finally, we must trust the \textbf{Coq kernel} and its  benoit committed Oct 01, 2020 49 50 51  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}.  Benoit Viguier committed Jul 10, 2019 52 \end{itemize}  Peter Schwabe committed Jun 20, 2019 53   Benoit Viguier committed Sep 02, 2019 54 \subheading{Corrections in TweetNaCl.}  Benoit Viguier committed Aug 17, 2019 55 As a result of this verification, we removed superfluous code.  Benoit Viguier committed Sep 02, 2019 56 57 58 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 59   Peter Schwabe committed Oct 02, 2020 60 Wu and Donenfeld brought to our attention that the original  Benoit Viguier committed Oct 01, 2019 61 \TNaCle{car25519} function carried a risk of undefined behavior if \texttt{c}  Benoit Viguier committed Aug 17, 2019 62 is a negative number.  Benoit Viguier committed Feb 06, 2020 63 \begin{lstlisting}[language=Ctweetnacl,stepnumber=0]  Benoit Viguier committed Aug 17, 2019 64 65 66 c=o[i]>>16; o[i]-=c<<16; // c < 0 = UB ! \end{lstlisting}  Peter Schwabe committed Sep 29, 2019 67 68 We replaced this statement with a logical \texttt{and}, proved correctness, and thus solved this problem.  Benoit Viguier committed Feb 06, 2020 69 \begin{lstlisting}[language=Ctweetnacl,stepnumber=0]  Benoit Viguier committed Aug 17, 2019 70 71 o[i]&=0xffff; \end{lstlisting}  Benoit Viguier committed Aug 12, 2019 72   Peter Schwabe committed Feb 15, 2020 73 74 Aside from this modifications, all subsequent alterations to the TweetNaCl code% ---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})---%  Benoit Viguier committed Feb 15, 2020 75 were required for VST to step through the code properly. We believe that those  Benoit Viguier committed Jan 17, 2020 76 77 adjustments do not impact the trust of our proof.  Peter Schwabe committed Feb 15, 2020 78 79 We contacted the authors of TweetNaCl and expect that the changes described above will soon be integrated in a new version of the library.  Benoit Viguier committed Jan 16, 2020 80   Benoit Viguier committed Feb 15, 2020 81 82 83 84 85 86  % Do we want to say that ? % \subheading{Verification Effort.} % In addition to the time required to get familiar with % research software, we faced a few bugs which we reported  Benoit Viguier committed Feb 15, 2020 87 % to the developers of VST to get them fixed.  Benoit Viguier committed Feb 15, 2020 88 89 90 91 92 93 94 % It is very hard to work with a tool without being involved % in the development loop. Additionally newer versions often % broke some of our proofs and it was often needed to adapt % to the changes. % As a result we do not believe the metric person-month to be % a good representation of the verification effort.  benoit committed Oct 01, 2020 95 96 97 98 99 100 101 102 103 104 105 106 107 \subheading{Lessons learned.} The effort to verify an existing code base is significantly harder than synthesizing a proven by construction piece of software. This difficulty is additionally increased by not having the freedom to modify the original code, and by the low-level optimization applied in it. This often requires to write functions that mimic the behavior of the C code before proving multi-level equivalences to reach the desired level of specifications. VST provides on one hand a large set of lemmas, and on the second hand tactics to use them. If a lemma is directly applied, it generates a multiple sub-goals with a large set of dependent existential variables. The tactics provided try to resolve those, and aim to simplify the workload of its user. In an ideal world, the user does not need to know the lemmas applied under the hood and can just rely on those tactics. Unfortunately, there were instances where those were not helping % (\eg applying unnecessary substitutions, unfolding, exploding the size of our current goal; or simply failing),  benoit committed Oct 01, 2020 108 at such moment, making it necessary to look into the VST code base and search for the right lemma.  benoit committed Oct 01, 2020 109 110 111 112  Furthermore, the VST being an academic software, it is very hard to work with a tool without being involved in the development loop. Additionally newer versions often broke some of our proofs and it was often needed to adapt to the changes. That being said,  benoit committed Oct 01, 2020 113 as we reported our bugs and struggles to the development team, since then the toolchain improved a lot.  Peter Schwabe committed Oct 01, 2020 114   Benoit Viguier committed Jan 16, 2020 115 116 117 \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  Benoit Viguier committed Jan 17, 2020 118 assuming the same formulas are used.  Benoit Viguier committed Jan 16, 2020 119 120 121 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 122 With respect to the C code verification (\sref{sec:C-Coq}), the extension of  Peter Schwabe committed Feb 15, 2020 123 the verification effort to Ed25519 would make directly use of the low-level  Benoit Viguier committed Jan 17, 2020 124 arithmetic. The ladder steps formula being different this would require a high  Peter Schwabe committed Oct 02, 2020 125 126 127 level verification similar to \tref{thm:montgomery-ladder-correct}; also, a full correctness verification of Ed25519 signatures would require verifying correctness of SHA-512.  Benoit Viguier committed Jan 17, 2020 128   Benoit Viguier committed Feb 15, 2020 129 The verification of \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would  Peter Schwabe committed Feb 15, 2020 130 require the adaptation of most of the low-level arithmetic (mainly the  Benoit Viguier committed Jan 17, 2020 131 multiplication, carry propagation and reduction).  Benoit Viguier committed Jan 16, 2020 132 Once the correctness and bounds of the basic operations are established,  Benoit Viguier committed Feb 15, 2020 133 reproving the full ladder would make use of our generic definition.  Benoit Viguier committed Aug 12, 2019 134   Benoit Viguier committed Sep 02, 2019 135 \subheading{A complete proof.}  Benoit Viguier committed Sep 21, 2019 136 We provide a mechanized formal proof of the correctness of the X25519  Benoit Viguier committed Feb 06, 2020 137 138 implementation in TweetNaCl from C up the mathematical definitions with a single tool. We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq.  Peter Schwabe committed Feb 15, 2020 139 We then proved that TweetNaCl's implementation of X25519 matches our formalization.  Benoit Viguier committed Sep 02, 2019 140 In a second step we extended the Coq library for elliptic curves \cite{BartziaS14}  Benoit Viguier committed Feb 06, 2020 141 142 143 144 145 146 by Bartzia and Strub to support Montgomery curves. Using this extension we proved that the X25519 from the RFC matches the mathematical definitions as given in~\cite[Sec.~2]{Ber06}. Therefore in addition to proving the mathematical correctness of TweetNaCl, we also increases the trust of other works such as \cite{zinzindohoue2017hacl,Erbsen2016SystematicSO} which rely on RFC~7748.