conclusion.tex 2.74 KB
 Peter Schwabe committed Jun 20, 2019 1 \section{Conclusion}  Benoit Viguier committed Jul 03, 2019 2 \label{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 Jul 10, 2019 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 \subsection{Trusted Core Base of the proof} Our proof relies on a trusted base , i.e. a foundation of specifications and implementations that must stay correct with respect to their specifications. One should not be able to prove a false statement in that system e.g. by proving an inconsistency. In our case we rely on: \begin{itemize} \item \textbf{Calculus of Inductive Construction}. The intuitionistic logic used by Coq must be consistent in order to trust the proofs. As an axiom, we assumed that the functional extensionality, which is also consistent with that logic. $$\forall x, f(x) = g(x) ) \implies f = g$$ \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 26  \item \textbf{Verifiable Software Toolchain}. This framework developed at  Benoit Viguier committed Jul 10, 2019 27  Princeton allows a user to prove that a \texttt{CLight} code matches pure Coq  Benoit Viguier committed Jul 22, 2019 28  specification. However one must trust the framework properly captures and  Benoit Viguier committed Aug 01, 2019 29  map the CLight behavior to the basic pure Coq functions. At the beginning of  Benoit Viguier committed Jul 10, 2019 30 31 32  the project we found inconsistency and reported them to the authors. \item \textbf{CompCert}. The formally proven compiler. We trust that the Clight  Benoit Viguier committed Jul 16, 2019 33 34  model captures correctly the C standard. \todo{VERIFY THIS, WHICH STANDARD ?}.  Benoit Viguier committed Jul 10, 2019 35  Our proof also assumes that the TweetNaCl code will behave as expected if  Benoit Viguier committed Aug 01, 2019 36  compiled under CompCert. We do not provide guarantees for other C compilers  Benoit Viguier committed Jul 10, 2019 37 38 39 40 41 42 43 44 45 46 47 48 49 50  such as Clang or GCC. \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} The trust of the proof relied on the trust of a correct translation from the initial version of \textit{TweetNaCl} to \textit{TweetNaclVerificable}.  Benoit Viguier committed Aug 01, 2019 51  While this problem is still present, the CompCert developers provided us with  Benoit Viguier committed Jul 10, 2019 52 53 54 55 56 57 58 59 60  the \texttt{-normalize} option for \texttt{clightgen} which takes care of generating auxiliary variables in order to automatically derive these steps. The changes required for a C-code to make it Verifiable are now minimal. \item Last but not the least, we must trust: the \textbf{Coq kernel} and its 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 61 62  \subsection{Proof toolchain}