1_Introduction.tex 3.07 KB
 Benoit Viguier committed Nov 13, 2017 1 2 \section{Introduction}  Benoit Viguier committed Feb 09, 2018 3 Implementing cryptographic primitives without any bugs is hard.  Benoit Viguier committed May 17, 2019 4 While tests provides a code coverage and are used in the limits,  Benoit Viguier committed Mar 13, 2018 5 they still don't cover 100\% of the possible input values.  Benoit Viguier committed May 24, 2019 6 7 8 9 10 11 12 13 14  In order to get formal guaranties a software meets its specifications, two methodologies exist. The first one is by synthesizing a formal specification and generating machine code by refinment. This approach is being used in the B-method\cite{Abrial:1996:BAP:236705}, F* \cite{DBLP:journals/corr/BhargavanDFHPRR17} with Kremlin, or in Coq \cite{CpdtJFR}. 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 15 Verifying an existing cryptographic library, we use the second approach.  Benoit Viguier committed May 24, 2019 16 Our method can be seen as a static analysis over the input values coupled  Benoit Viguier committed May 17, 2019 17 with the formal proof that the code of the algorithm matches its specification.  Benoit Viguier committed May 24, 2019 18 19 Similar approaches have been used to prove the correctness of OpenSSL HMAC \cite{Beringer2015VerifiedCA} and SHA-256 \cite{Appel2015VerificationOA}.  Benoit Viguier committed Feb 09, 2018 20 21 22 23  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.  Benoit Viguier committed May 17, 2019 24 It maintains some degree of readability in order to be easily auditable.  Benoit Viguier committed Feb 09, 2018 25   Benoit Viguier committed May 03, 2019 26 This library makes use of Curve25519\cite{Ber06}, a function over a \F{p}-restricted  Benoit Viguier committed May 24, 2019 27 28 $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 Feb 09, 2018 29   Benoit Viguier committed May 17, 2019 30 31 Coq is a formal system that allows to machine-check our proofs. A famous example of its use is the proof of the Four Color Theorem.  Benoit Viguier committed May 24, 2019 32 33 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 34 35  Our approach is as follow, we use the \textit{clightgen} tool from Compcert to  Benoit Viguier committed Nov 13, 2017 36 generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of  Benoit Viguier committed May 17, 2019 37 38 39 40 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 41 42 We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support Montgomery curves.  Benoit Viguier committed May 17, 2019 43 44 With this formalization, we prove the correctness of a generic Montgomery ladder and show that our specification can be seen as an instance of it.  Benoit Viguier committed May 30, 2019 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62  % 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