intro.tex 11.3 KB
Newer Older
1
2
\section{Introduction}
\label{sec:intro}
3

Benoit Viguier's avatar
Benoit Viguier committed
4
5
The Networking and Cryptography library (NaCl)~\cite{BLS12}
is an easy-to-use, high-security, high-speed cryptography library.
Benoit Viguier's avatar
Benoit Viguier committed
6
It uses specialized code for different platforms, which makes it rather complex and hard to audit.
Benoit Viguier's avatar
Benoit Viguier committed
7
8
TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C
of the core functionalities of NaCl and is claimed to be
9
\emph{``the first cryptographic library that allows correct functionality
benoit's avatar
benoit committed
10
  to be verified by auditors with reasonable effort''}~\cite{BGJ+15}.
11
The original paper presenting TweetNaCl describes some effort to support
Peter Schwabe's avatar
Peter Schwabe committed
12
13
this claim, for example, formal verification of memory safety, but does not actually
prove correctness of any of the primitives implemented by the library.
14

Benoit Viguier's avatar
Benoit Viguier committed
15
One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519 presented
16
by Bernstein in~\cite{Ber06}.
17
This protocol is standardized in RFC~7748 and used by a wide variety of applications~\cite{things-that-use-curve25519}
18
such as SSH, the Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over
19
an insecure channel.
20
21
The X25519 key-exchange protocol is an \xcoord-only
elliptic-curve Diffie--Hellman key exchange using the Montgomery
Benoit Viguier's avatar
Benoit Viguier committed
22
curve $E: y^2 = x^3 + 486662 x^2 + x$ over the field $\F{\p}$.
23
Note that originally, the name ``Curve25519'' referred to the key-exchange protocol,
Peter Schwabe's avatar
Peter Schwabe committed
24
25
but Bernstein suggested to rename the protocol to X25519 and to use the name
Curve25519 for the underlying elliptic curve~\cite{Ber14}.
26
We use this updated terminology in this paper.
27

28
\subheading{Contributions of this paper.}
29
30
31
In short, in this paper we provide a computer-verified proof that the
X25519 implementation in TweetNaCl matches the mathematical definition
of the function given in~\cite[Sec.~2]{Ber06}.
Benoit Viguier's avatar
Benoit Viguier committed
32
This proof is done in three steps:
33
34

We first formalize RFC~7748~\cite{rfc7748} in Coq~\cite{coq-faq}.
Benoit Viguier's avatar
Benoit Viguier committed
35

36
In the second step we prove equivalence of the C implementation of X25519
Benoit Viguier's avatar
Benoit Viguier committed
37
to our RFC formalization.
Peter Schwabe's avatar
Peter Schwabe committed
38
This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}
Benoit Viguier's avatar
Benoit Viguier committed
39
to establish a link between C and Coq.
40
VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
benoit's avatar
benoit committed
41
to show that the semantics of the program satisfies a functional specification in Coq.
Benoit Viguier's avatar
Benoit Viguier committed
42
To the best of our knowledge, this is the first time that VST
43
is used in the formal proof of correctness of an implementation
Peter Schwabe's avatar
Peter Schwabe committed
44
45
of an asymmetric cryptographic primitive.

46
In the last step we prove that the Coq formalization of the RFC matches
Peter Schwabe's avatar
Peter Schwabe committed
47
the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.
48
We do this by extending the Coq library
Benoit Viguier's avatar
Benoit Viguier committed
49
for elliptic curves~\cite{BartziaS14} by Bartzia and Strub to
50
support Montgomery curves, and in particular Curve25519.
51

52
53
54
To our knowledge, this verification effort is the first to not just
connect a low-level implementation to a higher-level implementation (or ``specification''),
but to prove correctness all the way up
55
to the mathematical definition in terms of scalar multiplication on an elliptic curve.
56
57
58
59
As a consequence, the result of this paper can readily be used in mechanized proofs
arguing about the security of cryptographic constructions on the more abstract
level of operations in groups and related problems, like the elliptic-curve
discrete-logarithm (ECDLP) or elliptic-curve Diffie-Hellman (ECDH) problem.
60
61
Also, connecting our formalization of the RFC to the mathematical definition
significantly increases trust into the correctness of the formalization and
Peter Schwabe's avatar
Peter Schwabe committed
62
reduces the effort of manually auditing the formalization.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
63

64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
\subheading{The bigger picture of high-assurance crypto.}
This work fits into the bigger area of \emph{high-assurance} cryptography,
i.e., a line of work that applies techniques and tools from formal methods 
to obtain computer-verified guarantees for cryptographic software. 
Traditionally, high-assurance cryptography is concerned with three main properties
of cryptographic software:
\begin{enumerate}
  \item verifying \textbf{correctness} of cryptographic software, 
    typically against a high-level specification;\label{hacs:correct}
  \item verifying \textbf{implementation security} and in particular
    security against timing attacks; and\label{hacs:sca}
  \item verifying \textbf{cryptographic security} notions of primitives and protocols 
    through computer-checked reductions from some assumed-to-be-hard mathematical problem.\label{hacs:secure}
