Commit 3523ebff authored by Benoit Viguier's avatar Benoit Viguier
Browse files

mods

parent b4801b99
......@@ -78,11 +78,13 @@ proofs up to the mathematical definition of the group theory behind elliptic cur
When considering the target of the verification effort, the closest work
to this paper is presented in~\cite{Chen2014VerifyingCS}, which presents
a mechanized proof of two assembly-level implementations of the core function of X25519.
a mechanized proof of two assembly-level implementations of the core function
of X25519.
The proof in~\cite{Chen2014VerifyingCS} takes a different approach from ours.
It uses heavy annotation of code together with SAT solvers;
It uses heavy annotation of code in order to ``guide'' a SAT solver,
also, it does not cover the full X25519 functionality and does
not make the link to the mathematical definition from~\cite{Ber06}.
We only need to anotate the specifications and loop invariants.
%Synthesis approaches force the user to depend on generated code which may not
%be optimal (speed, compactness) and they require compiler tweaks in order
......
......@@ -32,7 +32,8 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{
\subsection{Formalization of elliptic Curves}
\label{subsec:ECC}
\fref{tikz:ProofHighLevel1} presents an intuition of the proof.
\fref{tikz:ProofHighLevel1} presents an intuition of the proof of the ladder's
correctness.
\begin{figure}[h]
\centering
\include{tikz/highlevel1}
......@@ -329,10 +330,11 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) :
\label{tikz:ProofHighLevel2}
\end{figure}
To be able to use the above theorem we need to satisfy hypothesis
\ref{hyp:a_minus_4_not_square}: $a^2-4$ is not a square in \K:
To be able to use the \tref{thm:montgomery-ladder-correct} we need to satisfy
hypothesis~\ref{hyp:a_minus_4_not_square}:%
% $a^2-4$ is not a square in \K:
$$\forall x \in \K,\ x^2 \neq a^2-4.$$
There always exists $x \in \F{p^2}$ such that $x^2 = a^2-4$,
However there always exists $x \in \F{p^2}$ such that $x^2 = a^2-4$,
preventing the use \tref{thm:montgomery-ladder-correct}
with $\K = \F{p^2}$.
......
......@@ -212,29 +212,29 @@ Definition RFC (n: list Z) (p: list Z) : list Z :=
% Pack25519 (Low.M a (Inv25519 c)).
% \end{lstlisting}
\subsection{Equivalence between For Loops}
\label{subsubsec:for}
~
\begin{lstlisting}[language=Coq]
Variable T: Type.
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)
end.
Fixpoint rec_fn_rev_acc (n:nat) (m:nat) (s:T) :=
match n with
| 0 => s
| S n => g (m - n - 1) (rec_fn_rev_acc n m s)
end.
Definition rec_fn_rev (n:nat) (s:T) :=
rec_fn_rev_acc n n s.
Lemma Tail_Head_equiv :
forall (n:nat) (s:T),
rec_fn n s = rec_fn_rev n s.
\end{lstlisting}
% \subsection{Equivalence between For Loops}
% \label{subsubsec:for}
% ~
% \begin{lstlisting}[language=Coq]
% Variable T: Type.
% 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)
% end.
%
% Fixpoint rec_fn_rev_acc (n:nat) (m:nat) (s:T) :=
% match n with
% | 0 => s
% | S n => g (m - n - 1) (rec_fn_rev_acc n m s)
% end.
%
% Definition rec_fn_rev (n:nat) (s:T) :=
% rec_fn_rev_acc n n s.
%
% Lemma Tail_Head_equiv :
% forall (n:nat) (s:T),
% rec_fn n s = rec_fn_rev n s.
% \end{lstlisting}
\newpage
~\\
\newpage
\section{Prior reviews}
\label{appendix:past-reviews}
......
% DEADLINE: Tuesday 21 at Noon.
\todo{
- Get down to 12 pages: "no more than 12 pages long, excluding the bibliography,
well-marked appendices, and supplementary material."
- Change the story: Verification of a crypto software from C up to Maths and
usable in protocol verification.
- Emphasize:\\
+ the added confidence between in X25519 Correctness\\
+ proof of real world software\\
......@@ -25,7 +30,11 @@ not in our case as we direct the proof.\\
- "I was wondering whether you consider the approach in [13] as synthesis or
verification, because to me, it seemed a mix/neither."\\
+ [13] is "Verified Low-Level Programming Embedded in F*",\\
+ reread [13] and answer in the "our answer part"
+ reread [13] and answer in the "our answer part"\\
+ => While the title says Verified Low-Level Programming, they generate C code,
so by definition it is synthesis. However, Low* forces the user to anotate the
code (if necessary) and uses a SMT solver to prove the memory safety,
correctness etc. at the Low* level. Depending of the level being considered.
- "[18] even uses Coq to verify a large portion of a C implementation of X25519
fully automatically."\\
......
% \documentclass[conference]{IEEEtran}
\documentclass[format=sigconf, anonymous=false, authordraft=true, screen=true, review=true]{acmart}
\documentclass[format=sigconf, anonymous=false, authordraft=false, screen=true, review=true]{acmart}
\usepackage{setup}
......
Markdown is supported
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