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

forward

parent 6af3609e
......@@ -45,7 +45,7 @@ program satisfies a functionnal specification in Coq.
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.
and show that our specification is an instance of it.
\todo[inline]{Add where the software is available}
......
......@@ -59,7 +59,7 @@ Points of an elliptic curve can be equiped with a structure of an abelian group.
\item $\Oinf$ is the neutral element under this law: if 3 points are colinear, their sum is equal to $\Oinf$.
\end{itemize}
This operaction can be defined in Coq as follow:
This operaction are defined in Coq as follow:
\begin{lstlisting}[language=Coq]
Definition neg (p : point) :=
if p is (| x, y |) then (| x, -y |) else EC_Inf.
......@@ -166,7 +166,7 @@ Lemma ec_of_mc_bij : bijective ec_of_mc.
Points on a projective plane are represented with a triple $(X:Y:Z)$. Any points except $(0:0:0)$ defines a point on a projective plane. A scalar multiple of a point defines the same point, \ie
for all $\alpha \neq 0$, $(X:Y:Z)$ and $(\alpha X:\alpha Y:\alpha Z)$ defines the same point. For $Z\neq 0$, the projective point $(X:Y:Z)$ corresponds to the point $(X/Z,Y/Z)$ on the Euclidian plane, likewise the point $(X,Y)$ on the Euclidian plane corresponds to $(X:Y:1)$ on the projective plane.
We can write the equation for a Montgomery curve $M_{a,b}(\K)$ as such:
We write the equation for a Montgomery curve $M_{a,b}(\K)$ as such:
\begin{equation}
b \bigg(\frac{Y}{Z}\bigg)^2 = \bigg(\frac{X}{Z}\bigg)^3 + a \bigg(\frac{X}{Z}\bigg)^2 + \bigg(\frac{X}{Z}\bigg)
\end{equation}
......
......@@ -6,7 +6,7 @@ Clight description of TweetNaCl and Coq functions producing similar behaviors.
\subsection{Number representation and C implementation}
As described in Section \ref{sec:impl}, numbers in \TNaCle{gf} are represented
in base $2^{16}$ and we can use a direct mapping to represent that array as a list
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 as a full integer.
\begin{definition}
......@@ -51,7 +51,7 @@ Lemma mult_GF_Zlength :
\subsection{Inversions in \Zfield}
In a similar fashion we can define a Coq version of the inversion mimicking
In a similar fashion we define a Coq version of the inversion mimicking
the behavior of \TNaCle{inv25519} over \Coqe{list Z}.
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf a)
......@@ -126,7 +126,7 @@ To prove the correctness of the result we can use multiple strategies such as:
\item Proving it is special case of square-and-multiply algorithm applied to
a specific number and then show that this number is indeed $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 can prove that
$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 for the benefits of simplicity. However it requires to
......@@ -145,13 +145,13 @@ 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.
$$reify\_P : P_{bool} = true \implies P$$
By applying $reify\_P$ on $P$ our goal become $P_{bool} = true$.
We can then compute the result of $P_{bool}$. If the decision goes well we are
We then compute the result of $P_{bool}$. If the decision goes well we are
left with the tautology $true = true$.
To prove that the \Coqe{Inv25519_Z} is computing $x^{2^{255}-21}$,
we define a Domain Specific Language.
\begin{definition}
Let \Coqe{expr_inv} denote an expression which can be either a term;
Let \Coqe{expr_inv} denote an expression which is either a term;
a multiplication of expressions; a squaring of an expression or a power of an expression.
And Let \Coqe{formula_inv} denote an equality between two expressions.
\end{definition}
......@@ -212,7 +212,7 @@ Lemma pow_inv_pow_fn_rev_eq :
e_inv_denote (pow_inv a b c g) =
pow_fn_rev_Z a b (e_inv_denote c) (e_inv_denote g).
\end{lstlisting}
We can then derive the following lemma.
We then derive the following lemma.
\begin{lemma}
\label{reify}
With an appropriate choice of variables,
......@@ -222,7 +222,7 @@ With an appropriate choice of variables,
In order to prove formulas in \Coqe{formula_inv},
we have the following a decidable procedure.
We define \Coqe{pow_expr_inv}, a function which returns the power of an expression.
We can then compare the two values and decide over their equality.
We then compare the two values and decide over their equality.
\begin{Coq}
Fixpoint pow_expr_inv (t:expr_inv) : Z :=
match t with
......@@ -256,7 +256,7 @@ We prove our decision procedure correct.
For all formulas $f$, if the decision over $f$ returns \Coqe{true},
then the denoted equality by $f$ is true.
\end{lemma}
Which can be formalized as:
Which is formalized as:
\begin{Coq}
Lemma decide_formula_inv_impl :
forall (f:formula_inv),
......
\section{Using VST}
\section{VST and the Trust of the proof}
Any formal system relies on a trusted base. In this section we describe our
chain of trust bringing up to light some tripping points a user may encounter
......@@ -90,27 +90,33 @@ Example of such cases are summarized in Fig \ref{tk:MemSame}.
\subsection{Verifiying \texttt{for} loops: head and tail recursion}
Final state of \texttt{for} loops can be computed by simple recursive functions.
However we must define invariants which are true for each step of the iterations.
For a lower value of the iterator \texttt{i}, a normal recursive function in Coq
would only compute the last \texttt{i} steps instead of the first \texttt{i} ones
as we would like for our invariant.
e.g. for a function $g : \N \rightarrow T \rightarrow T $ iterated a maximum of
5 times, for $i = 2$, $g(4, g(3, x))$ instead of $g(1, g(0 , x))$.
This requires us to define each function with
an accumulator.
We define two recursive functions \Coqe{rec_fn} and \Coqe{rec_fn_rev_acc}.
They emulate the behavior of \texttt{for} loops and take as implicit argument a
function \Coqe{g} which emulate the body of the loop.
\begin{lemma}
With their appropriate \texttt{for} loops, Head recursion and Tail recursion
compute the same result.
\end{lemma}
The intuition behind the proof
Final state of \texttt{for} loops are usually computed by simple recursive functions.
However we must define invariants which are true for each iterations.
Assume 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 and return a state.
It simulate the body of the \texttt{for} loop.
Assume it's recursive call: $f : \N \rightarrow State \rightarrow State $ which iteratively apply $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))))
% \\
% f(3,s) &= g(0,g(1,g(2,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 as follows:
\begin{Coq}
Variable T : Type.
Variable g : nat -> T -> T.
......@@ -118,7 +124,7 @@ Variable g : nat -> T -> T.
Fixpoint rec_fn (n:nat) (s:T) :=
match n with
| 0 => s
| S n => (rec_fn n (g n s))
| S n => rec_fn n (g n s)
end.
Fixpoint rec_fn_rev_acc (n:nat) (m:nat) (s:T) :=
......@@ -134,9 +140,7 @@ Lemma Tail_Head_equiv :
forall (n:nat) (s:T),
rec_fn n s = rec_fn_rev n s.
\end{Coq}
Using this formalization, we prove that the 255 steps of the montgomery ladder in C provide the same computations are the one defined in Algorithm \ref{montgomery-double-add}.
\todo[inline]{How many lines of specification ?}
\todo[inline]{How many lines of proofs ?}
\todo[inline]{How long did it take ?}
......@@ -10,7 +10,7 @@
\usepackage{type1cm}
\newcommand{\lstsize}{\fontsize{8.5pt}{8.5pt}\selectfont}
\usepackage{algorithm, algorithmic}
\usepackage{amsmath}
\usepackage{xspace}
\usepackage{listings}
\usepackage{booktabs}
......
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