Commit 4dc57fba authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more text

parent e77c9685
This diff is collapsed.
......@@ -30,7 +30,8 @@ Lemma f_ext: forall (A B:Type),
the project we found inconsistency and reported them to the authors.
\item \textbf{CompCert}. The formally proven compiler. We trust that the Clight
model captures correctly the C standard. (VERIFY THIS, WHICH STANDARD ?).
model captures correctly the C standard.
\todo{VERIFY THIS, WHICH STANDARD ?}.
Our proof also assumes that the TweetNaCl code will behave as expected if
compiled under CompCert. We do not provide garantees for other C compilers
such as Clang or GCC.
......
\section{Proving equivalence of X25519 in C and Coq}
\label{C-Coq}
In this section we describe techniques used to prove the equivalence between the
In this section we first describe the global structure of our proof.
Then we discuss techniques used to prove the equivalence between the
Clight description of TweetNaCl and Coq functions producing similar behaviors.
\subsection{One proof? No, two!}
\todo{SUBSECTION?}
In order to prove the correctness of X25519, we use VST to prove that TweetNaCl's code
matches our functional specification of \texttt{crypto\_scalarmult} (abreviated as CSM) in Coq.
Then we prove that our specification of the scalar multiplication matches the
mathematical definition of elliptic curves and Theorem 2.1 by Bernstein~\cite{Ber06}.
Figure~\ref{tk:ProofOverview} shows a graph of dependencies of the proofs considered.
The mathematical proof of our specification is presented in Section~\ref{sec3-maths}.
\begin{figure}[h]
\centering
\include{tikz/proof}
\caption{Overview construction of the proof}
\caption{Overview of the proof}
\label{tk:ProofOverview}
\end{figure}
......@@ -184,7 +192,7 @@ We also define a notation to do the modulo, projecting any numbers in $\Zfield$.
\begin{lstlisting}[language=Coq]
Notation "A :GF" := (A mod (2^255-19)).
\end{lstlisting}
Remark that this representation is different from \Coqe{Zmodp}.
% Remark that this representation is different from \Coqe{Zmodp}.
However the equivalence between operations over $\Zfield$ and $\F{p}$ is easily proven.
Using these two definitions, we proved intermediates lemmas such as the correctness of the
......@@ -477,7 +485,7 @@ ZofList 8 (Pack25519 l) = (Z16.lst l) mod (2^255-19).
\end{Coq}
\subsection{Using the Verifiable Software Toolchain}
\label{using-VST}
The Verifiable Software Toolchain uses a strongest postcondition strategy.
The user must first write a formal specification of the function he wants to verify in Coq.
This should be as close as possible to the C implementation behavior.
......
......@@ -24,7 +24,8 @@ scalar multiplication of $P$ by $n$. Note that the result would is the same with
Using X25519, RFC~7748~\cite{rfc7748} formalized a Diffie–Hellman key-exchange algorithm.
Each party generate a secret random number $S_a$ (respectively $S_b$), and computes $P_a$ (respectively $P_b$),
the $x$-coordinate of the scalar multiplication of the base point where $x = 9$ and $S_a$ (respectively $S_b$).
the resulting $x$-coordinate of the scalar multiplication of the base point
where $x = 9$ and $S_a$ (respectively $S_b$).
The party exchanges $P_a$ and $P_b$ and computes their shared secret with X25519
over $S_a$ and $P_b$ (respectively $S_b$ and $P_a$).
......@@ -207,14 +208,27 @@ int crypto_scalarmult(u8 *q,
Coq~\cite{coq-faq} is an interactive theorem prover. It provides an expressive
formal language to write mathematical definitions, algorithms and theorems coupled
with their proofs. As opposed to other systems such as F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
Coq does not use a SMT solver to discharge its proof obligations but requires
the user to specify exactly which lemmas, hypothesis to apply and uses its type
system to verify their application~\cite{Howard1995-HOWTFN}.
It also provides some automations tools so that the user can apply and try multiple
proofs techniques in an efficient manner.
The Verified Software Toolchain is \cite{cao2018vst-floyd}.
\todo{Describe Hoare Logic}
\todo{Describe Separation Logic}
Coq does not rely on the trust ofa SMT solver. It uses its type
system to verify the applications of hypothesis, lemmas , theorems~\cite{Howard1995-HOWTFN}.
The Hoare logic is a formal system which allows to reason about programs.
It uses tripples such as
$$\{{\color{doc@lstnumbers}\textbf{Pre}}\}\texttt{~Prog~}\{{\color{doc@lstdirective}\textbf{Post}}\}$$
where ${\color{doc@lstnumbers}\textbf{Pre}}$ and ${\color{doc@lstdirective}\textbf{Post}}$
are assertions and \texttt{Prog} is a piece of Code.
It is read as ``when the precondition $Pre$ is met, executing \texttt{Prog} while yield to postcondition $Post$''.
We use compositional rules to prove the truth value of a Hoare tripple.
For example, here is the rule for sequential composition:
\begin{prooftree}
\AxiomC{$\{P\}C_1\{Q\}$}
\AxiomC{$\{Q\}C_2\{R\}$}
\LeftLabel{Hoare-Seq}
\BinaryInfC{$\{P\}C_1;C_2\{R\}$}
\end{prooftree}
Separation Logic is an extension of the Hoare logic which allows to reason about
pointers and memory manipulation. This provides the strict condition that considered
memory shares are disjoint, forcing non-aliasing. We discuss further about this limitation in Section~\ref{using-VST}.
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework which uses
the Separation logic to prove the functional correctness of C programs.
Its can be seen as a forward symbolic execution of the program.
Its uses a strongest postcondition approach to prove that a code matches its specification.
......@@ -17,6 +17,7 @@
\usepackage{multirow}
\usepackage{ntheorem}
\usepackage{textcomp}
\usepackage{bussproofs}
\RequirePackage{xcolor}
\definecolor{linkcolor}{rgb}{0.65,0,0}
......
\begin{tikzpicture}[textstyle/.style={black, anchor= south west, align=center, minimum height=0.45cm, text centered, font=\scriptsize}]
% adapt line thickness and line width, if needed
\tikzstyle{vecArrow} = [thick, decoration={markings,mark=at position
1 with {\arrow[semithick]{open triangle 60}}},
double distance=1.4pt, shorten >= 5.5pt,
preaction = {decorate},
postaction = {draw,line width=1.4pt, white,shorten >= 4.5pt}]
% C code
\begin{scope}[yshift=0 cm,xshift=0 cm]
\draw (0,0) -- (0.4, 0.4) -- (1.25,0.4) -- (1.25,0) -- cycle;
......@@ -66,11 +74,11 @@
\draw (1.25,-0.75) node[textstyle, anchor=center] {{\color{doc@lstnumbers}\textbf{Pre}} $\implies$\\$\text{\texttt{CSM}}(n,P) = [n]P$};
\end{scope}
\draw [very thick, ->] (1.25,-0.5) -- (2.5, -0.5);
\draw [very thick, ->] (3.75,-0.5) -- (6, -0.5);
\draw [very thick, ->] (5,-3.5) -- (6.5, -1.25);
\draw [very thick, ->] (2,-5) -- (3, -3.5);
\draw [very thick, ->] (2,-5) -- (6, -7);
\draw [very thick, ->] (2,-7.5) -- (6, -7.5);
\path [thick, double, ->] (1.25,-0.5) edge (2.5, -0.5);
\path [thick, double, ->] (3.75,-0.5) edge (6, -0.5);
\path [thick, double, ->] (5,-3.5) edge [out=0, in=-90] (6.5, -1.25);
\path [thick, double, ->] (2,-5) edge [out=0, in=-180] (3, -3.5);
\path [thick, double, ->] (2,-5) edge [out=0, in=-180] (6, -7);
\path [thick, double, ->] (2,-7.5) edge [out=0, in=-180] (6, -7.5);
\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