1-intro.tex 9.32 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 \emph{the first cryptographic library that allows correct functionality benoit committed Sep 09, 2020 10 to be verified by auditors with reasonable effort''}~\cite{BGJ+15}. Peter Schwabe committed Jul 29, 2019 11 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 Feb 15, 2020 16 by Bernstein in~\cite{Ber06}. 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 Feb 15, 2020 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 committed Sep 20, 2019 32 This proof is done in three steps: Peter Schwabe committed Oct 01, 2019 33 34 We first formalize RFC~7748~\cite{rfc7748} in Coq~\cite{coq-faq}. Benoit Viguier committed Sep 20, 2019 35 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 Feb 15, 2020 40 VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic} benoit committed Sep 15, 2020 41 to show that the semantics of the program satisfies a functional specification in Coq. Benoit Viguier committed Feb 15, 2020 42 To the best of our knowledge, this is the first time that VST Peter Schwabe committed Feb 15, 2020 43 is used in the formal proof of correctness of an implementation Peter Schwabe committed Jul 30, 2019 44 45 of an asymmetric cryptographic primitive. Peter Schwabe committed Feb 15, 2020 46 In the last step we prove that the Coq formalization of the RFC 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 Feb 15, 2020 51 Peter Schwabe committed Feb 15, 2020 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 Peter Schwabe committed Feb 15, 2020 55 to the mathematical definition in terms of scalar multiplication on an elliptic curve. Peter Schwabe committed Feb 15, 2020 56 57 58 59 60 As a consequence, the result of this paper can readily be used in mechanized proofs of higher-level protocols that work with the mathematical definition of X25519. Also, connecting our formalization of the RFC to the mathematical definition significantly increases trust into the correctness of the formalization and reduces the effort of manual auditing of that formalization. Benoit Viguier committed Jul 03, 2019 61 Peter Schwabe committed Jul 30, 2019 62 \subheading{Related work.} Peter Schwabe committed Feb 15, 2020 63 64 65 66 67 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 committed Feb 15, 2020 68 This SoK paper, in Section III.C, also gives an overview of verification efforts of Peter Schwabe committed Feb 15, 2020 69 70 71 72 73 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 committed Feb 15, 2020 74 There are two general approaches to establish this link Peter Schwabe committed Feb 15, 2020 75 76 77 78 79 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 committed Feb 15, 2020 80 The X25519 implementation from the Evercrypt project~\cite{EverCrypt} Peter Schwabe committed Feb 15, 2020 81 82 uses a low-level language called Vale that translates directly to assembly and proves equivalence to a high-level specification in F$^*$. Benoit Viguier committed Feb 15, 2020 83 In~\cite{Zinzindohoue2016AVE}, Zinzindohou{\'{e}}, Bartzia, and Bhargavan Peter Schwabe committed Feb 15, 2020 84 85 86 87 88 89 90 91 92 93 94 95 96 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 of proving and synthesising: A fairly low-level implementation written in 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}. Peter Schwabe committed Feb 15, 2020 97 Peter Schwabe committed Feb 15, 2020 98 All of these X25519 verification efforts use a clean-slate approach to obtain code and proofs. Peter Schwabe committed Feb 15, 2020 99 Our effort targets existing software; we are aware of only one earlier work verifying existing X25519 software: Peter Schwabe committed Feb 15, 2020 100 101 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 committed Feb 15, 2020 102 103 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 committed Sep 28, 2019 104 105 also, it does not cover the full X25519 functionality and does not make the link to the mathematical definition from~\cite{Ber06}. Peter Schwabe committed Feb 15, 2020 106 107 108 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 committed Feb 15, 2020 109 110 implementations of HMAC~\cite{Beringer2015VerifiedCA}, and mbedTLS' implementations of Peter Schwabe committed Feb 15, 2020 111 HMAC-DRBG~\cite{2017-Ye} and SHA-256~\cite{2015-Appel}. Peter Schwabe committed Feb 15, 2020 112 113 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 committed Aug 05, 2019 114 Peter Schwabe committed Jun 20, 2019 115 \subheading{Reproducing the proofs.} Benoit Viguier committed Feb 15, 2020 116 117 To maximize reusability of our results we place the code of our formal proof presented in this paper into the public domain. benoit committed Sep 09, 2020 118 It is available at \url{https://github.com/coq-verif-tweetnacl/coq-verif-tweetnacl/} Benoit Viguier committed Jul 22, 2019 119 with instructions of how to compile and verify our proof. Peter Schwabe committed Oct 01, 2019 120 A description of the content of the code archive is provided in Benoit Viguier committed Aug 05, 2019 121 Appendix~\ref{appendix:proof-folders}. Benoit Viguier committed Jun 06, 2019 122 Peter Schwabe committed Jun 20, 2019 123 \subheading{Organization of this paper.} Peter Schwabe committed Sep 28, 2019 124 \sref{sec:preliminaries} gives the necessary background on Curve25519 and X25519 Benoit Viguier committed Sep 02, 2019 125 implementations and a brief explanation of how formal verification works. Peter Schwabe committed Sep 28, 2019 126 127 128 \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 129 \sref{sec:maths} describes our extension of the formal library by Bartzia Benoit Viguier committed Sep 02, 2019 130 and Strub and the correctness of X25519 implementation with respect to Bernstein's Benoit Viguier committed Jul 03, 2019 131 specifications~\cite{Ber14}. Peter Schwabe committed Feb 15, 2020 132 Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs Benoit Viguier committed Feb 15, 2020 133 and conclude with some lessons learned about TweetNaCl and with sketching the Peter Schwabe committed Feb 15, 2020 134 effort required to extend our work to other elliptic-curve software. Benoit Viguier committed Jan 17, 2020 135 Benoit Viguier committed Sep 20, 2019 136 \fref{tikz:ProofOverview} shows a graph of dependencies of the proofs. Benoit Viguier committed Jan 17, 2020 137 C source files are represented by {\color{doc@lstfunctions}.C} while benoit committed Sep 09, 2020 138 {\color{doc@lstfunctions}.V} corresponds to Coq files. benoit committed Sep 28, 2020 139 140 141 142 143 144 145 146 \todo{Double Check (new)} In a nutshell, we formalize X25519 into a Coq function \texttt{RFC}, and we write a specification in Separation logic with VST. The first step of CompCert compilation (clightgen) is used to translates the C source code into a DSL (CLight). By using VST, 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, under the same preconditions as used in the specification, \texttt{RFC} computes the desired results Benoit Viguier committed Sep 20, 2019 147 148 149 150 \begin{figure}[h] \centering \include{tikz/proof} Benoit Viguier committed Jan 16, 2020 151 \caption{Structure of the proof.} Benoit Viguier committed Sep 20, 2019 152 153 \label{tikz:ProofOverview} \end{figure} Benoit Viguier committed Jun 06, 2019 154 Benoit Viguier committed May 30, 2019 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 % 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