conclusion.tex 2.74 KB
Newer Older
1
\section{Conclusion}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
2
\label{Conclusion}
3

Benoit Viguier's avatar
Benoit Viguier committed
4
5
Any formal system relies on a trusted base. In this section we describe our
chain of trust.
6

Benoit Viguier's avatar
Benoit Viguier committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
\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}

  \item \textbf{Verifiable Software Toolchain}. This framework developped at
  Princeton allows a user to prove that a \texttt{CLight} code matches pure Coq
Benoit Viguier's avatar
Benoit Viguier committed
28
  specification. However one must trust the framework properly captures and
Benoit Viguier's avatar
Benoit Viguier committed
29
30
31
32
  map the CLight behavior to the basic pure Coq functions. At the begining of
  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's avatar
Benoit Viguier committed
33
34
  model captures correctly the C standard.
  \todo{VERIFY THIS, WHICH STANDARD ?}.
Benoit Viguier's avatar
Benoit Viguier committed
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
  Our proof also assumes that the TweetNaCl code will behave as expected if
  compiled under CompCert. We do not provide garantees for other C compilers
  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}.

  While this problem is still present, the Compcert developpers provided us with
  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}
61
62

\subsection{Proof toolchain}