Commit 712bc435 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more writting

parent adfd17c6
\subsection*{Abstract}
% \subsection*{Abstract}
\begin{abstract}
By using the Coq formal proof assistant, we first extend
the formalization of elliptic curves of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support
Montgomery curves. Then with the Verified Software Toolchain \cite{2012-Appel}
we prove the soundness and correctness of TweetNaCl's Curve25519 implementation.
\end{abstract}
......@@ -3,8 +3,20 @@
Implementing cryptographic primitives without any bugs is hard.
While tests provides a code coverage and are used in the limits,
they still don't cover 100\% of the possible input values.
Our method is can be seen as a static analysis over the input values coupled
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.
As we verify an existing cryptographic library, we use the second approach.
Our method 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.
Similar approaches have been used to prove the correctness of OpenSSL HMAC
\cite{Beringer2015VerifiedCA} and SHA-256 \cite{Appel2015VerificationOA}.
TweetNaCl\cite{BGJ+15} is a compact reimplementation of the
NaCl\cite{BLS12} library. It does not aim for high speed
......@@ -12,13 +24,13 @@ application and has been optimized for source code compactness.
It maintains some degree of readability in order to be easily auditable.
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$.
$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$.
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.
The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain (VST)\cite{2012-Appel} are build
on top of it.
The Compcert\cite{Leroy-backend} compiler and the Verifiable Software Toolchain
(VST)\cite{2012-Appel} are build on top of it.
Our approach is as follow, we use the \textit{clightgen} tool from Compcert to
generate the \textit{semantic version} (Clight\cite{Blazy-Leroy-Clight-09}) of
......@@ -26,6 +38,7 @@ 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.
We extend the work of Bartzia and Strub \cite{DBLP:conf/itp/BartziaS14} to support Montgomery curves.
We extend the work of Bartzia and Strub \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 can be seen as an instance of it.
\section{Curve25519 implementation}
In this section we present in detail the algorithm computing the crypto scalar multiplication.
We then discuss what will be the required proofs.
We then discuss which proofs are required.
\subsection{Implementation} \label{sec:impl}
Given a natural number $n$ and a value $x \in \F{p}$, Curve25519 is a function over a $\F{p}$-restricted
$x$-coordinate computing a scalar multiplication on $E(\F{p^2})$.
Due to this restriction, all computations are done over $\F{p}$.
Number in that field can be represented by a 256-bits number.
We can represent them in either 8-bit limbs (respectively 16-bit limbs),
As a result of this restriction, all computations are done over $\F{p}$.
Numbers in that field can be represented by with 256 bits.
We represent them in 8-bit limbs (respectively 16-bit limbs),
making use of a base $2^8$ (respectively $2^{16}$).
As a result, input of the Curve25519 function are seen as arrays of bytes.
Consequently, inputs of the Curve25519 function are seen as arrays of bytes.
Computations inside this function makes use of the 16-bit limbs representation.
Those are placed into 64-bits signed container in order to mitigate overflows or underflows.
\begin{lstlisting}[language=Ctweetnacl]
typedef long long i64;
typedef i64 gf[16];
\end{lstlisting}
We notice this does not guaranty a unique representation of each number. i.e.\\
Notice this does not guaranty a unique representation of each number. i.e.\\
$\exists x,y \in$ \TNaCle{gf} such that
\vspace{-0.25cm}
$$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$
On the other hand it allows simple definitions of addition (\texttt{A}),
substraction (\texttt{Z}) and a (school-book) multiplication (\texttt{M}).
substraction (\texttt{Z}), and school-book multiplication (\texttt{M}).
% and squaring (\texttt{S}).
\begin{lstlisting}[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b) {
int i;
......@@ -77,8 +77,8 @@ sv car25519(gf o)
At the end of the Montgomery ladder, we have to compute an inverse.
This is done using the Fermat's little theorem by the exponentiation to
$2^{255}-21$ with the Square-and-multiply algorithm and taking
advantage of the shape of the number.
$2^{255}-21$ with the Square-and-multiply algorithm. It takes
advantage of the shape of the number by not doing the multiplications only twice.
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf a)
{
......@@ -93,12 +93,11 @@ sv inv25519(gf o,const gf a)
}
\end{lstlisting}
The last step of \texttt{crypto\_scalarmult} is the packing of the limbs, it returns
an array of bytes. It first performs 3 carry propagations in order to guarantee
The last step of \texttt{crypto\_scalarmult} is the packing of the limbs: an array of 32 bytes.
It first performs 3 carry propagations in order to guarantee
that each 16-bit limbs values are between $0$ and $2^{16}$.
Then it computes a modulo reduction by $\p$ by iterative substraction and
conditional swap until it reaches a negative number.
This guarantees a unique representation in $\Zfield$.
Then computes a modulo reduction by $\p$ using iterative substraction and
conditional swapping. This guarantees a unique representation in $\Zfield$.
After which each 16-bit limbs are splitted into 8-bit limbs.
\begin{lstlisting}[language=Ctweetnacl]
......@@ -130,7 +129,7 @@ sv pack25519(u8 *o,const gf n)
\end{lstlisting}
The full Montgomery ladder is defined as follow.
First extract and clamb the value of $n$. Then unpack the value of $p$.
First extract and clamp the value of $n$. Then unpack the value of $p$.
Compute the Montgomery ladder over the clamped $n$ and $p$, pack the result into $q$.
\begin{lstlisting}[language=Ctweetnacl]
int crypto_scalarmult(u8 *q,
......@@ -190,15 +189,11 @@ subsequently called: \texttt{unpack25519}; \texttt{A}; \texttt{Z}; \texttt{M};
\texttt{pack25519}.
We prove that the implementation of Curve25519 is \textbf{sound} \ie
\begin{itemize}
\item absence of access out-of-bounds of arrays (memory safety).
\item absence of overflows/underflow on the arithmetic.
\end{itemize}
\noindent
We also prove that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
\item Curve25519 is correctly implemented (we get what we expect).
\item Operations on \texttt{gf} (\texttt{A}, \texttt{Z}, \texttt{M}, \texttt{S})
......@@ -209,17 +204,15 @@ are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
In order to prove the soundness and correctness of \texttt{crypto\_scalarmult},
we define multiples levels of specifications.
A high level specification (over a generic field $\K$) looking only at
the structure of the Montgomery ladder provided us with the correcntess.
the structure of the Montgomery ladder provide us with the correctness of the algorithm.
A low level specification close to the \texttt{C} code (over lists of $\mathbb{Z}$)
gave us the soundness assurance.
We defined a third specification over \Zfield (mid level) and
we proved to be an instance of the high level one.
We also proved its equivalence with the low level one.
As such we proved all specifications to equivalent (Fig.\ref{tk:ProofStructure}).
This garantees us the correctness of the
implementation.
gives us the soundness assurance.
We define a third specification over \Zfield (mid level) and
prove it to be an instance of the high level one.
We also prove its equivalence with the low level one.
As such we prove all specifications to equivalent (Fig.\ref{tk:ProofStructure}).
This garantees us the correctness of the implementation.
\begin{figure}[h]
\include{tikz/specifications}
......@@ -229,10 +222,8 @@ implementation.
\subsection{Correctness specification}
% The soundness is implied by the proof of the following specification.
We show the soundness of TweetNaCl by proving the {\red{equivalence}} of the following
specification. This defines the equivalence between the Clight representation
and a Coq definition of the ladder.
We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function.
This defines the equivalence between the Clight representation and a Coq definition of the ladder.
\begin{CoqVST}
Definition crypto_scalarmult_spec :=
......@@ -306,8 +297,8 @@ Theorem Crypto_Scalarmult_Correct:
forall (n p:list Z) (P:mc curve25519_Fp2_mcuType),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
Forall (fun x => 0 <= x /\ x < 2^8) n ->
Forall (fun x => 0 <= x /\ x < 2^8) p ->
Fp2_x (ZUnpack25519 (ZofList 8 p)) = P#x0 ->
ZofList 8 (Crypto_Scalarmult n p) =
(P *+ (Z.to_nat (Zclamp (ZofList 8 n)))) _x0.
......
......@@ -141,7 +141,7 @@ Definition addmc (p1 p2 : mc) : mc :=
We then prove a bijection between a Montgomery curve and its Weierstra{\ss} equation.
\begin{lemma}
Let $M_{a,b}(\K)$ be a Mongomery curve, Define $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
Let $M_{a,b}(\K)$ be a Montgomery curve, Define $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
Then $E_{a',b'}(\K)$ is an elliptic curve, and the mapping $\varphi : M_{a,b}(\K) \mapsto E_{a',b'}(\K)$ defined as:
\begin{align*}
\varphi(\Oinf_M) &= \Oinf_E\\
......
This diff is collapsed.
This diff is collapsed.
This diff is collapsed.
......@@ -1129,3 +1129,102 @@ VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: F
doi = {10.1090/S0025-5718-1987-0866113-7},
note = {\url{http://links.jstor.org/sici?sici=0025-5718(198701)48:177<243:STPAEC>2.0.CO;2-3}}
}
@book{Abrial:1996:BAP:236705,
author = {Jean-Raymond Abrial},
title = {The B-book: Assigning Programs to Meanings},
year = {1996},
isbn = {0-521-49619-5},
publisher = {Cambridge University Press},
address = {New York, NY, USA},
}
@article{DBLP:journals/corr/BhargavanDFHPRR17,
author = {Karthikeyan Bhargavan and
Antoine Delignat{-}Lavaud and
C{\'{e}}dric Fournet and
Catalin Hritcu and
Jonathan Protzenko and
Tahina Ramananandro and
Aseem Rastogi and
Nikhil Swamy and
Peng Wang and
Santiago Zanella B{\'{e}}guelin and
Jean Karim Zinzindohou{\'{e}}},
title = {Verified Low-Level Programming Embedded in {F}},
journal = {CoRR},
volume = {abs/1703.00053},
year = {2017},
url = {http://arxiv.org/abs/1703.00053},
archivePrefix = {arXiv},
eprint = {1703.00053},
timestamp = {Mon, 13 Aug 2018 16:46:57 +0200},
biburl = {https://dblp.org/rec/bib/journals/corr/BhargavanDFHPRR17},
bibsource = {dblp computer science bibliography, https://dblp.org}
}
@article{Zinzindohoue2016AVE,
title={A Verified Extensible Library of Elliptic Curves},
author={Jean Karim Zinzindohoue and Evmorfia-Iro Bartzia and Karthikeyan Bhargavan},
journal={2016 IEEE 29th Computer Security Foundations Symposium (CSF)},
year={2016},
pages={296-309}
}
@inproceedings{Chen2014VerifyingCS,
title={Verifying Curve25519 Software},
author={Yu-Fang Chen and Chang-Hong Hsu and Hsin-Hung Lin and Peter Schwabe and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang and Shang-Yi Yang},
booktitle={ACM Conference on Computer and Communications Security},
year={2014}
}
@article{Appel2015VerificationOA,
title={Verification of a Cryptographic Primitive: SHA-256},
author={Andrew W. Appel},
journal={ACM Trans. Program. Lang. Syst.},
year={2015},
volume={37},
pages={7:1-7:31}
}
@inproceedings{Beringer2015VerifiedCA,
title={Verified Correctness and Security of OpenSSL HMAC},
author={Lennart Beringer and Adam Petcher and Katherine Q. Ye and Andrew W. Appel},
booktitle={USENIX Security Symposium},
year={2015}
}
@inproceedings{Erbsen2017CraftingCE,
title={Crafting certified elliptic curve cryptography implementations in Coq},
author={Andres Erbsen},
year={2017}
}
@inproceedings{Philipoom2018CorrectbyconstructionFF,
title={Correct-by-construction finite field arithmetic in Coq},
author={Jade Philipoom},
year={2018}
}
@inproceedings{Erbsen2016SystematicSO,
title={Systematic Synthesis of Elliptic Curve Cryptography Implementations},
author={Andres Erbsen and Jason Gross and Adam Chlipala},
year={2016}
}
@inproceedings{Erbsen2019SimpleHC,
title={Simple High-Level Code for Cryptographic Arithmetic - With Proofs, Without Compromises},
author={Andres Erbsen and Jade Philipoom and Jason Gross and Robert H. Sloan and Adam Chlipala},
booktitle={S&P 2019},
year={2019}
}
@Article{CpdtJFR,
author = {Adam Chlipala},
title = {An Introduction to Programming and Proving with Dependent Types in Coq},
volume = {3(2)},
pages = {1-93},
year = {2010},
journal = {Journal of Formalized Reasoning},
url = {http://adam.chlipala.net/papers/CpdtJFR/}
}
......@@ -20,8 +20,10 @@
% usepackage command, below.
% This version uses the latex2e styles, not the very ancient 2.09 stuff.
\documentclass[letterpaper,twocolumn,9pt]{article}
\usepackage{usenix,epsfig}
% \documentclass[letterpaper,twocolumn,9pt]{article}
\documentclass[conference, 9pt]{IEEEtran}
% \usepackage{usenix}
\usepackage{epsfig}
\usepackage{setup}
\newif\ifpublic
......
......@@ -276,6 +276,8 @@ literate=
{~}{{\ }}1
% {\@\@}{{$@$}}1
{:GF}{{\color{doc@lstfunctions}{:$GF$}}}1
% {0}{{\color{doc@lstnumbers}{$0$}}}1
{32}{{\color{doc@lstnumbers}{$32$}}}1
{2^8}{{\color{doc@lstnumbers}{$2^8$}}}1
{2^16}{{\color{doc@lstnumbers}{$2^{16}$}}}1
{2^26}{{\color{doc@lstnumbers}{$2^{26}$}}}1
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment