intro.tex 7.52 KB
 Peter Schwabe committed Jul 29, 2019 1 2 \section{Introduction} \label{sec:intro}  Peter Schwabe committed Jun 20, 2019 3   Peter Schwabe committed Jul 29, 2019 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 The Networking and Cryptography library (NaCl)~\cite{BLS12} is an easy-to-use high-security high-speed crypto library. It uses specialized code for different platform, making it complex and hard to audit. TweetNaCl~\cite{BGJ+15} is a compact reimplementation in C of the core functionalities of NaCl and is claimed to be \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 this claim, like formal verification of memory safety, but does not actually prove correctness of any of the primitives offered by the library. A core component of TweetNaCl (and NaCl) is the key-exchange protocol X25519~\cite{rfc7748}. This protocol is being used by a wide variety of applications~\cite{things-that-use-curve25519} such as SSH, Signal Protocol, Tor, Zcash, TLS to establish a shared secret over an insecure channel. % For example TweetNaCl is being used by ZeroMQ~\cite{zmq} %messaging queue system to provide portability to its users.  Benoit Viguier committed Jun 25, 2019 22 23 24 % XXX: TweetNaCl (find real-world use of TweetNaCl?) % Mega.nz uses tweetnacl-js (as JS port of tweetnacl) for their webclient https://mega.nz/ % Keybase client: https://github.com/keybase/node-nacl/blob/master/lib/tweetnacl.js  Peter Schwabe committed Jun 20, 2019 25   Benoit Viguier committed May 24, 2019 26   Benoit Viguier committed Jun 21, 2019 27 This library makes use of Curve25519~\cite{Ber06}, a function over a \F{p}-restricted  Benoit Viguier committed Jun 04, 2019 28 29 30 $x$-coordinate computing a scalar multiplication on $E(\F{p^2})$, where $p$ is the prime number $\p$ and $E$ is the elliptic curve $y^2 = x^3 + 486662 x^2 + x$.  Benoit Viguier committed Jul 22, 2019 31 Originally, the name Curve25519'' referred to the key exchange protocol,  Benoit Viguier committed Jun 25, 2019 32 33 34 but Bernstein suggested to rename the scheme to X25519 and to use the name Curve25519 for the underlying elliptic curve~\cite{Ber14}. We make use of this notation in this paper.  Benoit Viguier committed Jul 22, 2019 35 % do we need to specify which "this" refers to ?  Benoit Viguier committed Jun 21, 2019 36 37  \subheading{Contribution of this paper}  Benoit Viguier committed Jul 03, 2019 38 39 We provide a mechanized formal proof of the correctness of X25519 implementation in TweetNaCl. This is done by first extending the formal library for  Benoit Viguier committed Jul 22, 2019 40 41 elliptic curves~\cite{DBLP:conf/itp/BartziaS14} of Bartzia and Strub to support Curve25519. Then we prove the code correctly implements the definitions  Benoit Viguier committed Jul 03, 2019 42 43 from the original paper by Bernstein~\cite{Ber14}.  Benoit Viguier committed Jul 22, 2019 44 45 46 47 48 49 50 % In order to get formal guaranties a software meets its % specifications, two methodologies exist. There are two methodologies to get formal guarantees a software meets its specifications. The first one is by synthesizing a formal specification and then generating machine code by refinement. % in order to get a software correct by construction.  Benoit Viguier committed Jun 21, 2019 51 52 This approach is being used in e.g. the B-method~\cite{Abrial:1996:BAP:236705}, F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17}, or with Coq~\cite{CpdtJFR}.  Benoit Viguier committed Jun 06, 2019 53 However this first method cannot be applied to an existing piece of software.  Benoit Viguier committed Jul 22, 2019 54 55 56 57 58  The second approach consists of writing the specifications and then verifying the correctness of the implementation. Because we verify the TweetNaCl cryptographic library, we use this second method.  Benoit Viguier committed Jun 06, 2019 59   Peter Schwabe committed Jun 20, 2019 60 \subheading{Our Formal Approach.}  Benoit Viguier committed Jul 22, 2019 61 62 Our verification process can be seen as a static analysis over the input values coupled with the formal proof that the code of the algorithm matches its specification.  Benoit Viguier committed Feb 09, 2018 63   Benoit Viguier committed Jun 21, 2019 64 We use Coq~\cite{coq-faq}, a formal system that allows us to machine-check our proofs.  Benoit Viguier committed Jul 10, 2019 65 66 Some famous examples of its use are the proof of the Four Color Theorem~\cite{gonthier2008formal}; or CompCert, a C~compiler~\cite{Leroy-backend} which proven correct and sound by being build on top of it.  Benoit Viguier committed Jul 22, 2019 67 In its proof, CompCert uses multiple intermediate languages and show equivalence between them.  Benoit Viguier committed Jul 10, 2019 68 The first step of the compilation by CompCert is done by the parser \textit{clightgen}.  Benoit Viguier committed Jun 21, 2019 69 It takes as input C code and generates its Clight~\cite{Blazy-Leroy-Clight-09} translation.  Benoit Viguier committed Jun 06, 2019 70 71  Using this intermediate representation Clight, we use the Verifiable Software Toolchain  Benoit Viguier committed Jun 21, 2019 72 (VST)~\cite{2012-Appel}, a framework which uses Separation logic~\cite{1969-Hoare,Reynolds02separationlogic}  Benoit Viguier committed Jun 06, 2019 73 74 and shows that the semantics of the program satisfies a functionnal specification in Coq. VST steps through each line of Clight using a strongest post-condition strategy.  Benoit Viguier committed Jul 22, 2019 75 We write a specification of TweetNaCl's crypto scalar multiplication and using  Benoit Viguier committed Jun 06, 2019 76 77 VST we prove that the code matches our definitions.  Benoit Viguier committed Jul 22, 2019 78 79 80 We extend Bartzia and Strub's elliptic curves library~\cite{DBLP:conf/itp/BartziaS14} to support Montgomery curves. With this formalization, we prove the correctness of a generic Montgomery ladder and show that our specification is an instance of it.  Benoit Viguier committed Jun 06, 2019 81   Peter Schwabe committed Jun 20, 2019 82 \subheading{Related work.}  Benoit Viguier committed Jun 06, 2019 83   Peter Schwabe committed Jun 20, 2019 84 85 \todo{Separate verification of existing code from generating proof-carrying code.}  Benoit Viguier committed Jul 22, 2019 86 87 88 89 Similar approaches have been used to prove the correctness of OpenSSL HMAC~\cite{Beringer2015VerifiedCA} and SHA-256~\cite{2015-Appel}. Compared to their work our approaches makes a complete link between the C implementation and the formal mathematical definition of the group theory behind elliptic curves.  Benoit Viguier committed Jun 06, 2019 90 91  Using the synthesis approach, Zinzindohou{\'{e}} et al. wrote an verified extensible  Benoit Viguier committed Jun 21, 2019 92 93 library of elliptic curves~\cite{Zinzindohoue2016AVE}. This served as ground work for the cryptographic library HACL*~\cite{zinzindohoue2017hacl} used in the NSS suite from Mozilla.  Benoit Viguier committed Jun 06, 2019 94 95  Coq does not only allows verification but also synthesis.  Benoit Viguier committed Jun 21, 2019 96 97 98 Using correct-by-construction finite field arithmetic~\cite{Philipoom2018CorrectbyconstructionFF} one can synthesize~\cite{Erbsen2016SystematicSO} certified elliptic curve implementations~\cite{Erbsen2017CraftingCE}. These implementation are now being used in BoringSSL~\cite{fiat-crypto}.  Benoit Viguier committed Jun 06, 2019 99   Benoit Viguier committed Jun 21, 2019 100 Curve25519 implementations has already been under the scrutiny~\cite{Chen2014VerifyingCS}.  Benoit Viguier committed Jun 06, 2019 101 102 103 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 Jul 03, 2019 104 105 106 107 108 109 Synthesis approaches forces the user to depend on generated code which may not be optimal (speed, compactness...), they require to tweak the compiler in order to achieve the desired properties. On the other hand a carefully handcrafted optimized code will force the verifier to consider all the possible special cases and write a complex low level specification in order to prove the correctness of the algorithm.  Benoit Viguier committed Jun 06, 2019 110   Peter Schwabe committed Jun 20, 2019 111 \subheading{Reproducing the proofs.}  Benoit Viguier committed Jul 22, 2019 112 To maximize reusability of our results we placed the code of our formal proof  Benoit Viguier committed Jun 06, 2019 113 presented in this paper into the public domain. They are available at XXXXXXX  Benoit Viguier committed Jul 22, 2019 114 with instructions of how to compile and verify our proof.  Benoit Viguier committed Jun 06, 2019 115   Peter Schwabe committed Jun 20, 2019 116 \subheading{Organization of this paper.}  Benoit Viguier committed Jul 03, 2019 117 118 119 120 121 122 123 124 Section~\ref{preliminaries} give the necessary background on Curve25519 implementation and a rough understand of how formal verification works. Section~\ref{C-Coq} provides the specification of X25519 in addition to proofs techniques used to show the correctness. Section~\ref{sec3-maths} describes our extension of the formal library by Bartzia and Strub and the correctness of X25519 implementation with respect to Bernstein specifications~\cite{Ber14}. And lastly in Section~\ref{Conclusion} we discuss the trust in this proof.  Benoit Viguier committed Jun 06, 2019 125   Benoit Viguier committed Jun 04, 2019 126   Benoit Viguier committed May 30, 2019 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 % 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