Commit 131dd1a6 authored by benoit's avatar benoit
Browse files

space reduction = 16 pages

parent 52a0a42c
...@@ -4,11 +4,11 @@ SOURCES= code-tweetnacl.tex collection.bib conclusion.tex coq.tex highlevel.tex ...@@ -4,11 +4,11 @@ SOURCES= code-tweetnacl.tex collection.bib conclusion.tex coq.tex highlevel.tex
PREVIOUS= csf-supplementary/previous.tex csf-supplementary/usenix-*.tex csf-supplementary/tweetverif-USENIX.pdf csf-supplementary/tweetverif-SP.pdf PREVIOUS= csf-supplementary/previous.tex csf-supplementary/usenix-*.tex csf-supplementary/tweetverif-USENIX.pdf csf-supplementary/tweetverif-SP.pdf
tweetverif.pdf: $(SOURCES) tweetverif.pdf: $(SOURCES)
latex ./latexrun.py tweetverif.tex
pdflatex tweetverif.tex # pdflatex tweetverif.tex
bibtex tweetverif # bibtex tweetverif
pdflatex tweetverif.tex # pdflatex tweetverif.tex
pdflatex tweetverif.tex # pdflatex tweetverif.tex
csf-supplementary/previous.pdf: $(PREVIOUS) csf-supplementary/previous.pdf: $(PREVIOUS)
make -C csf-supplementary make -C csf-supplementary
......
...@@ -35,6 +35,6 @@ As follow, we provide the explanations of the above changes to TweetNaCl's code. ...@@ -35,6 +35,6 @@ As follow, we provide the explanations of the above changes to TweetNaCl's code.
\item lines 79-82: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.\\ \item lines 79-82: VST does not support \TNaCle{for} loops over \TNaCle{i64}, we convert it into an \TNaCle{int}.\\
In the function calls of \TNaCle{sel25519}, the specifications requires the use of \TNaCle{int}, the value of \TNaCle{r} being either \TNaCle{0} or \TNaCle{1}, we consider this change safe. In the function calls of \TNaCle{sel25519}, the specifications requires the use of \TNaCle{int}, the value of \TNaCle{r} being either \TNaCle{0} or \TNaCle{1}, we consider this change safe.
\item Lines 90-101: The \TNaCle{for} loop does not add any benefits to the code. By removing it we simplify the source and the verification steps as we do not need to deal with pointer arithmetic. As a result, \TNaCle{x} can be limited to only 16 \TNaCle{i64}, \ie \TNaCle{gf}. \item Lines 90-101: The \TNaCle{for} loop does not add any benefits to the code. By removing it we simplify the source and the verification steps as we do not need to deal with pointer arithmetic. Thus, \TNaCle{x} is limited to only 16 \TNaCle{i64}, \ie \TNaCle{gf}.
\end{itemize} \end{itemize}
...@@ -15,11 +15,11 @@ In our case we rely on: ...@@ -15,11 +15,11 @@ In our case we rely on:
used by Coq must be consistent in order to trust the proofs. As an axiom, used by Coq must be consistent in order to trust the proofs. As an axiom,
we assume that the functional extensionality is also consistent with that logic. we assume that the functional extensionality is also consistent with that logic.
$$\forall x, f(x) = g(x) \implies f = g$$ $$\forall x, f(x) = g(x) \implies f = g$$
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] % \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Lemma f_ext: forall (A B:Type), % Lemma f_ext: forall (A B:Type),
forall (f g: A -> B), % forall (f g: A -> B),
(forall x, f(x) = g(x)) -> f = g. % (forall x, f(x) = g(x)) -> f = g.
\end{lstlisting} % \end{lstlisting}
\item \textbf{Verifiable Software Toolchain}. This framework developed at \item \textbf{Verifiable Software Toolchain}. This framework developed at
Princeton allows a user to prove that a Clight code matches pure Coq Princeton allows a user to prove that a Clight code matches pure Coq
...@@ -165,3 +165,4 @@ mathematical definitions as given in~\cite[Sec.~2]{Ber06}. ...@@ -165,3 +165,4 @@ mathematical definitions as given in~\cite[Sec.~2]{Ber06}.
Therefore in addition to proving the mathematical correctness of TweetNaCl, Therefore in addition to proving the mathematical correctness of TweetNaCl,
we also increases the trust of other works such as we also increases the trust of other works such as
\cite{zinzindohoue2017hacl,Erbsen2016SystematicSO} which rely on RFC~7748. \cite{zinzindohoue2017hacl,Erbsen2016SystematicSO} which rely on RFC~7748.
\vspace{-0.3cm}
\ No newline at end of file
...@@ -3,7 +3,6 @@ ...@@ -3,7 +3,6 @@
\subsection{Montgomery Ladder} \subsection{Montgomery Ladder}
\label{subsubsec:coq-ladder} \label{subsubsec:coq-ladder}
~
Generic definition of the ladder: Generic definition of the ladder:
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
...@@ -91,7 +90,6 @@ end. ...@@ -91,7 +90,6 @@ end.
\subsection{RFC in Coq} \subsection{RFC in Coq}
\label{subsubsec:RFC-Coq} \label{subsubsec:RFC-Coq}
~
Instantiation of the Class \Coqe{Ops} with operations over \Z and modulo \p. Instantiation of the Class \Coqe{Ops} with operations over \Z and modulo \p.
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Definition modP (x:Z) : Z := Definition modP (x:Z) : Z :=
......
...@@ -48,6 +48,7 @@ $a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref ...@@ -48,6 +48,7 @@ $a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref
\begin{figure}[h] \begin{figure}[h]
\centering \centering
\include{tikz/highlevel1} \include{tikz/highlevel1}
\vspace{-0.5cm}
\caption{Overview of the proof of Montgomery ladder's correctness} \caption{Overview of the proof of Montgomery ladder's correctness}
\label{tikz:ProofHighLevel1} \label{tikz:ProofHighLevel1}
\end{figure} \end{figure}
...@@ -193,13 +194,13 @@ After having verified the group properties, it follows that the bijection is a g ...@@ -193,13 +194,13 @@ After having verified the group properties, it follows that the bijection is a g
\begin{lemma} \begin{lemma}
\label{lemma:bij-ecc} \label{lemma:bij-ecc}
Let $M_{a,b}$ be a Montgomery curve, define Let $M_{a,b}$ be a Montgomery curve, define
%\vspace{-0.3em} \vspace{-0.3em}
$$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$ $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$
then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping
$\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as: $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as:
%\vspace{-0.5em} \vspace{-0.5em}
\begin{align*} \begin{align*}
\varphi(\Oinf_M) & = \Oinf_E \\ \varphi(\Oinf_M) & = \Oinf_E \\[-0.5ex]
\varphi( (x , y) ) & = \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right) \varphi( (x , y) ) & = \left( \frac{x}{b} + \frac{a}{3b} , \frac{y}{b} \right)
\end{align*} \end{align*}
is a group isomorphism between elliptic curves. is a group isomorphism between elliptic curves.
...@@ -255,7 +256,7 @@ Hypothesis mcu_no_square : ...@@ -255,7 +256,7 @@ Hypothesis mcu_no_square :
We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve. We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
\begin{dfn} \begin{dfn}
Let $\chi : M_{a,b}(\K) \mapsto \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \mapsto \K$ such that Let $\chi : M_{a,b}(\K) \mapsto \K \cup \{\infty\}$ and $\chi_0 : M_{a,b}(\K) \mapsto \K$ such that
%\vspace{-0.5em} \vspace{-0.5em}
\begin{align*} \begin{align*}
\chi((x,y)) & = x, & \chi(\Oinf) & = \infty, & & \text{and} \\[-0.5ex] \chi((x,y)) & = x, & \chi(\Oinf) & = \infty, & & \text{and} \\[-0.5ex]
\chi_0((x,y)) & = x, & \chi_0(\Oinf) & = 0. \chi_0((x,y)) & = x, & \chi_0(\Oinf) & = 0.
...@@ -269,7 +270,7 @@ Using projective coordinates we prove the formula for differential addition.% (\ ...@@ -269,7 +270,7 @@ Using projective coordinates we prove the formula for differential addition.% (\
let $X_1, Z_1, X_2, Z_2, X_4, Z_4 \in \K$, such that $(X_1,Z_1) \neq (0,0)$, let $X_1, Z_1, X_2, Z_2, X_4, Z_4 \in \K$, such that $(X_1,Z_1) \neq (0,0)$,
$(X_2,Z_2) \neq (0,0)$, $X_4 \neq 0$ and $Z_4 \neq 0$. $(X_2,Z_2) \neq (0,0)$, $X_4 \neq 0$ and $Z_4 \neq 0$.
Define Define
%\vspace{-0.5em} \vspace{-0.5em}
\begin{align*} \begin{align*}
X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2 \\[-0.5ex] X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2 \\[-0.5ex]
Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2 Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2
...@@ -287,8 +288,8 @@ Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}). ...@@ -287,8 +288,8 @@ Similarly, we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
let $X_1, Z_1 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define let $X_1, Z_1 \in \K$, such that $(X_1,Z_1) \neq (0,0)$. Define
\begin{align*} \begin{align*}
c & = (X_1 + Z_1)^2 - (X_1 - Z_1)^2 \\ c & = (X_1 + Z_1)^2 - (X_1 - Z_1)^2 \\[-0.5ex]
X_3 & = (X_1 + Z_1)^2(X_1-Z_1)^2 \\ X_3 & = (X_1 + Z_1)^2(X_1-Z_1)^2 \\[-0.5ex]
Z_3 & = c\Big((X_1 + Z_1)^2+\frac{a-2}{4}\times c\Big), Z_3 & = c\Big((X_1 + Z_1)^2+\frac{a-2}{4}\times c\Big),
\end{align*} \end{align*}
then for any point $P_1$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1)$, then for any point $P_1$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1)$,
...@@ -355,6 +356,7 @@ The white tiles are definitions while green tiles are important lemmas and theor ...@@ -355,6 +356,7 @@ The white tiles are definitions while green tiles are important lemmas and theor
\begin{figure}[h] \begin{figure}[h]
\centering \centering
\include{tikz/highlevel2} \include{tikz/highlevel2}
\vspace{-0.5cm}
\caption{Proof dependencies for the correctness of X25519.} \caption{Proof dependencies for the correctness of X25519.}
\label{tikz:ProofHighLevel2} \label{tikz:ProofHighLevel2}
\end{figure} \end{figure}
...@@ -514,12 +516,12 @@ We then specialize the basic operations in order to speed up the verification ...@@ -514,12 +516,12 @@ We then specialize the basic operations in order to speed up the verification
of formulas by using rewrite rules: of formulas by using rewrite rules:
\begin{equation*} \begin{equation*}
\begin{split} \begin{split}
(a,0) + (b,0) &= (a+b, 0)\\ (a,0) + (b,0) &= (a+b, 0)\\[-0.5ex]
(a, 0)^{-1} &= (a^{-1}, 0) (a, 0)^{-1} &= (a^{-1}, 0)
\end{split} \end{split}
\qquad \qquad
\begin{split} \begin{split}
(a,0) \cdot (b,0) &= (a \cdot b, 0)\\ (a,0) \cdot (b,0) &= (a \cdot b, 0)\\[-0.5ex]
(0,a)^{-1} &= (0,(2\cdot a)^{-1}) (0,a)^{-1} &= (0,(2\cdot a)^{-1})
\end{split} \end{split}
\end{equation*} \end{equation*}
...@@ -558,16 +560,16 @@ We now study the case of the scalar multiplication and show similar proofs. ...@@ -558,16 +560,16 @@ We now study the case of the scalar multiplication and show similar proofs.
\label{lemma:proj} \label{lemma:proj}
For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve
$M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have
%\vspace{-0.3em} \vspace{-0.3em}
\begin{align*} \begin{align*}
P & \in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) & = n \cdot \varphi_c(P), & & \text{and} \\ P & \in M_{486662,1}(\F{p}) & \implies \varphi_c(n \cdot P) & = n \cdot \varphi_c(P), & & \text{and} \\[-0.5ex]
P & \in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) & = n \cdot \varphi_t(P). P & \in M_{486662,2}(\F{p}) & \implies \varphi_t(n \cdot P) & = n \cdot \varphi_t(P).
\end{align*} \end{align*}
\end{lemma} \end{lemma}
Notice that Notice that
%\vspace{-0.5em} \vspace{-0.5em}
\begin{align*} \begin{align*}
\forall P \in M_{486662,1}(\F{p}), & & \psi(\chi_0(\varphi_c(P))) & = \chi_0(P), & & \text{and} \\ \forall P \in M_{486662,1}(\F{p}), & & \psi(\chi_0(\varphi_c(P))) & = \chi_0(P), & & \text{and} \\[-0.5ex]
\forall P \in M_{486662,2}(\F{p}), & & \psi(\chi_0(\varphi_t(P))) & = \chi_0(P). \forall P \in M_{486662,2}(\F{p}), & & \psi(\chi_0(\varphi_t(P))) & = \chi_0(P).
\end{align*} \end{align*}
......
This diff is collapsed.
...@@ -163,6 +163,7 @@ Examples of such cases are illustrated in \fref{tikz:MemSame}. ...@@ -163,6 +163,7 @@ Examples of such cases are illustrated in \fref{tikz:MemSame}.
\begin{figure}[h]% \begin{figure}[h]%
\centering% \centering%
\include{tikz/memory_same_sh}% \include{tikz/memory_same_sh}%
\vspace{-0.5cm}
\caption{Aliasing and Separation Logic}% \caption{Aliasing and Separation Logic}%
\label{tikz:MemSame}% \label{tikz:MemSame}%
\end{figure} \end{figure}
...@@ -181,19 +182,19 @@ In the proof of our specification, we do a case analysis over $k$ when needed. ...@@ -181,19 +182,19 @@ In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all the possible cases of aliasing over 3 pointers This solution does not cover all the possible cases of aliasing over 3 pointers
(\eg \texttt{o} = \texttt{a} = \texttt{b}) but it is enough to satisfy our needs. (\eg \texttt{o} = \texttt{a} = \texttt{b}) but it is enough to satisfy our needs.
\subheading{Improving verification speed.} % \subheading{Improving verification speed.}
To make the verification the smoothest, the Coq formal definition of the function % To make the verification the smoothest, the Coq formal definition of the function
should be as close as possible to the C implementation. % should be as close as possible to the C implementation.
Attempting to write definitions more ``elegantly'', for example through the extensive % Attempting to write definitions more ``elegantly'', for example through the extensive
use of recursion, is often counter-productive because such definitions increase the % use of recursion, is often counter-productive because such definitions increase the
amount of proofs required for, \eg bounds checking or loop invariants. % amount of proofs required for, \eg bounds checking or loop invariants.
In order to further speed-up the verification process, to prove the specification % In order to further speed-up the verification process, to prove the specification
\TNaCle{crypto_scalarmult}, we only need the specification of the subsequently % \TNaCle{crypto_scalarmult}, we only need the specification of the subsequently
called functions (\eg \TNaCle{M}). % called functions (\eg \TNaCle{M}).
This provide with multiple advantages: the verification by Coq can be % This provide with multiple advantages: the verification by Coq can be
done in parallel and multiple users can work on proving different functions at % done in parallel and multiple users can work on proving different functions at
the same time. % the same time.
% We proved all intermediate functions. % We proved all intermediate functions.
......
...@@ -47,7 +47,7 @@ $(X : Z)$, with $x = X/Z$; the point at infinity is represented as $(1:0)$. ...@@ -47,7 +47,7 @@ $(X : Z)$, with $x = X/Z$; the point at infinity is represented as $(1:0)$.
See \sref{subsec:ECC-projective} for more details. See \sref{subsec:ECC-projective} for more details.
We define the operation: We define the operation:
\begin{align*} \begin{align*}
\texttt{xDBL\&ADD} & : (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\ \texttt{xDBL\&ADD} & : (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\[-0.5ex]
& ((X_{2 \cdot P}:Z_{2 \cdot P}), (X_{P + Q}:Z_{P + Q})) & ((X_{2 \cdot P}:Z_{2 \cdot P}), (X_{P + Q}:Z_{P + Q}))
\end{align*} \end{align*}
......
...@@ -17,15 +17,14 @@ The actual proofs can be found in the \textbf{\texttt{proofs}} folder in which ...@@ -17,15 +17,14 @@ The actual proofs can be found in the \textbf{\texttt{proofs}} folder in which
the reader will find the directories \textbf{\texttt{spec}} and \textbf{\texttt{vst}}. the reader will find the directories \textbf{\texttt{spec}} and \textbf{\texttt{vst}}.
\subheading{\texttt{packages/}} \subheading{\texttt{packages/}}
This folder makes sure that we are using the correct version of This folder provides all the required Coq dependencies: ssreflect (1.7),
Verifiable Software Toolchain (version 2.0) and CompCert (version 3.2). VST (2.0), CompCert (3.2), the elliptic curves library by Bartzia \& Strub,
Additionally it pins the version of the elliptic curves library by Bartzia and Strub and the theorem of quadratic reciprocity.
and allows us to use the theorem of quadratic reciprocity.
\subheading{\texttt{proofs/spec/}} \subheading{\texttt{proofs/spec/}}
In this folder the reader will find multiple levels of implementation of X25519. In this folder the reader will find multiple levels of implementation of X25519.
\begin{itemize} \begin{itemize}
\item \textbf{\texttt{Libs/}} contains basic libraries and tools to help use \item \textbf{\texttt{Libs/}} contains basic libraries and tools to help
reason with lists and decidable procedures. reason with lists and decidable procedures.
\item \textbf{\texttt{ListsOp/}} defines operators on list such as \item \textbf{\texttt{ListsOp/}} defines operators on list such as
\Coqe{ZofList} and related lemmas using \eg \VSTe{Forall}. \Coqe{ZofList} and related lemmas using \eg \VSTe{Forall}.
......
...@@ -126,7 +126,7 @@ The encoding from integers to bytes is defined in a similar way. ...@@ -126,7 +126,7 @@ The encoding from integers to bytes is defined in a similar way.
%XXX-Peter: Again I'm confused... why are there two \rightarrows? %XXX-Peter: Again I'm confused... why are there two \rightarrows?
%XXX-Benoit it is the functional view of arguments and partial functions. It is called Currying. %XXX-Benoit it is the functional view of arguments and partial functions. It is called Currying.
\end{dfn} \end{dfn}
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt] \begin{lstlisting}[language=Coq,aboveskip=1pt,belowskip=1pt]
Fixpoint ListofZn_fp {n:Z} (a:Z) (f:nat) : list Z := Fixpoint ListofZn_fp {n:Z} (a:Z) (f:nat) : list Z :=
match f with match f with
| 0%nat => [] | 0%nat => []
...@@ -138,7 +138,7 @@ Definition ListofZ32 {n:Z} (a:Z) : list Z := ...@@ -138,7 +138,7 @@ Definition ListofZ32 {n:Z} (a:Z) : list Z :=
\end{lstlisting} \end{lstlisting}
In order to increase the trust in our formalization, we prove that In order to increase the trust in our formalization, we prove that
\Coqe{ListofZ32} and \Coqe{ZofList} are inverse to each other. \Coqe{ListofZ32} and \Coqe{ZofList} are inverse to each other.
\begin{lstlisting}[language=Coq,aboveskip=0pt,belowskip=1pt] \begin{lstlisting}[language=Coq,aboveskip=1pt,belowskip=1pt]
Lemma ListofZ32_ZofList_Zlength: forall (l:list Z), Lemma ListofZ32_ZofList_Zlength: forall (l:list Z),
Forall (fun x => 0 <= x < 2^n) l -> Forall (fun x => 0 <= x < 2^n) l ->
Zlength l = 32 -> Zlength l = 32 ->
......
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