conclusion.tex 7.4 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
\subheading{Trusted Code Base of the proof.}
Our proof relies on a trusted base, i.e. a foundation of definitions that must be
Benoit Viguier's avatar
Benoit Viguier committed
9
correct. One should not be able to prove a false statement in that system, \eg by
10
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's avatar
benoit committed
15
16
17
18
        used by Coq must be consistent in order to trust the proofs. As an axiom,
        we assume that the functional extensionality is also consistent with that logic.
        $$\forall x, f(x) = g(x) \implies f = g$$
        \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's avatar
benoit committed
25
26
        Princeton allows a user to prove that a Clight code matches pure Coq
        specification.
Benoit Viguier's avatar
Benoit Viguier committed
27

28
  \item \textbf{CompCert}. When compiling with CompCert we only need to trust
benoit's avatar
benoit committed
29
30
31
        CompCert's {assembly} semantics, as the compilation chain has been formally proven correct.
        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
benoit's avatar
benoit committed
34
35
36
37
          {Clight}, the first step of the CompCert compilation.
        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]
38
aux1 = a[i]; aux2 = b[i];
Benoit Viguier's avatar
Benoit Viguier committed
39
40
o[i] = aux1 + aux2;
\end{lstlisting}
benoit's avatar
benoit committed
41
42
43
44
45
        The \texttt{-normalize} flag is taking care of this
        rewriting 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's avatar
benoit committed
48
49
50
        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}.
Benoit Viguier's avatar
Benoit Viguier committed
51
\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

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

77
78
We contacted the authors of TweetNaCl and expect that the changes described
above will soon be integrated in a new version of the library.
79

80
81
82
83
84
85

% Do we want to say that ?

% \subheading{Verification Effort.}
% In addition to the time required to get familiar with
% research software, we faced a few bugs which we reported
Benoit Viguier's avatar
Benoit Viguier committed
86
% to the developers of VST to get them fixed.
87
88
89
90
91
92
93
% It is very hard to work with a tool without being involved
% in the development loop. Additionally newer versions often
% broke some of our proofs and it was often needed to adapt
% to the changes.
% As a result we do not believe the metric person-month to be
% a good representation of the verification effort.

benoit's avatar
benoit committed
94
95
96
97
98
99
100
101
102
103
104
105
106
\subheading{Lessons learned.} The effort to verify an existing code base is
significantly harder than synthesizing a proven by construction piece of software.
This difficulty is additionally increased by not having the freedom to modify
the original code, and by the low-level optimization applied in it.
This often requires to write functions that mimic the behavior of the C
code before proving multi-level equivalences to reach the desired level of specifications.

VST provides on one hand a large set of lemmas, and on the second hand tactics to use them.
If a lemma is directly applied, it generates a multiple sub-goals with a large set of dependent existential variables.
The tactics provided try to resolve those, and aim to simplify the workload of its user.
In an ideal world, the user does not need to know the lemmas applied under the hood and can just rely on those tactics.
Unfortunately, there were instances where those were not helping
%  (\eg applying unnecessary substitutions, unfolding, exploding the size of our current goal; or simply failing),
benoit's avatar
flow    
benoit committed
107
at such moment, making it necessary to look into the VST code base and search for the right lemma.
benoit's avatar
benoit committed
108
109
110
111

Furthermore, the VST being an academic software, it is very hard to work with a tool
without being involved in the development loop. Additionally newer versions often broke
some of our proofs and it was often needed to adapt to the changes. That being said,
benoit's avatar
benoit committed
112
as we reported our bugs and struggles to the development team, since then the toolchain improved a lot.
113

114
115
116
\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
117
assuming the same formulas are used.
118
119
120
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.

121
With respect to the C code verification (\sref{sec:C-Coq}), the extension of
122
the verification effort to Ed25519 would make directly use of the low-level
123
124
125
arithmetic. The ladder steps formula being different this would require a high
level verification similar to \tref{thm:montgomery-ladder-correct}.

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

132
\subheading{A complete proof.}
Benoit Viguier's avatar
Benoit Viguier committed
133
We provide a mechanized formal proof of the correctness of the X25519
134
135
implementation in TweetNaCl from C up the mathematical definitions with a single tool.
We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq.
136
We then proved that TweetNaCl's implementation of X25519 matches our formalization.
Benoit Viguier's avatar
typos    
Benoit Viguier committed
137
In a second step we extended the Coq library for elliptic curves \cite{BartziaS14}
138
139
140
141
142
143
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.