Skip to content
GitLab
Commit 3fd3baa1 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

before renaming (order is wrong)

parent 20b3e989
Hide whitespace changes
Inline Side-by-side
paper/4.2_forloops.tex 0 → 100644
View file @ 3fd3baa1
%XXX-Peter: shouldn't verifying fixed-length for loops be rather standard?
%XXX Benoit: it is simple if the argument is increasing or if the "recursive call"
% is made before the computations.
% This is not the case here: you compute idx 255 before 254...
% Can we shorten the next paragraph?
\subheading{Verifying \texttt{for} loops.}
Final states of \texttt{for} loops are usually computed by simple recursive functions.
However, we must define invariants which are true for each iteration step.
Assume that we want to prove a decreasing loop where indexes go from 3 to 0.
Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
input an integer for the index and a state, then returns a state.
It simulates the body of the \texttt{for} loop.
Define the recursion: $f : \N \rightarrow State \rightarrow State $ which
iteratively applies $g$ with decreasing index:
\begin{equation*}
f ( i , s ) =
\begin{cases}
s & \text{if } s = 0 \\
f( i - 1 , g ( i - 1 , s )) & \text{otherwise}
\end{cases}
\end{equation*}
Then we have:
\begin{align*}
f(4,s) &= g(0,g(1,g(2,g(3,s))))
\end{align*}
To prove the correctness of $f(4,s)$, we need to prove that intermediate steps
$g(3,s)$; $g(2,g(3,s))$; $g(1,g(2,g(3,s)))$; $g(0,g(1,g(2,g(3,s))))$ are correct.
Due to the computation order of recursive function, our loop invariant for
$i\in\{0,1,2,3,4\}$ cannot use $f(i)$.
To solve this, we define an auxiliary function with an accumulator such that
given $i\in\{0,1,2,3,4\}$, it will compute the first $i$ steps of the loop.
We then prove for the complete number of steps, the function with the accumulator
and without returns the same result.
We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
Using this formalization, we prove that the 255 steps of the Montgomery ladder
in C provide the same computations as in \coqe{RFC}.
% %
paper/4.3_numbers.tex 0 → 100644
View file @ 3fd3baa1
\subsection{Number representation and C implementation}
\label{subsec:num-repr-rfc}
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
in base $2^{16}$ and we use a direct mapping to represent that array as a list
integers in Coq. However, in order to show the correctness of the basic operations,
we need to convert this number to a full integer.
We reuse the mapping
$\text{\coqe{ZofList}} : \Z \rightarrow \texttt{list}~\Z \rightarrow \Z$ from \sref{subsec:integer-bytes}
and define a notation where $n$ is $16$, placing us with a radix of $2^{16}$.
\begin{lstlisting}[language=Coq]
Notation "Z16.lst A" := (ZofList 16 A).
\end{lstlisting}
To facilitate working in $\Zfield$, we define the \coqe{:GF} notation.
\begin{lstlisting}[language=Coq]
Notation "A :GF" := (A mod (2^255-19)).
\end{lstlisting}
Later in \sref{subsec:Zmodp}, we formally define $\Ffield$.
Equivalence between operations in $\Zfield$ (\ie under \coqe{:GF}) and in $\Ffield$ are easily proven.
Using these two definitions, we prove intermediate lemmas such as the correctness of the
multiplication \Coqe{Low.M} where \Coqe{Low.M} replicates the computations and steps done in C.
\begin{lemma}
\label{lemma:mult_correct}
\Coqe{Low.M} correctly implements the multiplication over $\Zfield$.
\end{lemma}
And specified in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma mult_GF_Zlength :
forall (a:list Z) (b:list Z),
Zlength a = 16 ->
Zlength b = 16 ->
(Z16.lst (Low.M a b)) :GF =
(Z16.lst a * Z16.lst b) :GF.
\end{lstlisting}
However for our purpose, simple functional correctness is not enough.
We also need to define the bounds under which the operation is correct,
allowing us to chain them, guaranteeing us the absence of overflow.
\begin{lemma}
\label{lemma:mult_bounded}
if all the values of the input arrays are constrained between $-2^{26}$ and $2^{26}$,
then the output of \coqe{Low.M} will be constrained between $-38$ and $2^{16} + 38$.
\end{lemma}
And seen in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma M_bound_Zlength :
forall (a:list Z) (b:list Z),
Zlength a = 16 ->
Zlength b = 16 ->
Forall (fun x => -2^26 < x < 2^26) a ->
Forall (fun x => -2^26 < x < 2^26) b ->
Forall (fun x => -38 <= x < 2^16 + 38) (Low.M a b).
\end{lstlisting}
paper/4.4_reflections.tex 0 → 100644
View file @ 3fd3baa1
\subsection{Reflections, inversions and packing}
\label{subsec:inversions-reflections}
We now turn our attention to the multiplicative inverse in $\Zfield$ and techniques
to improve the verification speed of complex formulas.
\subheading{Inversion in \Zfield.}
We define a Coq version of the inversion mimicking
the behavior of \TNaCle{inv25519} (see below) over \Coqe{list Z}.
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf i)
{
gf c;
int a;
set25519(c,i);
for(a=253;a>=0;a--) {
S(c,c);
if(a!=2&&a!=4) M(c,c,i);
}
FOR(a,16) o[a]=c[a];
}
\end{lstlisting}
We specify this with 2 functions: a recursive \Coqe{pow_fn_rev}
to simulate the \texttt{for} loop and a simple \Coqe{step_pow} containing the body.
\begin{lstlisting}[language=Coq]
Definition step_pow (a:Z)
(c:list Z) (g:list Z) : list Z :=
let c := Sq c in
if a <>? 2 && a <>? 4
then M c g
else c.
Function pow_fn_rev (a:Z) (b:Z)
(c: list Z) (g: list Z)
{measure Z.to_nat a} : (list Z) :=
if a <=? 0
then c
else
let prev := pow_fn_rev (a - 1) b c g in
step_pow (b - a) prev g.
\end{lstlisting}
This \Coqe{Function} requires a proof of termination. It is done by proving the
well-foundedness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling
\Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the Clight definition.
\begin{lstlisting}[language=Coq]
Definition Inv25519 (x:list Z) : list Z :=
pow_fn_rev 254 254 x x.
\end{lstlisting}
Similarly we define the same function over $\Z$.
\begin{lstlisting}[language=Coq]
Definition step_pow_Z (a:Z) (c:Z) (g:Z) : Z :=
let c := c * c in
if a <>? 2 && a <>? 4
then c * g
else c.
Function pow_fn_rev_Z (a:Z) (b:Z) (c:Z) (g: Z)
{measure Z.to_nat a} : Z :=
if (a <=? 0)
then c
else
let prev := pow_fn_rev_Z (a - 1) b c g in
step_pow_Z (b - a) prev g.
Definition Inv25519_Z (x:Z) : Z :=
pow_fn_rev_Z 254 254 x x.
\end{lstlisting}
By using \lref{lemma:mult_correct}, we prove their equivalence in $\Zfield$.
\begin{lemma}
\label{lemma:Inv_equivalence}
The function \coqe{Inv25519} over list of integers computes the same
result at \coqe{Inv25519_Z} over integers in \Zfield.
\end{lemma}
This is formalized in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma Inv25519_Z_GF : forall (g:list Z),
length g = 16 ->
(Z16.lst (Inv25519 g)) :GF =
(Inv25519_Z (Z16.lst g)) :GF.
\end{lstlisting}
In TweetNaCl, \TNaCle{inv25519} computes an inverse in $\Zfield$.
It uses Fermat's little theorem by raising to the power of $2^{255}-21$ with a
square-and-multiply algorithm. The binary representation
of $p-2$ implies that every step does a multiplications except for bits 2 and 4.
To prove the correctness of the result we could use multiple strategies such as:
\begin{itemize}
\item Proving it is a special case of square-and-multiply algorithm applied to $2^{255}-21$.
\item Unrolling the for loop step-by-step and applying the equalities
$x^a \times x^b = x^{(a+b)}$ and $(x^a)^2 = x^{(2 \times a)}$. We prove that
the resulting exponent is $2^{255}-21$.
\end{itemize}
We use the second method because it is simpler. However, it requires us to
apply the unrolling and exponentiation formulas 255 times. This could be automated
in Coq with tacticals such as \Coqe{repeat}, but it generates a proof object which
will take a long time to verify.
\subheading{Reflections.}
In order to speed up the verification we use a
technique called ``Reflection''. It provides us with flexibility, \eg we don't
need to know the number of times nor the order in which the lemmas needs to be
applied (chapter 15 in \cite{CpdtJFR}).
The idea is to \emph{reflect} the goal into a decidable environment.
We show that for a property $P$, we can define a decidable Boolean property
$P_{bool}$ such that if $P_{bool}$ is \Coqe{true} then $P$ holds.
$$\text{\textit{reify\_P}} : P_{bool} = \text{\textit{true}} \implies P$$
By applying \textit{reify\_P} on $P$ our goal becomes $P_{bool} = true$.
We then compute the result of $P_{bool}$. If the decision goes well we are
left with the tautology $\text{\textit{true}} = \text{\textit{true}}$.
With this technique we prove the functional correctness of the inversion over \Zfield.
\begin{lemma}
\label{cor:inv_comput_field}
\Coqe{Inv25519} computes an inverse in \Zfield.
\end{lemma}
This statement is formalized as
\begin{lstlisting}[language=Coq]
Corollary Inv25519_Zpow_GF : forall (g:list Z),
length g = 16 ->
Z16.lst (Inv25519 g) :GF =
(pow (Z16.lst g) (2^255-21)) :GF.
\end{lstlisting}
This reflection technique is also used where proofs requires some computing
over a small and finite domain of variables to test e.g. for all $i$ such that
$0 \le i < 16$.
Using reflection we prove that we can split the for loop in \TNaCle{pack25519}
into two parts.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
m[i-1]&=0xffff;
}
\end{lstlisting}
The first loop computes the subtraction, and the second applies the carries.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff
}
for(i=1;i<15;i++) {
m[i]=m[i]-((m[i-1]>>16)&1);
m[i-1]&=0xffff;
}
\end{lstlisting}
This loop separation allows simpler proofs. The first loop is seen as the
subtraction of \p. The resulting number represented in $\Zfield$ is invariant with
the iteration of the second loop. This result in the proof that \TNaCle{pack25519}
reduces modulo $\p$ and returns a number in base $2^8$.
\begin{lstlisting}[language=Coq]
Lemma Pack25519_mod_25519 :
forall (l:list Z),
Zlength l = 16 ->
Forall (fun x => -2^62 < x < 2^62) l ->
ZofList 8 (Pack25519 l) =
(Z16.lst l) mod (2^255-19).
\end{lstlisting}
By using each function \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519}; \coqe{montgomery_rec},
we defined a Coq definition \coqe{Crypto_Scalarmult} mimicking the exact behavior of X25519 in TweetNaCl.
By proving that each function \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519} behave over \coqe{list Z}
as their equivalent over \coqe{Z} with \coqe{:GF} (in \Zfield), we prove that given the same inputs \coqe{Crypto_Scalarmult} performs the same computation as \coqe{RFC}.
% This is formalized as follows in Coq:
\begin{lstlisting}[language=Coq]
Lemma Crypto_Scalarmult_RFC_eq :
forall (n: list Z) (p: list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
Crypto_Scalarmult n p = RFC n p.
\end{lstlisting}
This proves that TweetNaCl's X25519 implementation respect RFC~7748.
paper/4_lowlevel.tex
View file @ 3fd3baa1
......@@ -94,7 +94,7 @@ In this specification we state preconditions like:
to a list of integer values \VSTe{mVI p}.
\item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\
In order to consider all the possible inputs, we assume each
elements of the list \texttt{p} to be bounded by $0$ included and $2^8$
element of the list \texttt{p} to be bounded by $0$ included and $2^8$
excluded.
\item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\
We also assume that the length of the list \texttt{p} is 32. This defines the
......@@ -175,291 +175,3 @@ we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all cases (\eg all arguments are aliased) but it
is enough for our needs.
%XXX-Peter: shouldn't verifying fixed-length for loops be rather standard?
%XXX Benoit: it is simple if the argument is increasing or if the "recursive call"
% is made before the computations.
% This is not the case here: you compute idx 255 before 254...
% Can we shorten the next paragraph?
\subheading{Verifying \texttt{for} loops.}
Final states of \texttt{for} loops are usually computed by simple recursive functions.
However, we must define invariants which are true for each iteration step.
Assume that we want to prove a decreasing loop where indexes go from 3 to 0.
Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
input an integer for the index and a state, then returns a state.
It simulates the body of the \texttt{for} loop.
Define the recursion: $f : \N \rightarrow State \rightarrow State $ which
iteratively applies $g$ with decreasing index:
\begin{equation*}
f ( i , s ) =
\begin{cases}
s & \text{if } s = 0 \\
f( i - 1 , g ( i - 1 , s )) & \text{otherwise}
\end{cases}
\end{equation*}
Then we have:
\begin{align*}
f(4,s) &= g(0,g(1,g(2,g(3,s))))
\end{align*}
To prove the correctness of $f(4,s)$, we need to prove that intermediate steps
$g(3,s)$; $g(2,g(3,s))$; $g(1,g(2,g(3,s)))$; $g(0,g(1,g(2,g(3,s))))$ are correct.
Due to the computation order of recursive function, our loop invariant for
$i\in\{0,1,2,3,4\}$ cannot use $f(i)$.
To solve this, we define an auxiliary function with an accumulator such that
given $i\in\{0,1,2,3,4\}$, it will compute the first $i$ steps of the loop.
We then prove for the complete number of steps, the function with the accumulator
and without returns the same result.
We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
Using this formalization, we prove that the 255 steps of the Montgomery ladder
in C provide the same computations as in \coqe{RFC}.
% %
\subsection{Number representation and C implementation}
\label{subsec:num-repr-rfc}
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
in base $2^{16}$ and we use a direct mapping to represent that array as a list
integers in Coq. However, in order to show the correctness of the basic operations,
we need to convert this number to a full integer.
We reuse the mapping
$\text{\coqe{ZofList}} : \Z \rightarrow \texttt{list}~\Z \rightarrow \Z$ from \sref{subsec:integer-bytes}
and define a notation where $n$ is $16$, placing us with a radix of $2^{16}$.
\begin{lstlisting}[language=Coq]
Notation "Z16.lst A" := (ZofList 16 A).
\end{lstlisting}
To facilitate working in $\Zfield$, we define the \coqe{:GF} notation.
\begin{lstlisting}[language=Coq]
Notation "A :GF" := (A mod (2^255-19)).
\end{lstlisting}
Later in \sref{subsec:Zmodp}, we formally define $\Ffield$.
Equivalence between operations in $\Zfield$ (\ie under \coqe{:GF}) and in $\Ffield$ are easily proven.
Using these two definitions, we prove intermediate lemmas such as the correctness of the
multiplication \Coqe{Low.M} where \Coqe{Low.M} replicates the computations and steps done in C.
\begin{lemma}
\label{lemma:mult_correct}
\Coqe{Low.M} correctly implements the multiplication over $\Zfield$.
\end{lemma}
And specified in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma mult_GF_Zlength :
forall (a:list Z) (b:list Z),
Zlength a = 16 ->
Zlength b = 16 ->
(Z16.lst (Low.M a b)) :GF =
(Z16.lst a * Z16.lst b) :GF.
\end{lstlisting}
However for our purpose, simple functional correctness is not enough.
We also need to define the bounds under which the operation is correct,
allowing us to chain them, guaranteeing us the absence of overflow.
\begin{lemma}
\label{lemma:mult_bounded}
if all the values of the input arrays are constrained between $-2^{26}$ and $2^{26}$,
then the output of \coqe{Low.M} will be constrained between $-38$ and $2^{16} + 38$.
\end{lemma}
And seen in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma M_bound_Zlength :
forall (a:list Z) (b:list Z),
Zlength a = 16 ->
Zlength b = 16 ->
Forall (fun x => -2^26 < x < 2^26) a ->
Forall (fun x => -2^26 < x < 2^26) b ->
Forall (fun x => -38 <= x < 2^16 + 38) (Low.M a b).
\end{lstlisting}
\subsection{Reflections, inversions and packing}
\label{subsec:inversions-reflections}
We now turn our attention to the multiplicative inverse in $\Zfield$ and techniques
to improve the verification speed of complex formulas.
\subheading{Inversion in \Zfield.}
We define a Coq version of the inversion mimicking
the behavior of \TNaCle{inv25519} (see below) over \Coqe{list Z}.
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf i)
{
gf c;
int a;
set25519(c,i);
for(a=253;a>=0;a--) {
S(c,c);
if(a!=2&&a!=4) M(c,c,i);
}
FOR(a,16) o[a]=c[a];
}
\end{lstlisting}
We specify this with 2 functions: a recursive \Coqe{pow_fn_rev}
to simulate the \texttt{for} loop and a simple \Coqe{step_pow} containing the body.
\begin{lstlisting}[language=Coq]
Definition step_pow (a:Z)
(c:list Z) (g:list Z) : list Z :=
let c := Sq c in
if a <>? 2 && a <>? 4
then M c g
else c.
Function pow_fn_rev (a:Z) (b:Z)
(c: list Z) (g: list Z)
{measure Z.to_nat a} : (list Z) :=
if a <=? 0
then c
else
let prev := pow_fn_rev (a - 1) b c g in
step_pow (b - a) prev g.
\end{lstlisting}
This \Coqe{Function} requires a proof of termination. It is done by proving the
well-foundedness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling
\Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the Clight definition.
\begin{lstlisting}[language=Coq]
Definition Inv25519 (x:list Z) : list Z :=
pow_fn_rev 254 254 x x.
\end{lstlisting}
Similarly we define the same function over $\Z$.
\begin{lstlisting}[language=Coq]
Definition step_pow_Z (a:Z) (c:Z) (g:Z) : Z :=
let c := c * c in
if a <>? 2 && a <>? 4
then c * g
else c.
Function pow_fn_rev_Z (a:Z) (b:Z) (c:Z) (g: Z)
{measure Z.to_nat a} : Z :=
if (a <=? 0)
then c
else
let prev := pow_fn_rev_Z (a - 1) b c g in
step_pow_Z (b - a) prev g.
Definition Inv25519_Z (x:Z) : Z :=
pow_fn_rev_Z 254 254 x x.
\end{lstlisting}
By using \lref{lemma:mult_correct}, we prove their equivalence in $\Zfield$.
\begin{lemma}
\label{lemma:Inv_equivalence}
The function \coqe{Inv25519} over list of integers computes the same
result at \coqe{Inv25519_Z} over integers in \Zfield.
\end{lemma}
This is formalized in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma Inv25519_Z_GF : forall (g:list Z),
length g = 16 ->
(Z16.lst (Inv25519 g)) :GF =
(Inv25519_Z (Z16.lst g)) :GF.
\end{lstlisting}
In TweetNaCl, \TNaCle{inv25519} computes an inverse in $\Zfield$.
It uses Fermat's little theorem by raising to the power of $2^{255}-21$ with a
square-and-multiply algorithm. The binary representation
of $p-2$ implies that every step does a multiplications except for bits 2 and 4.
To prove the correctness of the result we could use multiple strategies such as:
\begin{itemize}
\item Proving it is a special case of square-and-multiply algorithm applied to $2^{255}-21$.
\item Unrolling the for loop step-by-step and applying the equalities
$x^a \times x^b = x^{(a+b)}$ and $(x^a)^2 = x^{(2 \times a)}$. We prove that
the resulting exponent is $2^{255}-21$.
\end{itemize}
We use the second method because it is simpler. However, it requires us to
apply the unrolling and exponentiation formulas 255 times. This could be automated
in Coq with tacticals such as \Coqe{repeat}, but it generates a proof object which
will take a long time to verify.
\subheading{Reflections.}
In order to speed up the verification we use a
technique called ``Reflection''. It provides us with flexibility, \eg we don't
need to know the number of times nor the order in which the lemmas needs to be
applied (chapter 15 in \cite{CpdtJFR}).
The idea is to \emph{reflect} the goal into a decidable environment.
We show that for a property $P$, we can define a decidable Boolean property
$P_{bool}$ such that if $P_{bool}$ is \Coqe{true} then $P$ holds.
$$\text{\textit{reify\_P}} : P_{bool} = \text{\textit{true}} \implies P$$
By applying \textit{reify\_P} on $P$ our goal becomes $P_{bool} = true$.
We then compute the result of $P_{bool}$. If the decision goes well we are
left with the tautology $\text{\textit{true}} = \text{\textit{true}}$.
With this technique we prove the functional correctness of the inversion over \Zfield.
\begin{lemma}
\label{cor:inv_comput_field}
\Coqe{Inv25519} computes an inverse in \Zfield.
\end{lemma}
This statement is formalized as
\begin{lstlisting}[language=Coq]
Corollary Inv25519_Zpow_GF : forall (g:list Z),
length g = 16 ->
Z16.lst (Inv25519 g) :GF =
(pow (Z16.lst g) (2^255-21)) :GF.
\end{lstlisting}
This reflection technique is also used where proofs requires some computing
over a small and finite domain of variables to test e.g. for all $i$ such that
$0 \le i < 16$.
Using reflection we prove that we can split the for loop in \TNaCle{pack25519}
into two parts.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
m[i-1]&=0xffff;
}
\end{lstlisting}
The first loop computes the subtraction, and the second applies the carries.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
m[i]=t[i]-0xffff
}
for(i=1;i<15;i++) {
m[i]=m[i]-((m[i-1]>>16)&1);
m[i-1]&=0xffff;
}
\end{lstlisting}
This loop separation allows simpler proofs. The first loop is seen as the
subtraction of \p. The resulting number represented in $\Zfield$ is invariant with
the iteration of the second loop. This result in the proof that \TNaCle{pack25519}
reduces modulo $\p$ and returns a number in base $2^8$.
\begin{lstlisting}[language=Coq]
Lemma Pack25519_mod_25519 :
forall (l:list Z),
Zlength l = 16 ->
Forall (fun x => -2^62 < x < 2^62) l ->
ZofList 8 (Pack25519 l) =
(Z16.lst l) mod (2^255-19).
\end{lstlisting}
By using each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519}; \coqe{montgomery_rec},
we defined a Coq definition \coqe{Crypto_Scalarmult} mimicking the exact behavior of X25519 in TweetNaCl.
By proving that each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519} behave over \coqe{list Z}
as their equivalent over \coqe{Z} with \coqe{:GF} (in \Zfield), we prove that given the same inputs \coqe{Crypto_Scalarmult} performs the same computation as \coqe{RFC}.
% This is formalized as follows in Coq:
\begin{lstlisting}[language=Coq]
Lemma Crypto_Scalarmult_RFC_eq :
forall (n: list Z) (p: list Z),
Zlength n = 32 ->
Zlength p = 32 ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) n ->
Forall (fun x => 0 <= x /\ x < 2 ^ 8) p ->
Crypto_Scalarmult n p = RFC n p.
\end{lstlisting}
This proves that TweetNaCl's X25519 implementation respect RFC~7748.
paper/A4_reviews.tex
View file @ 3fd3baa1
......@@ -79,6 +79,13 @@ dangling there.
On page 9: "each functions" => no s
\subheading{Our answer}
XXX:TODO
We corrected the typos. There are no new proof techniques in the case of this
verification. We used reflections techniques to generically solve some of our
goals such as the proof of inversion.
\subsection{S\&P 2020 Review \#582B}
Overall merit: 4. Weak accept - While flawed, the paper has merit and we should
......@@ -175,6 +182,11 @@ of an assymmetric cryptographic primitives. Does this mean that VST has been
used for symmetric cryptographic primitives before? From the text, I wasn't sure
whether this is careful quantification or not.
\subheading{Our answer}
Clarification in intro: VST has already been used to verify symmetric Cryptographic
primities, as mentioned later by \cite{Beringer2015VerifiedCA} and \cite{2015-Appel}.
\subsection{S\&P 2020 Review \#582C}
Overall merit: 3. Weak reject - The paper has flaws, but I will not argue against it.
......
paper/tikz/proof.tex
View file @ 3fd3baa1
......@@ -56,6 +56,7 @@
% ~~$P \in$ \TNaCles{u8[32]}\\
{\color{doc@lstdirective}\textbf{Post}}:\\
~~\texttt{s}$[\!\!\{$\texttt{q}$\}\!\!]\leftarrow$~\texttt{RFC}$(n,P)$};
\draw (2.75,-2) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};
\end{scope}
% VST Theorem
......@@ -64,7 +65,8 @@
\draw (0,0) -- (2.5,0) -- (2.5,-1.25) -- (0, -1.25) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Proof};
\draw (1.25,-0.5) node[textstyle, anchor=center] {\{{\color{doc@lstnumbers}\textbf{Pre}}\} \texttt{Prog} \{{\color{doc@lstdirective}\textbf{Post}}\}};
\draw (2.5,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
\draw (2.5,0) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{\checkmark}};
\draw (2.5,-1.25) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};
\end{scope}
\path [thick, double] (5.625,-1.5) edge [out=-90, in=90] (5.625, -2.5);
......@@ -81,6 +83,7 @@
\draw (0,0) -- (1.75,0) -- (1.75,-1) -- (0, -1) -- cycle;
\draw (0.3,-0.05) node[textstyle] {Definition};
\draw (0.875,-0.5) node[textstyle, anchor=center] {$n \cdot P$};
\draw (1.75,-1) node[textstyle, anchor = south east] {\color{doc@lstfunctions}{.V}};
\end{scope}