1-intro.tex 7.5 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
10
11
\emph{``the first cryptographic library that allows correct functionality
to be verified by auditors with reasonable effort''}~\cite{BGJ+15}.
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
Peter Schwabe's avatar
Peter Schwabe committed
16
by Bernstein in~\cite{rfc7748}.
17
This protocol is standardized in RFC~7748 and used by a wide variety of applications~\cite{things-that-use-curve25519}
Peter Schwabe's avatar
Peter Schwabe committed
18
such as SSH, 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{Contribution of this paper.}
Peter Schwabe's avatar
Peter Schwabe committed
29
We provide a mechanized formal proof of the correctness of the X25519
Benoit Viguier's avatar
Benoit Viguier committed
30
implementation in TweetNaCl.
Benoit Viguier's avatar
Benoit Viguier committed
31
This proof is done in three steps:
32
33

We first formalize RFC~7748~\cite{rfc7748} in Coq~\cite{coq-faq}.
Benoit Viguier's avatar
Benoit Viguier committed
34
35
% This part uses generic techniques to facilitate later proofs.

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
The VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
Peter Schwabe's avatar
Peter Schwabe committed
41
to show that the semantics of the program satisfy a functional specification in Coq.
42
To the best of our knowledge, this is the first time that the
Peter Schwabe's avatar
Peter Schwabe committed
43
44
45
VST is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive.

46
In the last step we prove that the Coq implementation matches
Peter Schwabe's avatar
Peter Schwabe committed
47
the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.
Freek Wiedijk's avatar
Freek Wiedijk committed
48
This provides additional confidence that there are no transcription errors
Freek Wiedijk's avatar
wording    
Freek Wiedijk committed
49
in our formalized version of X25519.
50
We do this by extending the Coq library
Benoit Viguier's avatar
Benoit Viguier committed
51
for elliptic curves~\cite{BartziaS14} by Bartzia and Strub to
52
support Montgomery curves, and in particular Curve25519.
Peter Schwabe's avatar
Peter Schwabe committed
53
This extension may be of independent interest.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
54

Peter Schwabe's avatar
Peter Schwabe committed
55
\subheading{Related work.}
56
Two methodologies exist to get formal guarantees that software meets its specification.
Peter Schwabe's avatar
Peter Schwabe committed
57
The first is to write a formal specification and then synthesize
Benoit Viguier's avatar
Benoit Viguier committed
58
machine code by refinement; the second is to formalize
Peter Schwabe's avatar
Peter Schwabe committed
59
a specification and then verify that some
Benoit Viguier's avatar
Benoit Viguier committed
60
implementation satisfies it.
Benoit Viguier's avatar
Benoit Viguier committed
61

Peter Schwabe's avatar
Peter Schwabe committed
62
The synthesis approach was used by Zinzindohou{\'{e}}, Bartzia, and Bhargavan to build a verified extensible
Benoit Viguier's avatar
Benoit Viguier committed
63
64
65
66
library of elliptic curves~\cite{Zinzindohoue2016AVE} 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.

Benoit Viguier's avatar
Benoit Viguier committed
67
Coq not only allows verification but also synthesis~\cite{CpdtJFR}.
Peter Schwabe's avatar
Peter Schwabe committed
68
69
70
71
72
73
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}.

The verification approach has been used to prove the correctness of OpenSSL's
74
implementations of HMAC~\cite{Beringer2015VerifiedCA}, mbedTLS HMAC-DRBG~\cite{2017-Ye} and SHA-256~\cite{2015-Appel}.
Peter Schwabe's avatar
Peter Schwabe committed
75
76
77
78
79
80
In terms of languages and tooling, this work is closest to what we present here,
but our work considers an asymmetric primitive and provides computer-verified
proofs up to the mathematical definition of the group theory behind elliptic curves.

