6-conclusion.tex 5.24 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

7
8
9
10
\subheading{Trusted Code Base of the proof.}
Our proof relies on a trusted base, i.e. a foundation of definitions that must be
correct. One should not be able to prove a false statement in that system, \eg, by
proving an inconsistency.
Benoit Viguier's avatar
Benoit Viguier committed
11
12
13

In our case we rely on:
\begin{itemize}
14
  \item \textbf{Calculus of Inductive Constructions}. The intuitionistic logic
Benoit Viguier's avatar
Benoit Viguier committed
15
  used by Coq must be consistent in order to trust the proofs. As an axiom,
16
  we assume that the functional extensionality is also consistent with that logic.
Benoit Viguier's avatar
Benoit Viguier committed
17
  $$\forall x, f(x) = g(x) \implies f = g$$
18
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Benoit Viguier's avatar
Benoit Viguier committed
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's avatar
Benoit Viguier committed
24
  \item \textbf{Verifiable Software Toolchain}. This framework developed at
Benoit Viguier's avatar
Benoit Viguier committed
25
  Princeton allows a user to prove that a Clight code matches pure Coq
26
  specification.
Benoit Viguier's avatar
Benoit Viguier committed
27

28
29
  \item \textbf{CompCert}. When compiling with CompCert we only need to trust
  CompCert's {assembly} semantics, because it has been formally proven correct.
30
31
  However, when compiling with other C compilers like Clang or GCC, we need to
  trust that the CompCert's Clight semantics matches the C17 standard.
Benoit Viguier's avatar
Benoit Viguier committed
32

Freek Wiedijk's avatar
Freek Wiedijk committed
33
  \item \textbf{\texttt{clightgen}}. The tool making the translation from {C} to
34
35
36
37
38
  {Clight}, the first step of the CompCert compilation.
  The VST does not support the direct verification of \texttt{o[i] = a[i] + b[i]}.
  This needs to be rewritten into:
  \begin{lstlisting}[language=Ctweetnacl,stepnumber=0,belowskip=-0.5 \baselineskip]
aux1 = a[i]; aux2 = b[i];
Benoit Viguier's avatar
Benoit Viguier committed
39
40
o[i] = aux1 + aux2;
\end{lstlisting}
41
42
43
44
45
  The \texttt{-normalize} flag is taking care of this
  rewritting 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's avatar
Benoit Viguier committed
46

47
  \item Finally, we must trust the \textbf{Coq kernel} and its
Benoit Viguier's avatar
Benoit Viguier committed
48
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}.
\end{itemize}
52

53
\subheading{Corrections in TweetNaCl.}
Benoit Viguier's avatar
Benoit Viguier committed
54
As a result of this verification, we removed superfluous code.
55
56
57
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.
58
59

Peter Wu and Jason A. Donenfeld brought to our attention that the original
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
60
\TNaCle{car25519} function carried a risk of undefined behavior if \texttt{c}
61
is a negative number.
62
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0]
63
64
65
c=o[i]>>16;
o[i]-=c<<16; // c < 0 = UB !
\end{lstlisting}
66
67
We replaced this statement with a logical \texttt{and}, proved correctness,
and thus solved this problem.
68
\begin{lstlisting}[language=Ctweetnacl,stepnumber=0]
69
70
o[i]&=0xffff;
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
71

Benoit Viguier's avatar
Benoit Viguier committed
72
Aside from the modifications above mentioned, all subsequent alteration
73
---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})---
74
were required for VST to parse the code properly. We believe those
75
76
77
adjustments do not impact the trust of our proof.

We contacted the authors of TweetNaCl and expect that the changes above
Benoit Viguier's avatar
Benoit Viguier committed
78
mentioned will soon be integrated in a new version of the library.
79
80
81
82

\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's avatar
Benoit Viguier committed
83
assuming the same formulas are used.
84
85
86
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.

87
With respect to the C code verification (\sref{sec:C-Coq}), the extension of
88
the verification effort to Ed25519 would make directly use of the low level
89
90
91
92
93
arithmetic. The ladder steps formula being different this would require a high
level verification similar to \tref{thm:montgomery-ladder-correct}.

The verification \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would
require the adaptation of most of the low level arithmetic (mainly the
Benoit Viguier's avatar
Benoit Viguier committed
94
multiplication, carry propagation and reduction).
95
96
97
Once the correctness and bounds of the basic operations are established,
reproving the full ladder would make use of our generic definition and lower
the workload.
Benoit Viguier's avatar
Benoit Viguier committed
98

99
\subheading{A complete proof.}
Benoit Viguier's avatar
Benoit Viguier committed
100
We provide a mechanized formal proof of the correctness of the X25519
101
102
103
implementation in TweetNaCl from C up the mathematical definitions with a single tool.
We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq.
Then we proved that TweetNaCl's implementation of X25519 matches our formalization.
Benoit Viguier's avatar
typos    
Benoit Viguier committed
104
In a second step we extended the Coq library for elliptic curves \cite{BartziaS14}
105
106
107
108
109
110
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.