1_intro.tex 7.23 KB
 Peter Schwabe committed Jul 29, 2019 1 2 \section{Introduction} \label{sec:intro}  Peter Schwabe committed Jun 20, 2019 3   Benoit Viguier committed Aug 01, 2019 4 5 The Networking and Cryptography library (NaCl)~\cite{BLS12} is an easy-to-use, high-security, high-speed cryptography library.  Benoit Viguier committed Aug 16, 2019 6 It uses specialized code for different platforms, which makes it rather complex and hard to audit.  Benoit Viguier committed Aug 01, 2019 7 8 TweetNaCl~\cite{BGJ+15} is a compact re-implementation in C of the core functionalities of NaCl and is claimed to be  Peter Schwabe committed Jul 29, 2019 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 committed Jul 30, 2019 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.  Peter Schwabe committed Jul 29, 2019 14   Benoit Viguier committed Sep 30, 2019 15 One core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519 presented  Peter Schwabe committed Sep 28, 2019 16 by Bernstein in~\cite{rfc7748}.  Benoit Viguier committed Oct 01, 2019 17 This protocol is standardized in RFC~7748 and used by a wide variety of applications~\cite{things-that-use-curve25519}  Peter Schwabe committed Jul 30, 2019 18 such as SSH, Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over  Peter Schwabe committed Jul 29, 2019 19 an insecure channel.  Benoit Viguier committed Oct 01, 2019 20 21 The X25519 key-exchange protocol is an \xcoord-only elliptic-curve Diffie--Hellman key exchange using the Montgomery  Benoit Viguier committed Aug 01, 2019 22 curve $E: y^2 = x^3 + 486662 x^2 + x$ over the field $\F{\p}$.  Peter Schwabe committed Oct 01, 2019 23 Note that originally, the name Curve25519'' referred to the key-exchange protocol,  Peter Schwabe committed Sep 28, 2019 24 25 but Bernstein suggested to rename the protocol to X25519 and to use the name Curve25519 for the underlying elliptic curve~\cite{Ber14}.  Benoit Viguier committed Sep 27, 2019 26 We use this updated terminology in this paper.  Benoit Viguier committed Jun 21, 2019 27   Peter Schwabe committed Sep 29, 2019 28 \subheading{Contribution of this paper.}  Peter Schwabe committed Jul 30, 2019 29 We provide a mechanized formal proof of the correctness of the X25519  Benoit Viguier committed Aug 01, 2019 30 implementation in TweetNaCl.  Benoit Viguier committed Sep 20, 2019 31 This proof is done in three steps:  Peter Schwabe committed Oct 01, 2019 32 33  We first formalize RFC~7748~\cite{rfc7748} in Coq~\cite{coq-faq}.  Benoit Viguier committed Sep 20, 2019 34 35 % This part uses generic techniques to facilitate later proofs.  Peter Schwabe committed Oct 01, 2019 36 In the second step we prove equivalence of the C implementation of X25519  Benoit Viguier committed Sep 20, 2019 37 to our RFC formalization.  Peter Schwabe committed Jul 30, 2019 38 This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-Appel}  Benoit Viguier committed Aug 01, 2019 39 to establish a link between C and Coq.  Peter Schwabe committed Jul 30, 2019 40 41 42 43 44 45 VST uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic} to show that the semantics of the program satisfy a functional specification in Coq. To the best of our knowledge, this is the first time that VST is used in the formal proof of correctness of an implementation of an asymmetric cryptographic primitive.  Peter Schwabe committed Oct 01, 2019 46 In the last step we prove that the Coq implementation matches  Peter Schwabe committed Jul 30, 2019 47 the mathematical definition of X25519 as given in~\cite[Sec.~2]{Ber06}.  Peter Schwabe committed Oct 01, 2019 48 We do this by extending the Coq library  Benoit Viguier committed Aug 16, 2019 49 for elliptic curves~\cite{BartziaS14} by Bartzia and Strub to  Benoit Viguier committed Oct 01, 2019 50 support Montgomery curves, and in particular Curve25519.  Peter Schwabe committed Jul 30, 2019 51 This extension may be of independent interest.  Benoit Viguier committed Jul 03, 2019 52   Peter Schwabe committed Jul 30, 2019 53 \subheading{Related work.}  Benoit Viguier committed Sep 02, 2019 54 Two methodologies exist to get formal guarantees that software meets its specification.  Peter Schwabe committed Sep 28, 2019 55 The first is to write a formal specification and then synthesize  Benoit Viguier committed Sep 30, 2019 56 machine code by refinement; the second is to formalize  Peter Schwabe committed Sep 28, 2019 57 a specification and then verify that some  Benoit Viguier committed Aug 05, 2019 58 implementation satisfies it.  Benoit Viguier committed Jul 22, 2019 59   Benoit Viguier committed Aug 05, 2019 60 61 % One of the earliest example of this first approach is the % B-method~\cite{Abrial:1996:BAP:236705} in 1986.  Peter Schwabe committed Sep 28, 2019 62 The synthesis approach was used by Zinzindohou{\'{e}}, Bartzia, and Bhargavan to build a verified extensible  Benoit Viguier committed Aug 05, 2019 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 committed Aug 16, 2019 67 Coq not only allows verification but also synthesis~\cite{CpdtJFR}.  Peter Schwabe committed Sep 28, 2019 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  Benoit Viguier committed Sep 30, 2019 74 implementations of HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}.  Peter Schwabe committed Sep 28, 2019 75 76 77 78 79 80 81 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 a mechanized proof of two assembly-level implementations of the core function of X25519.  Benoit Viguier committed Sep 30, 2019 82 83 The proof in~\cite{Chen2014VerifyingCS} takes a different approach from ours. It uses heavy annotation of code together with SAT solvers;  Peter Schwabe committed Sep 28, 2019 84 85 86 87 88 89 90 91 92 93 94 95 96 also, it does not cover the full X25519 functionality and does not make the link to the mathematical definition from~\cite{Ber06}. %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 committed Aug 05, 2019 97   Peter Schwabe committed Jun 20, 2019 98 \subheading{Reproducing the proofs.}  Benoit Viguier committed Jul 22, 2019 99 To maximize reusability of our results we placed the code of our formal proof  Benoit Viguier committed Sep 20, 2019 100 presented in this paper into the public domain.  Benoit Viguier committed Sep 30, 2019 101 They are available at \url{https://anonfile.com/6fp8ta70n9/coq-verif-tweetnacl.tar_gz}  Benoit Viguier committed Jul 22, 2019 102 with instructions of how to compile and verify our proof.  Benoit Viguier committed Aug 05, 2019 103 104 A description of the content of the archive is provided in Appendix~\ref{appendix:proof-folders}.  Benoit Viguier committed Jun 06, 2019 105   Peter Schwabe committed Jun 20, 2019 106 \subheading{Organization of this paper.}  Peter Schwabe committed Sep 28, 2019 107 \sref{sec:preliminaries} gives the necessary background on Curve25519 and X25519  Benoit Viguier committed Sep 02, 2019 108 implementations and a brief explanation of how formal verification works.  Peter Schwabe committed Sep 28, 2019 109 110 111 \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 committed Aug 12, 2019 112 \sref{sec:maths} describes our extension of the formal library by Bartzia  Benoit Viguier committed Sep 02, 2019 113 and Strub and the correctness of X25519 implementation with respect to Bernstein's  Benoit Viguier committed Jul 03, 2019 114 specifications~\cite{Ber14}.  Peter Schwabe committed Sep 28, 2019 115 Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs.  Benoit Viguier committed Sep 20, 2019 116 117 118 119 120 121 122 123 \fref{tikz:ProofOverview} shows a graph of dependencies of the proofs. \begin{figure}[h] \centering \include{tikz/proof} \caption{Structure of the proof} \label{tikz:ProofOverview} \end{figure}  Benoit Viguier committed Jun 06, 2019 124   Benoit Viguier committed Jun 04, 2019 125   Benoit Viguier committed May 30, 2019 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 % 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