conclusion.tex 2.98 KB
Newer Older
1
\section{Conclusion}
Benoit Viguier's avatar
Benoit Viguier committed
2
\label{sec: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
\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's avatar
Benoit Viguier committed
26
  \item \textbf{Verifiable Software Toolchain}. This framework developed at
Benoit Viguier's avatar
Benoit Viguier committed
27
  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
  map the CLight behavior to the basic pure Coq functions. At the beginning of
Benoit Viguier's avatar
Benoit Viguier committed
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'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
  Our proof also assumes that the TweetNaCl code will behave as expected if
Benoit Viguier's avatar
Benoit Viguier committed
36
  compiled under CompCert. We do not provide guarantees for other C compilers
Benoit Viguier's avatar
Benoit Viguier committed
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's avatar
Benoit Viguier committed
51
  While this problem is still present, the CompCert developers provided us with
Benoit Viguier's avatar
Benoit Viguier committed
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}
61

Benoit Viguier's avatar
Benoit Viguier committed
62
63
64
65
66
67
68
\subsection{Modifications in TweetNaCl}

The upper 64 indexes of the \TNaCle{i64 x[80]} intermediate variable of
\TNaCle{crypto_scalarmult} were adding unnecessary complexity to the code,
we fixed it.

\todo{Mention Peter Wu and Jason A. Donenfeld change to car25519}