1_Introduction.tex 3.28 KB
 Benoit Viguier committed Nov 13, 2017 1 2 \section{Introduction}  Benoit Viguier committed Jun 04, 2019 3 4 5 6 TweetNaCl\cite{BGJ+15} is a compact reimplementation of the NaCl\cite{BLS12} library. It does not aim for high speed application and has been optimized for source code compactness. It maintains some degree of readability in order to be easily auditable.  Benoit Viguier committed May 24, 2019 7   Benoit Viguier committed Jun 04, 2019 8 9 10 11 12 13 14 15 16 This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted $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$. This function is used by a wide variety of applications \cite{this-that-use-curve25519} to establish a shared secret over an insecure channel. Implementing cryptographic primitives without any bugs is difficult. While tests provides with code coverage, they still don't cover 100\% of the possible input values.  Benoit Viguier committed May 24, 2019 17 In order to get formal guaranties a software meets its specifications,  Benoit Viguier committed Jun 04, 2019 18 19 20 two methodologies exist. The first one is by synthesizing a formal specification and  Benoit Viguier committed May 24, 2019 21 generating machine code by refinment. This approach is being used in the  Benoit Viguier committed Jun 04, 2019 22 23 B-method\cite{Abrial:1996:BAP:236705}, HACL*\cite{zinzindohoue2017hacl} and F* \cite{DBLP:journals/corr/BhargavanDFHPRR17} with Kremlin, or with Coq \cite{CpdtJFR}.  Benoit Viguier committed May 24, 2019 24 25 26 27 This gives you a software correct by construction. However it cannot be applied to an existing piece of software. In such case we need to write the specifications and then verify the correctness of the implementation.  Benoit Viguier committed May 27, 2019 28 Verifying an existing cryptographic library, we use the second approach.  Benoit Viguier committed May 24, 2019 29 Our method can be seen as a static analysis over the input values coupled  Benoit Viguier committed May 17, 2019 30 with the formal proof that the code of the algorithm matches its specification.  Benoit Viguier committed May 24, 2019 31 Similar approaches have been used to prove the correctness of OpenSSL HMAC  Benoit Viguier committed Jun 04, 2019 32 \cite{Beringer2015VerifiedCA} and SHA-256 \cite{2015-Appel}.  Benoit Viguier committed Feb 09, 2018 33   Benoit Viguier committed May 17, 2019 34 Coq is a formal system that allows to machine-check our proofs.  Benoit Viguier committed Jun 04, 2019 35 A famous example of its use is the proof of the Four Color Theorem \cite{gonthier2008formal}.  Benoit Viguier committed May 24, 2019 36 37 The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build on top of it.  Benoit Viguier committed Feb 09, 2018 38 39  Our approach is as follow, we use the \textit{clightgen} tool from Compcert to  Benoit Viguier committed Nov 13, 2017 40 generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of  Benoit Viguier committed May 17, 2019 41 42 43 44 the TweetNaCl C code. Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic} with with the Verifiable Software Toolchain we show that the semantics of the program satisfies a functionnal specification in Coq.  Benoit Viguier committed May 24, 2019 45 46 We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support Montgomery curves.  Benoit Viguier committed May 17, 2019 47 With this formalization, we prove the correctness of a generic Montgomery ladder  Benoit Viguier committed Jun 05, 2019 48 and show that our specification is an instance of it.  Benoit Viguier committed May 30, 2019 49   Benoit Viguier committed Jun 04, 2019 50 51 \todo[inline]{Add where the software is available}  Benoit Viguier committed May 30, 2019 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 % 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