When considering the target of the verification effort, the closest work
to this paper is presented in~\cite{Chen2014VerifyingCS}, which presents
Benoit Viguier's avatar
mods    
Benoit Viguier committed
81
82
a mechanized proof of two assembly-level implementations of the core function
of X25519.
Benoit Viguier's avatar
Benoit Viguier committed
83
The proof in~\cite{Chen2014VerifyingCS} takes a different approach from ours.
Benoit Viguier's avatar
mods    
Benoit Viguier committed
84
It uses heavy annotation of code in order to ``guide'' a SAT solver,
Peter Schwabe's avatar
Peter Schwabe committed
85
86
also, it does not cover the full X25519 functionality and does
not make the link to the mathematical definition from~\cite{Ber06}.
Benoit Viguier's avatar
typos    
Benoit Viguier committed
87
We only need to annotate the specifications and loop invariants.
Peter Schwabe's avatar
Peter Schwabe committed
88
89
90
91
92
93
94
95
96
97
98

%Synthesis approaches force the user to depend on generated code which may not
%be optimal (speed, compactness) and they require compiler tweaks in order
%to achieve the desired properties. On the other hand, carefully handcrafted
%optimized code forces the verifier to consider all the possible special cases
%and write a low-level specification of the details of the code in order to prove
%the correctness of the algorithm.

%It has to be noted that Curve25519 implementations have already been under scrutiny
%However in this paper we provide a proofs of correctness and soundness of a C program up to
%the theory of elliptic curves.
Benoit Viguier's avatar
Benoit Viguier committed
99

100
\subheading{Reproducing the proofs.}
Benoit Viguier's avatar
Benoit Viguier committed
101
To maximize reusability of our results we placed the code of our formal proof
Benoit Viguier's avatar
Benoit Viguier committed
102
presented in this paper into the public domain.
103
It is available at \todo{FIX ME: https://cdn-09.anonfile.com/6fp8ta70n9/014c4f8c-1569921449/coq-verif-tweetnacl.tar.gz}
Benoit Viguier's avatar
Benoit Viguier committed
104
with instructions of how to compile and verify our proof.
105
A description of the content of the code archive is provided in
Benoit Viguier's avatar
Benoit Viguier committed
106
Appendix~\ref{appendix:proof-folders}.
Benoit Viguier's avatar
done    
Benoit Viguier committed
107

108
\subheading{Organization of this paper.}
Peter Schwabe's avatar
Peter Schwabe committed
109
\sref{sec:preliminaries} gives the necessary background on Curve25519 and X25519
110
implementations and a brief explanation of how formal verification works.
Peter Schwabe's avatar
Peter Schwabe committed
111
112
113
\sref{sec:Coq-RFC} provides our Coq formalization of X25519 as specified in RFC~7748~\cite{rfc7748}.
\sref{sec:C-Coq} provides the specifications of X25519 in TweetNaCl and some of the
proof techniques used to show the correctness with respect to RFC~7748~\cite{rfc7748}.
Benoit Viguier's avatar
Benoit Viguier committed
114
\sref{sec:maths} describes our extension of the formal library by Bartzia
115
and Strub and the correctness of X25519 implementation with respect to Bernstein's
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
116
specifications~\cite{Ber14}.
Peter Schwabe's avatar
Peter Schwabe committed
117
Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs.
Benoit Viguier's avatar
Benoit Viguier committed
118

Benoit Viguier's avatar
Benoit Viguier committed
119
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
Benoit Viguier's avatar
Benoit Viguier committed
120
121
C source files are represented by {\color{doc@lstfunctions}.C} while
{\color{doc@lstfunctions}.V} corresponds to Coq files.
Benoit Viguier's avatar
Benoit Viguier committed
122
123
124
125

\begin{figure}[h]
  \centering
  \include{tikz/proof}
Benoit Viguier's avatar
Benoit Viguier committed
126
  \caption{Structure of the proof.}
Benoit Viguier's avatar
Benoit Viguier committed
127
128
  \label{tikz:ProofOverview}
\end{figure}
Benoit Viguier's avatar
done    
Benoit Viguier committed
129

Benoit Viguier's avatar
forward    
Benoit Viguier committed
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
% 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