Commit c28bf94f authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more text in the Intro, taking account to Freek comments

parent 69f5be3a
\subsection*{Abstract}
By using the Coq formal proof assistant with the VST library, we prove the
soundness and correctness of TweetNaCl's Curve25519 implementation.
\section{Introduction}
Implementing cryptographic primitives without any bugs is hard. While tests
provides a decent code coverage, they don't cover 100\% of the possible values.
We verify the implementation in C of Curve25519 in Tweetnacl\cite{BGJ+15}.
Using the \textit{clightgen} tool from Compcert\cite{Leroy-backend}, we can
Implementing cryptographic primitives without any bugs is hard.
While tests provides a some code coverage, they don't cover
100\% of the possible input values. Using Coq, we prove the
correctness of the scalar multiplication in Tweetnacl.
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.
This library makes use of Curve25519\cite{Ber06}, an elliptic
curve defined over the field $\mathbb{Z}_{2^{255}-19}$.
It defines the function \texttt{crypto\_scalarmult} which
takes as input a scalar $n$ and the $x$ coordinate of a
point $P$ and returns the $x$ coordinate of the
point $[n]P$.
Coq is a formal system that allows us to machine-check our proofs. 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
the C code. Using the Floyd–Hoare logic\cite{1969-Hoare} with the Verifiable
Software Toolchain (VST)\cite{2012-Appel} we can show that the semantic of the
program is equivalent to a functionnal specification in Coq.
We can then prove that this specification is represent the scalar multiplication
on Curve25519\cite{}.
the TweetNaCl C code. Using the Separation logic\cite{1969-Hoare,Reynolds02separationlogic}
with (VST) we show that the semantics of the program satisfies a functionnal
specification in Coq. We then prove that this specification represent the scalar
multiplication on Curve25519.
\subsection{Meet-in-the-middle Approach}
In order to prove that \texttt{crypto\_scalarmult} is computing a scalar
multiplication over the x-coordinate of a point P, we need to define multiples
levels of specifications and show equivalence between them.
levels of specifications and show equivalence between them (Fig.\ref{tk:ProofStructure}).
\begin{enumerate}
\item Write a high level specification (over a generic field $\mathbb{F}$).
\item Show that the high level specification is equivalent to the
\item Prove that the high level specification is equivalent to the
computation of a montgomery ladder.
\item Write a low level specification (e.g. over lists of $\mathbb{Z}$).
\item Show that the low level specification represent the operations of
\item Prove that the low level specification represent the operations of
defined C code.
\item Show that the low level specification are equivalent to simple
operations in $\mathbb{Z}_{2^{255}-19}$ (middle level specification).
\item Show that the middle level specification is an instance of the high
\item Write a middle level specification over $\mathbb{Z}_{2^{255}-19}$.
\item Prove that the low level specification are equivalent to simple
operations in $\mathbb{Z}_{2^{255}-19}$ and thus equivalent to the middle level.
\item Prove that the middle level specification is an instance of the high
level one.
\end{enumerate}
The equivalence between each level, garantees us the correctness of the
implementation.
\begin{figure}[h]
\include{tikz/specifications}
\caption{Structural construction of the proof}
\label{tk:ProofStructure}
\end{figure}
......@@ -15,8 +15,12 @@ bits placed into 64-bits signed container.
typedef long long i64;
typedef i64 gf[16];
\end{lstlisting}
This representation does not guaranties uniqueness. i.e.\\
$\exists x,y \in \texttt{gf} \text{ such that }$
\vspace{-0.25cm}
$$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$
This representation allows simple definitions of addition (\texttt{A}),
It allows simple definitions of addition (\texttt{A}),
substraction (\texttt{Z}) and a (school-book) multiplication (\texttt{M}).
\begin{lstlisting}[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b) {
......@@ -24,6 +28,11 @@ sv A(gf o,const gf a,const gf b) {
FOR(i,16) o[i]=a[i]+b[i];
}
sv Z(gf o,const gf a,const gf b) {
int i;
FOR(i,16) o[i]=a[i]-b[i];
}
sv M(gf o,const gf a,const gf b) {
i64 i,j,t[31];
FOR(i,31) t[i]=0;
......@@ -49,6 +58,53 @@ sv car25519(gf o) {
}
\end{lstlisting}
At the end of the Mongomery ladder, we have the operation $A \cdot C^{-1}$.
The inverse of $C$ is computed using the Fermat's little theorem by the
exponentiation to $2^{255}-21$ with the Square-and-multiply algorithm.
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf a)
{
gf c;
int i;
set25519(c,a);
for(i=253;i>=0;i--) {
S(c,c);
if(i!=2&&i!=4) M(c,c,a);
}
FOR(i,16) o[i]=c[i];
}
\end{lstlisting}
The last step of the crypto\_scalarmult is the packing of the limbs, it returns
an array of bytes and guarantees the uniqueness of the representation in $\mathbb{Z}_{2^{255}-19}$.
\begin{lstlisting}[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
{
int i,j;
i64 b;
gf t,m={0};
set25519(t,n);
car25519(t);
car25519(t);
car25519(t);
FOR(j,2) {
m[0]=t[0]- 0xffed;
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
m[i-1]&=0xffff;
}
m[15]=t[15]-0x7fff-((m[14]>>16)&1);
m[14]&=0xffff;
b=1-((m[15]>>16)&1);
sel25519(t,m,b);
}
FOR(i,16) {
o[2*i]=t[i]&0xff;
o[2*i+1]=t[i]>>8;
}
}
\end{lstlisting}
The full Mongomery ladder is defined as follow:
\begin{lstlisting}[language=Ctweetnacl]
int crypto_scalarmult(u8 *q,
......@@ -100,10 +156,6 @@ int crypto_scalarmult(u8 *q,
}
\end{lstlisting}
It should be noted that this representation does not guaranties uniqueness. i.e.\\
$\exists x,y \in \texttt{gf} \text{ such that }$
\vspace{-0.25cm}
$$x \neq y\ \ \land\ \ x \equiv y \pmod{2^{255}-19}$$
\subsection{What need to be proven?}
......
\section{Number representation and C implementation}
\subsection{Reflection and Inversions}
\begin{lstlisting}
\end{lstlisting}
......@@ -7,6 +7,7 @@
\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
Add comparison with Fiat-crypto
......@@ -21,6 +21,20 @@ $
\item \textbf{\texttt{clightgen}} translation from \textbf{C} to
\textbf{Clight}.
VST does not support the verification of
\texttt{o[i] = a[i] + b[i]}, the \texttt{forward} tactic will simply not work.
This required us to rewrite the lines into:\\
\texttt{aux1 = a[i];\\
aux2 = b[i];\\
o[i] = aux1 + aux2;}. This rewriting is done
The trust of the proof relied on the trust of a correct translation from the
initial version of \textit{TweetNaCl} to \textit{TweetNaclVerificable}.
While this problem is still present, the Compcert developpers provided us with
the \texttt{-normalize} option for \texttt{clightgen} which takes care of
generating auxiliary variables in order to automatically derive these steps.
The changes required for a C-code to make it Verifiable are now minimals.
\item The \textbf{Coq kernel}, the \textbf{Ocaml compiler},
the \textbf{Ocaml Runtime} and the \textbf{CPU}. These are common to all proofs
......@@ -30,13 +44,13 @@ $
\subsection{Aliasing and Memory collision}
Necessity to go back into your specification multiple times to refine your model.
e.g. prove \texttt{M(o,a,b)} later notice that you can have aliasing, need to redifine
e.g. prove \texttt{M(o,a,b)} later notice that you can have aliasing, need to redefine
your theorem to prove \texttt{M(o,a,a)} (\textit{squaring}) and other variants such as:
\texttt{M(a,a,b)} and \texttt{M(b,a,b)}.
\begin{figure}[h]
\include{tikz/memory_same_sh}
\caption{Aliasing and Separation Logic (1)}
\caption{Aliasing and Separation Logic}
\label{tk:MemSame}
\end{figure}
......@@ -44,11 +58,11 @@ Prove \texttt{M(o,a,b)} where o is a \texttt{list $\Z$} and then realize that
\texttt{o} can be a list of \textit{undefined} (\texttt{list val}). Thus needs
to reprove the above theorem again.
\begin{figure}[h]
\include{tikz/memory_diff_sh}
\caption{Memory Share and Separation Logic}
\label{tk:MemSame}
\end{figure}
% \begin{figure}[h]
% \include{tikz/memory_diff_sh}
% \caption{Memory Share and Separation Logic}
% \label{tk:MemSame}
% \end{figure}
\subsection{How to be efficient with VST?}
......@@ -73,19 +87,7 @@ Three years ago:
\subsection{Pointers arithmetic, arrays and types}
VST does not support the verification of \texttt{o[i] = a[i] + b[i]},
the \texttt{forward} tactic will simply not work. This initially required us to
rewrite the lines into:\\
\texttt{aux1 = a[i];\\
aux2 = b[i];\\
o[i] = aux1 + aux2;}\\
The trust of the proof relied on the trust of a correct translation from the
initial version of \textit{TweetNaCl} to \textit{TweetNaclVerificable}.
While this problem is still present, the Compcert developpers provided us with
the \texttt{-normalize} option for \texttt{clightgen} which takes care of
generating auxiliary variables in order to automatically derive these steps.
The changes required for a C-code to make it Verifiable are now minimals.
It is to be noted that the \texttt{clightgen} tool has not been formally verified.
......
......@@ -20,6 +20,21 @@
publisher = {ACM}
}
INPROCEEDINGS{Reynolds02separationlogic:,
author = {John C. Reynolds},
title = {Separation logic: A logic for shared mutable data structures},
}
@article{Reynolds02separationlogic,
author = {John C. Reynolds},
title = {Separation Logic: A Logic for Shared Mutable Data Structures},
journal = {LICS},
volume = {17},
year = {2002},
pages = {55-74},
note = {\url{http://www.cs.cmu.edu/~jcr/seplogic.pdf}},
url = {http://www.cs.cmu.edu/~jcr/seplogic.pdf}
}
@article{2007-Blazy-C-chronique,
author = {Sandrine Blazy},
title = {Comment gagner confiance en {C} ?},
......@@ -74,6 +89,19 @@
note = {Document ID: c74b5bbf605ba02ad8d9e49f04aca9a2, \url{http://cryptojedi.org/papers/\#tweetnacl}},
}
@inproceedings{ BLS12,
author = {Daniel J. Bernstein and Tanja Lange and Peter Schwabe},
title = {The security impact of a new cryptographic library},
booktitle = {Progress in Cryptology -- {LATINCRYPT 2012}},
editor = {Alejandro Hevia and Gregory Neven},
publisher = SV,
series = LNCS,
volume = {7533},
year = {2012},
pages = {159--176},
note = {Document ID: 5f6fc69cc5a319aecba43760c56fab04, \url{http://cryptojedi.org/papers/\#coolnacl}},
}
VeriSmall: Verified Smallfoot Shape Analysis, by Andrew W. Appel. In CPP 2011: First International Conference on Certified Programs and Proofs, Springer LNCS 7086, pp. 231-246, December 2011.
@inproceedings{2012-Appel,
......
......@@ -38,7 +38,7 @@
\date{}
%make title bold and 14 pt font (Latex default is non-bold, 16 pt)
\title{\Large \bf Proving the complete correctness of TweetNaCl's Curve25519 implementation.%
\title{\Large \bf A Coq proof of Tweetnacl's Curve25519 correctness.%
\thanks{
Date: somewhen in 2018.}
}
......@@ -48,15 +48,12 @@ Date: somewhen in 2018.}
\author{
{\rm Peter Schwabe}\\
Radboud University, The Netherlands\\
%\~\\
\and
{\rm Beno\^it Viguier}\\
Radboud University, The Netherlands\\
%\~\\
\and
{\rm Timmy Weerwag}\\
Radboud University, The Netherlands\\
%\~\\
\and
{\rm Freek Wiedijk}\\
Radboud University, The Netherlands\\
......@@ -67,10 +64,7 @@ Date: somewhen in 2018.}
%\thispagestyle{empty}
\subsection*{Abstract}
By using the Coq formal proof assistant with the VST library, we prove the
soundness and correctness of TweetNaCl's Curve25519 implementation.
\input{0_Abstract.tex}
\input{1_Introduction.tex}
\input{2_Implementation.tex}
\input{3_Maths.tex}
......@@ -85,5 +79,4 @@ soundness and correctness of TweetNaCl's Curve25519 implementation.
\begin{appendix}
\end{appendix}
\end{document}
......@@ -27,6 +27,8 @@
%\usepackage{varioref}
\usepackage{hyperref}
\RequirePackage{tikz}
% \usetikzlibrary{shapes.arrows}
\usetikzlibrary{arrows}
\usepackage{ctable}
\usepackage{cite}
......@@ -169,8 +171,9 @@ width=0.8\columnwidth
morekeywords=[2]{sv, int, i64, gf, long, u8},
morekeywords=[3]{const, typedef},
morekeywords=[4]{A, Z, M, S, car25519, pack25519, inv25519,
crypto_scalarmult, unpack25519, sel25519},
morekeywords=[5]{ 0, 1, 1LL, 3, 7, 15, 16, 31, 32, 37, 38, 127, 64, 248, 254,_121665 },
crypto_scalarmult, unpack25519, sel25519, set25519},
morekeywords=[5]{ 0, 1, 1LL, 2, 3, 4, 7, 8, 14, 15, 16, 31, 32, 37, 38, 127, 64,
248, 254, _121665, 0x7fff, 0xffed, 0xffff, 0xff },
sensitive=true,
alsoletter = {0123456789^} ,
% morekeywords = [1]{1,2,3,40} ,
......
# Proving the complete correctness of TweetNaCl's Curve25519 implementation
**Abstract**:
By using the Coq formal proof assistant with the VST library, we prove the
soundness and correctness of TweetNaCl's Curve25519 implementation.
## Introduction
Implementing cryptographic primitives without any bugs is hard. While tests
provides a decent code coverage, they don't cover 100% of the possible values.
## Curve25519 implementation
### Implementation
256 bits words are cute into limbs of 16 bits placed into 64 bits signed
containers (`long long`).
void A(o,a,b):
int i;
for(i = 0 ; i < 16; ++i)
o[i] = a[i] + b[i]
void M(o,a,b):
int i, j;
long long[31] t;
for(i = 0 ; i < 31; ++i)
t[i]=0;
for(i = 0 ; i < 16; ++i)
for(j = 0 ; j < 16; ++j)
t[i+j] = a[i] * b[j] + t[i+j]
for(i = 0; i < 15; ++i)
t[i] = 38 * t[i+16]
for(i = 0 ; i < 16 ; ++ i)
o[i] = t[i]
car25519(o)
car25519(o)
void car25519(o)
for(i = 0 ; i < 15 ; ++i)
c = o[i] >> 16
o[i+1] += c
o[i] -= c << 16
c = o[15] >> 16
o[0] += 38*c
o[15] -= c << 16
### What to prove?
**Soundness**
- absence of array out-of-bounds
for each array access, VST requires to prove the range.
- absence of overflows/underflow
for each operation, VST requires to prove that the resulting value are in ranges.
This is *shape analysis*.
**Correctness**
- Curve25519 is correctly implemented
- The number representation
### Correctness Theorem
## Mathematical Model
ASK TIMMY
## Number representation and C implementation
## Related Works
- HACL*
- Proving SHA-256 and HMAC
- http://www.iis.sinica.edu.tw/~bywang/papers/ccs17.pdf
- http://www.iis.sinica.edu.tw/~bywang/papers/ccs14.pdf
- https://cryptojedi.org/crypto/#gfverif
- https://cryptojedi.org/crypto/#verify25519
## Using VST
This approach is **slow**, **tedious** and **frustrating**.
The time cost way to big for such a proof and definitively not applicable for a
cryptographic engineer.
Two years ago:
https://www.imperialviolet.org/2014/09/11/moveprovers.html
https://www.imperialviolet.org/2014/09/07/provers.html
\begin{tikzpicture}
\def\-{\raisebox{.75pt}{-}}
\draw (0,0) rectangle (3,0.3);
\draw[thick] (1,0) -- (1,0.3);
......@@ -16,7 +15,7 @@
$\mathtt{sh [\!\!\{ v\_b \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ b}$}};
\begin{scope}[yshift=0 cm,xshift=4 cm]
\begin{scope}[yshift=0 cm,xshift=4.5 cm]
\draw (0,0) rectangle (2,0.3);
\draw[thick] (1,0) -- (1,0.3);
% \draw[thick] (2,0) -- (2,0.3);
......@@ -35,4 +34,29 @@
\draw[dashed] (-0.5,-1.2) -- +(7.5,0);
\node [anchor=north west] (sep) at (-0.5,-1.2) {In Separation Logic:};
\begin{scope}[yshift=-5 cm,xshift=2 cm]
\draw (0,0) rectangle (2,0.3);
\draw[thick] (1,0) -- (1,0.3);
\node [anchor=east] (shm) at (0,0.15) {sh\;};
\draw (0,0.5) rectangle (1,0.8);
\node [anchor=east] (shm) at (0,0.65) {Ews};
\draw[thick] (2,0) -- (2,0.3);
\node [anchor=north west] (Mcaa) at (0.15,-0.5) {\texttt{M(a,c,\_121665)}};
\draw[thick, -> ] (0.75, -0.6) -- (0.75, -0.5) -- (0.5,-0.1);
\draw[thick, -> ] (1.1, -0.6) -- (1.1, -0.5) -- (1.5,-0.1);
\draw[thick, -> ] (2.0, -0.6) -- (2.45, -0.2) -- (2.45, 0.3) -- (2.2, 0.65) -- (1.5,0.65);
\node [anchor=north west, text width=6cm, align=left] (Sepoab) at (-0.5,-1.8)
{\footnotesize{$\mathtt{sh [\!\!\{ v\_a \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ a}$\\
$\mathtt{sh [\!\!\{ v\_c \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ c}$\\
$\mathtt{Ews} \mathtt{[\!\!\{ \_\_121665 \}\!\!]\ \textrm{<\!--(}lg16\textrm{)--}\ \_121665}$}};
\end{scope}
\draw[dashed] (0.5,-6.2) -- +(6,0);
\node [anchor=north west] (sep) at (0.5,-6.2) {In Separation Logic:};
\end{tikzpicture}
\begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center}]
\filldraw[draw=orange!10!doc@lstbackground, fill=doc@lstbackground, thick] (0.25,0.5) rectangle (4.5,5.5);
% node[textstyle, anchor=west, draw=yellow, fill=yellow!20, thick, minimum width=5.5cm,minimum height=5cm] {};
\draw (4.5,5.5) node[anchor=north east, inner sep=0pt] (russell) {\includegraphics[width=.03\textwidth]{img/coq_logo.png}};
\draw (0.5,-1) node [textstyle, anchor=west, draw=black, thick, minimum width=3cm,minimum height=0.5cm] (longlong) {\texttt{long long[16]}};
\draw (0,-1) node [anchor=east] (longlongdef) {\texttt{C} code};
\draw (2.25,-0.1) node [anchor=west] (app) {\texttt{clightgen}};
\draw (0.5,1) node [textstyle, anchor=west, draw=black, thick, minimum width=3cm,minimum height=0.5cm] (clight) {\texttt{tptr tlong}};
\draw (0,1) node [anchor=east] (clightdef) {\texttt{CLight}};
\draw [thick, ->] (longlong.north) -- (clight.south);
\begin{scope}[yshift=1 cm,xshift=0 cm]
\draw (0.5,2) node [textstyle, anchor=west, draw=black, thick, minimum width=3cm,minimum height=0.5cm] (ll) {\texttt{list} $\mathbb{Z}$};
\draw (0,2) node [anchor=east] (shn) {Low Level};
\draw [thick,double, <->, >=implies] (clight.north) -- (ll.south);
\draw (2.25,1) node[anchor=west, inner sep=0pt] (chain) {\includegraphics[width=.07\textwidth]{img/chain.png}};
\draw (0.5,3) node [textstyle, anchor=west, draw=black, thick, minimum width=3cm,minimum height=0.5cm] (ml) {$\mathbb{Z}_{2^{255}-19}$};
\draw (0,3) node [anchor=east] (shn) {Mid Level};
\draw[thick,double, <->, >=implies] (ll.north) -- (ml.south);
\draw (0.5,4) node [textstyle, anchor=west, draw=black, thick, minimum width=3cm,minimum height=0.5cm] (hl) {$\mathbb{F}$};
\draw (0,4) node [anchor=east] (shn) {High Level};
\draw[thick,double, <-, >=implies] (ml.north) -- (hl.south);
\end{scope}
\end{tikzpicture}
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