\end{enumerate}
A recent addition to this triplet (or rather an extension of implementation security)
Peter Schwabe's avatar
Peter Schwabe committed
79
80
is security also against attacks expoiting speculative execution;
see, e.g.,~\cite{DBLP:conf/pldi/CauligiDGTSRB20}.
81
82
83
84
85
86
87
This paper targets only the first point and attempts to make results
immediately usable for verification efforts of cryptographic security.

Verification of implementation security is probably equally important as
verification of correctness, but working on the C language level as we do
in this paper is not helpful. To obtain guarantees of security against 
timing-attack we recommend verifying \emph{compiled} code on LLVM level with, 
Peter Schwabe's avatar
Peter Schwabe committed
88
89
e.g., ct-verif~\cite{ABB+16}, 
or even better on binary level with, e.g., \textsc{Binsec/Rel}~\cite{DBR20}.
90

Peter Schwabe's avatar
Peter Schwabe committed
91
\subheading{Related work.}
92
93
94
95
96
The field of computer-aided cryptography, i.e., using computer-verified proofs
to strengthen our trust into cryptographic constructions and cryptographic software,
has seen massive progress in the recent past. This progress, the state of the art,
and future challenges have recently been compiled in a SoK paper by Barbosa,
Barthe, Bhargavan, Blanchet, Cremers, Liao, and Parno~\cite{BBB+19}.
Benoit Viguier's avatar
Benoit Viguier committed
97
This SoK paper, in Section III.C, also gives an overview of verification efforts of
98
99
100
101
102
X25519 software. What all the previous approaches have in common is that they
prove correctness by verifying that some low-level implementation matches a
higher-level specification. This specification is kept in terms of a sequence
of finite-field operations, typically close to the pseudocode in RFC 7748.

Benoit Viguier's avatar
Benoit Viguier committed
103
There are two general approaches to establish this link
104
105
106
107
108
between low-level code and higher-level specification:
Synthesize low-level code from the specification
or write the low-level code by hand and prove that it
matches the specification.

Peter Schwabe's avatar
Peter Schwabe committed
109
The X25519 implementation from the Evercrypt project~\cite{EverCrypt}
Peter Schwabe's avatar
Peter Schwabe committed
110
111
uses a low-level language called Vale that translates
directly to assembly and proves equivalence to a high-level specification in F$^*$.
Benoit Viguier's avatar
fixes    
Benoit Viguier committed
112
In~\cite{Zinzindohoue2016AVE}, Zinzindohou{\'{e}}, Bartzia, and Bhargavan
Peter Schwabe's avatar
Peter Schwabe committed
113
114
115
describe a verified extensible library of elliptic curves~ in F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}.
This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl}
used in the NSS suite from Mozilla. The approach they use is a combination
116
of proving and synthesizing: A fairly low-level implementation written in
Peter Schwabe's avatar
Peter Schwabe committed
117
118
119
120
121
122
123
124
125
Low$^*$ is proven to be equivalent to a high-level specification in F$^*$.
The Low$^*$ code is then compiled to C using an unverified and thus trusted
compiler called Kremlin.

Coq not only allows verification but also synthesis~\cite{CpdtJFR}.
Erbsen, Philipoom, Gross, and Chlipala make use of it to have
correct-by-construction finite-field arithmetic, which is used
to synthesize certified elliptic-curve crypto software~\cite{Philipoom2018CorrectbyconstructionFF,Erbsen2017CraftingCE,Erbsen2016SystematicSO}.
This software suite is now being used in BoringSSL~\cite{fiat-crypto}.
126

Peter Schwabe's avatar
Peter Schwabe committed
127
All of these X25519 verification efforts use a clean-slate approach to obtain code and proofs.
Peter Schwabe's avatar
Peter Schwabe committed
128
Our effort targets existing software; we are aware of only one earlier work verifying existing X25519 software:
129
130
In~\cite{Chen2014VerifyingCS}, Chen, Hsu, Lin, Schwabe, Tsai, Wang, Yang, and Yang present
a mechanized proof of two assembly-level implementations of the core function of X25519.
Peter Schwabe's avatar
Peter Schwabe committed
131
132
Their proof takes a different approach from ours.
It uses heavy annotation of the assembly-level code in order to ``guide'' a SAT solver;
Peter Schwabe's avatar
Peter Schwabe committed
133
134
also, it does not cover the full X25519 functionality and does
not make the link to the mathematical definition from~\cite{Ber06}.
135
136
137
138
As a consequence, this work would not find bugs in any of the routines
processing the scalar (like ``clamping'', see Section~\ref{subsec:X25519-key-exchange}),
bugs in the the serialization routines or, maybe most importantly,
bugs in the high-level specification that the code is verified against.
139
140
141

