conclusion.tex 3.45 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
\subsection{Trusted Core Base of the proof}

Benoit Viguier's avatar
Benoit Viguier committed
9
Our proof relies on a trusted base, i.e. a foundation of specifications
Benoit Viguier's avatar
Benoit Viguier committed
10
11
12
13
14
15
16
17
18
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.
Benoit Viguier's avatar
Benoit Viguier committed
19
  $$\forall x, f(x) = g(x) \implies f = g$$
Benoit Viguier's avatar
Benoit Viguier committed
20
21
22
23
24
25
\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
29
30
  map the CLight behavior to the basic pure Coq functions.
  % At the beginning of the project we found inconsistency and reported them to the authors.
Benoit Viguier's avatar
Benoit Viguier committed
31
32

  \item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
33
  model captures correctly the C99 standard.
Benoit Viguier's avatar
Benoit Viguier committed
34
  Our proof also assumes that the TweetNaCl code will behave as expected if
Benoit Viguier's avatar
Benoit Viguier committed
35
  compiled under CompCert. We do not provide guarantees for other C compilers
Benoit Viguier's avatar
Benoit Viguier committed
36
37
38
39
40
41
42
43
44
45
46
47
48
  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}.
49
50
  \texttt{clightgen} now comes with \texttt{-normalize} flag which
  factors out function calls and assignments from inside subexpressions.
Benoit Viguier's avatar
Benoit Viguier committed
51
52
53
54
55
56
57
  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}
58

59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
\subsection{Corrections in TweetNaCl}

As a result of this verification, we removed superflous code.
Indeed 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.

Peter Wu and Jason A. Donenfeld brought to our attention that the original
\TNaCle{car25519} function presented risk of Undefined Behavior if \texttt{c}
is a negative number.
\begin{lstlisting}[language=Ctweetnacl]
c=o[i]>>16;
o[i]-=c<<16; // c < 0 = UB !
\end{lstlisting}
By replacing statement by a logical \texttt{and} (and proving the correctness)
we solved this problem.
\begin{lstlisting}[language=Ctweetnacl]
o[i]&=0xffff;
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
77

78
79
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's avatar
Benoit Viguier committed
80

81
\todo{I don't see what to say more here.}