Finally, in terms of languages and tooling the work closest to what we present here
is the proof of correctness of OpenSSL's
Benoit Viguier's avatar
Benoit Viguier committed
142
143
implementations of HMAC~\cite{Beringer2015VerifiedCA},
and mbedTLS' implementations of
144
HMAC-DRBG~\cite{2017-Ye} and SHA-256~\cite{2015-Appel}.
Peter Schwabe's avatar
Peter Schwabe committed
145
146
As those are all symmetric primitives without the rich mathematical
structure of finite field and elliptic curves the actual proofs are quite different.
Benoit Viguier's avatar
Benoit Viguier committed
147

148
\subheading{Reproducing the proofs.}
Benoit Viguier's avatar
fixes    
Benoit Viguier committed
149
150
To maximize reusability of our results we place the code of our formal proof
presented in this paper into the public domain.
151
It is available at \url{https://doi.org/10.5281/zenodo.4439686}
Benoit Viguier's avatar
Benoit Viguier committed
152
with instructions of how to compile and verify our proof.
153
A description of the content of the code archive is provided in
Benoit Viguier's avatar
Benoit Viguier committed
154
Appendix~\ref{appendix:proof-folders}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
155

156
\subheading{Organization of this paper.}
Peter Schwabe's avatar
Peter Schwabe committed
157
\sref{sec:preliminaries} gives the necessary background on Curve25519 and X25519
158
implementations and a brief explanation of how formal verification works.
Peter Schwabe's avatar
Peter Schwabe committed
159
\sref{sec:Coq-RFC} provides our Coq formalization of X25519 as specified in RFC~7748~\cite{rfc7748}.
160
\sref{sec:C-Coq} details the specifications of X25519 in TweetNaCl and some of the
Peter Schwabe's avatar
Peter Schwabe committed
161
proof techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}.
Benoit Viguier's avatar
Benoit Viguier committed
162
\sref{sec:maths} describes our extension of the formal library by Bartzia
163
and Strub and the proof of correctness of the X25519 implementation with respect to Bernstein's
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
164
specifications~\cite{Ber14}.
165
Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs
Benoit Viguier's avatar
Benoit Viguier committed
166
and conclude with some lessons learned about TweetNaCl and with sketching the
167
effort required to extend our work to other elliptic-curve software.
Benoit Viguier's avatar
Benoit Viguier committed
168

Benoit Viguier's avatar
Benoit Viguier committed
169
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
Benoit Viguier's avatar
Benoit Viguier committed
170
C source files are represented by {\color{doc@lstfunctions}.C} while
benoit's avatar
benoit committed
171
  {\color{doc@lstfunctions}.V} corresponds to Coq files.
172
In a nutshell, we formalize X25519 into a Coq function \texttt{RFC},
173
174
and we write a specification in separation logic with VST.
The first step of CompCert compilation (clightgen) is used to translate
175
the C source code into a DSL in Coq (CLight). By using VST,
176
177
we step through the translated instructions and verify that the program satisfies the specifications.
Additionally we formally define the scalar multiplication over elliptic curves and show that,
178
under the same preconditions as used in the specification, \texttt{RFC} computes the desired results.
Benoit Viguier's avatar
Benoit Viguier committed
179
180
181
182

\begin{figure}[h]
  \centering
  \include{tikz/proof}
183
%  \vspace{-0.5cm}
Benoit Viguier's avatar
Benoit Viguier committed
184
  \caption{Structure of the proof.}
Benoit Viguier's avatar
Benoit Viguier committed
185
186
  \label{tikz:ProofOverview}
\end{figure}
Benoit Viguier's avatar
done    
Benoit Viguier committed
187

Benoit Viguier's avatar
forward    
Benoit Viguier committed
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
% \url{https://www.imperialviolet.org/2014/09/07/provers.html}

% \section{Related Works}
%
% \begin{itemize}
%   \item HACL*
%   \item Proving SHA-256 and HMAC
%   \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs17.pdf}
%   \item \url{http://www.iis.sinica.edu.tw/~bywang/papers/ccs14.pdf}
%   \item \url{https://cryptojedi.org/crypto/#gfverif}
%   \item \url{https://cryptojedi.org/crypto/#verify25519}
%   \item Fiat Crypto : synthesis
% \end{itemize}
%
% Add comparison with Fiat-crypto