Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coqveriftweetnacl
Commits
374f9d0d
Commit
374f9d0d
authored
Jan 17, 2020
by
Benoit Viguier
Browse files
more text + make spell
parent
0c99e7b1
Changes
14
Hide whitespace changes
Inline
Sidebyside
paper/0todo.tex
View file @
374f9d0d
\todo
{
% \todo{
%
 Get down to 12 pages: "no more than 12 pages long, excluding the bibliography,
%  Get down to 12 pages: "no more than 12 pages long, excluding the bibliography,
wellmarked appendices, and supplementary material."
% wellmarked appendices, and supplementary material."
%
 Emphasize:
\\
%  Emphasize:\\
+ the added confidence between in X25519 Correctness
\\
% + the added confidence between in X25519 Correctness\\
+ proof of real world software
\\
% + proof of real world software\\
}
% }
%
With respect to the reviews:
% With respect to the reviews:
%
\todo
{
% \todo{
%
 Give number of personhours
%  Give number of personhours
%
 "This did not become very clear, because you mostly describe names
%  "This did not become very clear, because you mostly describe names
of tool while leaving out the details of what these tools carry out
% of tool while leaving out the details of what these tools carry out
conceptually."
\\
% conceptually."\\
+ anotation have to be carried out through the proof to help the smtsolver,
% + anotation have to be carried out through the proof to help the smtsolver,
not in our case as we direct the proof.
% not in our case as we direct the proof.
%
 "In particular,
%  "I was wondering whether you consider the approach in [13] as synthesis or
the Figure seems to used a nice abstraction of properties that is not
% verification, because to me, it seemed a mix/neither."\\
used elsewhere in the paper. I.e., elsewhere in the paper, there is
% + [13] is "Verified LowLevel Programming Embedded in F*",\\
usually a lot of code details."
\\
% + reread [13] and answer in the "our answer part"
+ I don't know what to do on that one.
%
%  "[18] even uses Coq to verify a large portion of a C implementation of X25519
 "I was wondering whether you consider the approach in [13] as synthesis or
% fully automatically."\\
verification, because to me, it seemed a mix/neither."
\\
% + This is not verification, this is synthesis. The approach is completely different.
+ [13] is "Verified LowLevel Programming Embedded in F*",
\\
%
+ reread [13] and answer in the "our answer part"
%  "Still, TweetNaCl is not necessarily the most complex (and certainly not the most
% efficient) implementation of X25519 that has been verified, which makes the
 "[18] even uses Coq to verify a large portion of a C implementation of X25519
% novelty of this work hard to justify."\\
fully automatically."
\\
% + True, but all the other works have been from a spec and generate correct code
+ This is not verification, this is synthesis. The approach is completely different.
% approach, here we go the opposite way. While the code of other libraries are
% different, the montgomery ladder are often similar and the optimizations comes
 "Still, TweetNaCl is not necessarily the most complex (and certainly not the most
% mostly from the big number computations.\\
efficient) implementation of X25519 that has been verified, which makes the
%
novelty of this work hard to justify."
\\
%  "This is a wellknown problem for formal
+ True, but all the other works have been from a spec and generate correct code
% verification papers, and I don’t have great advice except to suggest
approach, here we go the opposite way. While the code of other libraries are
% that the authors separate out the code fragments into figures and
different, the montgomery ladder are often similar and the optimizations comes
% let the text focus on the highlevel ideas of the code."\\
mostly from the big number computations.
\\
% + @PETER: How to address that ?
%
 "This is a wellknown problem for formal
%  "At the end of Section IV, I would have loved to see some high
verification papers, and I don’t have great advice except to suggest
% level lessons on what the proof taught you, and what part of this
that the authors separate out the code fragments into figures and
% proof would be reusable if you decided to verify Ed25519 or X448
let the text focus on the highlevel ideas of the code."
\\
% or P256, for example."\\
+ @PETER: How to address that ?
% + see second Todo
%
 "At the end of Section IV, I would have loved to see some high
%  "It also appears that the authors do not verify the constanttime
level lessons on what the proof taught you, and what part of this
% guarantees of the TweetNaCl code. Could this be done in their
proof would be reusable if you decided to verify Ed25519 or X448
% framework?"
or P256, for example."
\\
% + Nope => mention in limitation at the end of the paper?
+ see second Todo
%
%  Clamping and section V.\\
 "It also appears that the authors do not verify the constanttime
% + The clamping allows to reduce the group to prime elements, we do not provide
guarantees of the TweetNaCl code. Could this be done in their
% such proofs.\\
framework?"
%  We prove that for all n the computations on the ladder holds.
+ Nope => mention in limitation at the end of the paper?
%
%  "More importantly, could you claim that your proof of equivalence also provides
 Clamping and section V.
\\
% a justification for the implementations of Fiat Crypto or HACL*, hence adding
+ The clamping allows to reduce the group to prime elements, we do not provide
% value to those other projects in addition to your own?"
such proofs.
\\
% + Peter ?
 We prove that for all n the computations on the ladder holds.
% }
 "More importantly, could you claim that your proof of equivalence also provides
a justification for the implementations of Fiat Crypto or HACL*, hence adding
value to those other projects in addition to your own?"
+ Peter ?
}
paper/1intro.tex
View file @
374f9d0d
...
@@ 113,7 +113,10 @@ proof techniques used to show the correctness with respect to RFC~7748~\cite{rfc
...
@@ 113,7 +113,10 @@ proof techniques used to show the correctness with respect to RFC~7748~\cite{rfc
and Strub and the correctness of X25519 implementation with respect to Bernstein's
and Strub and the correctness of X25519 implementation with respect to Bernstein's
specifications~
\cite
{
Ber14
}
.
specifications~
\cite
{
Ber14
}
.
Finally in
\sref
{
sec:Conclusion
}
we discuss the trusted code base of our proofs.
Finally in
\sref
{
sec:Conclusion
}
we discuss the trusted code base of our proofs.
\fref
{
tikz:ProofOverview
}
shows a graph of dependencies of the proofs.
\fref
{
tikz:ProofOverview
}
shows a graph of dependencies of the proofs.
C source files are represented by
{
\color
{
doc@lstfunctions
}
.C
}
while
{
\color
{
doc@lstfunctions
}
.V
}
corresponds to Coq files.
\begin{figure}
[h]
\begin{figure}
[h]
\centering
\centering
...
@@ 122,9 +125,6 @@ Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs.
...
@@ 122,9 +125,6 @@ Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs.
\label
{
tikz:ProofOverview
}
\label
{
tikz:ProofOverview
}
\end{figure}
\end{figure}
\todoln
{
NEW
}
In this figure,
{
\color
{
doc@lstfunctions
}
.V
}
represent Coq files.
% Five years ago:
% Five years ago:
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
% \url{https://www.imperialviolet.org/2014/09/11/moveprovers.html}
% \url{https://www.imperialviolet.org/2014/09/07/provers.html}
% \url{https://www.imperialviolet.org/2014/09/07/provers.html}
...
...
paper/3RFC.tex
View file @
374f9d0d
...
@@ 94,8 +94,6 @@ Then we describe our mapping between littleendian representations and integers
...
@@ 94,8 +94,6 @@ Then we describe our mapping between littleendian representations and integers
(
\ref
{
subsec:integerbytes
}
) which we use to formalize the encoding and decoding.
(
\ref
{
subsec:integerbytes
}
) which we use to formalize the encoding and decoding.
% subsection or subheading ?
\subsection
{
A generic ladder
}
\subsection
{
A generic ladder
}
\label
{
subsec:specladder
}
\label
{
subsec:specladder
}
...
@@ 108,11 +106,6 @@ used in the ladder over generic types \coqe{T} and \coqe{T'}.
...
@@ 108,11 +106,6 @@ used in the ladder over generic types \coqe{T} and \coqe{T'}.
Those types are later instantiated as list of integers, integers, natural
Those types are later instantiated as list of integers, integers, natural
numbers, or field elements.
numbers, or field elements.
% The generic definition of the ladder (\coqe{montgomery_rec}) and its parallel with
% the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coqladder}.
\todo
{
Do we keep the pointer to
\sref
{
cswap
}
for CSWAP?
}
Our formalization differs slightly from the RFC. Indeed in order to optimize the
Our formalization differs slightly from the RFC. Indeed in order to optimize the
number of calls to
\texttt
{
CSWAP
}
(defined in
\sref
{
cswap
}
)
number of calls to
\texttt
{
CSWAP
}
(defined in
\sref
{
cswap
}
)
the RFC uses an additional variable to decide
the RFC uses an additional variable to decide
...
@@ 199,5 +192,5 @@ Definition encodeUCoordinate (x: Z) : list Z :=
...
@@ 199,5 +192,5 @@ Definition encodeUCoordinate (x: Z) : list Z :=
ListofZ32 8 x.
ListofZ32 8 x.
\end{lstlisting}
\end{lstlisting}
In this definition,
\coqe
{
clamp
}
is taking care of setting and
unsett
ing the
In this definition,
\coqe
{
clamp
}
is taking care of setting and
clear
ing the
selected bits as stated in the RFC and described in~
\sref
{
subsec:X25519keyexchange
}
.
selected bits as stated in the RFC and described in~
\sref
{
subsec:X25519keyexchange
}
.
paper/4.1VST.tex
View file @
374f9d0d
...
@@ 110,7 +110,6 @@ The correctness of this specification is formally proven in Coq with
...
@@ 110,7 +110,6 @@ The correctness of this specification is formally proven in Coq with
% For the sake of completeness we proved all intermediate functions.
% For the sake of completeness we proved all intermediate functions.
\subheading
{
Memory aliasing.
}
\subheading
{
Memory aliasing.
}
%
The semicolon in the
\VSTe
{
SEP
}
parts of the Hoare triples represents the
\emph
{
separating conjunction
}
(often written as a star), which means that
The semicolon in the
\VSTe
{
SEP
}
parts of the Hoare triples represents the
\emph
{
separating conjunction
}
(often written as a star), which means that
the memory shares of
\texttt
{
q
}
,
\texttt
{
n
}
and
\texttt
{
p
}
do not overlap.
the memory shares of
\texttt
{
q
}
,
\texttt
{
n
}
and
\texttt
{
p
}
do not overlap.
In other words,
In other words,
...
@@ 130,7 +129,6 @@ Examples of such cases are illustrated in \fref{tikz:MemSame}.
...
@@ 130,7 +129,6 @@ Examples of such cases are illustrated in \fref{tikz:MemSame}.
\caption
{
Aliasing and Separation Logic
}
%
\caption
{
Aliasing and Separation Logic
}
%
\label
{
tikz:MemSame
}
%
\label
{
tikz:MemSame
}
%
\end{figure}
\end{figure}
As a result, a function must either have multiple specifications or specify which
As a result, a function must either have multiple specifications or specify which
aliasing case is being used.
aliasing case is being used.
The first option would require us to do very similar proofs multiple times for a same function.
The first option would require us to do very similar proofs multiple times for a same function.
...
@@ 145,3 +143,16 @@ we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
...
@@ 145,3 +143,16 @@ 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.
In the proof of our specification, we do a case analysis over
$
k
$
when needed.
This solution does not generate all the possible cases of aliasing over 3 pointers
This solution does not generate all the possible cases of aliasing over 3 pointers
(
\eg
\texttt
{
o
}
=
\texttt
{
a
}
=
\texttt
{
b
}
) but it is enough to cover our needs.
(
\eg
\texttt
{
o
}
=
\texttt
{
a
}
=
\texttt
{
b
}
) but it is enough to cover our needs.
\subheading
{
Improving speed.
}
To make the verification the smoothest, the Coq formal definition of the function
should be as close as possible to the C implementation behavior.
Optimizations of such definitions are often counterproductive as they increase the
amount of proofs required for
\eg
bounds checking, loops invariants
\ldots
.
In order to further speedup the verification process, to prove the specification
\TNaCle
{
crypto
_
scalarmult
}
, we only need the specification of the subsequently
called functions (
\eg
\TNaCle
{
M
}
).
This provide with multiple advantages: the verification by the Coq kernel can be
done in parallel and multiple users can work on proving different functions at
the same time. For the sake of completeness we proved all intermediate functions.
paper/4.3numbers.tex
View file @
374f9d0d
\subsection
{
Number representation and C implementation
}
\subsection
{
Number representation and C implementation
}
\label
{
subsec:numreprrfc
}
\label
{
subsec:numreprrfc
}
\todo
{
Do we completely rewrite this section?
}
As described in
\sref
{
subsec:NumberTweetNaCl
}
, numbers in
\TNaCle
{
gf
}
are represented
As described in
\sref
{
subsec:NumberTweetNaCl
}
, numbers in
\TNaCle
{
gf
}
are represented
in base
$
2
^{
16
}$
and we 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,
integers in Coq. However, in order to show the correctness of the basic operations,
...
...
paper/4.4reflections.tex
View file @
374f9d0d
...
@@ 16,7 +16,7 @@ Corollary Inv25519_Zpow_GF : forall (g:list Z),
...
@@ 16,7 +16,7 @@ Corollary Inv25519_Zpow_GF : forall (g:list Z),
By using each function
\coqe
{
Low.M
}
;
\coqe
{
Low.A
}
;
\coqe
{
Low.Sq
}
;
\coqe
{
Low.Zub
}
;
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
{
Unpack25519
}
;
\coqe
{
clamp
}
;
\coqe
{
Pack25519
}
;
\coqe
{
Inv25519
}
;
\coqe
{
car25519
}
;
\coqe
{
montgomery
_
rec
}
, we defined in Coq
\coqe
{
Crypto
_
Scalarmult
}
and with VST
\coqe
{
montgomery
_
rec
}
, we defined in Coq
\coqe
{
Crypto
_
Scalarmult
}
and with VST
proved it mimic
k
s the exact behavior of X25519 in TweetNaCl.
proved it mimics the exact behavior of X25519 in TweetNaCl.
\end{sloppypar}
\end{sloppypar}
\begin{sloppypar}
\begin{sloppypar}
...
...
paper/4.5takeaway.tex
deleted
100644 → 0
View file @
0c99e7b1
\subsection
{
Advices to future VST users
}
paper/5highlevel.tex
View file @
374f9d0d
...
@@ 32,8 +32,7 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{
...
@@ 32,8 +32,7 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{
\subsection
{
Formalization of elliptic Curves
}
\subsection
{
Formalization of elliptic Curves
}
\label
{
subsec:ECC
}
\label
{
subsec:ECC
}
\todo
{
Beter here of after the final theorem of the subsection?
}
\fref
{
tikz:ProofHighLevel1
}
presents a intuition of the proof.
\begin{figure}
[h]
\begin{figure}
[h]
\centering
\centering
\include
{
tikz/highlevel1
}
\include
{
tikz/highlevel1
}
...
@@ 41,7 +40,6 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{
...
@@ 41,7 +40,6 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{
\label
{
tikz:ProofHighLevel1
}
\label
{
tikz:ProofHighLevel1
}
\end{figure}
\end{figure}
We consider elliptic curves over a field
$
\K
$
. We assume that the
We consider elliptic curves over a field
$
\K
$
. We assume that the
characteristic of
$
\K
$
is neither 2 or 3.
characteristic of
$
\K
$
is neither 2 or 3.
...
@@ 322,16 +320,15 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) :
...
@@ 322,16 +320,15 @@ Theorem opt_montgomery_ok (n m: nat) (x : K) :
\subsection
{
Curves, twists and extension fields
}
\subsection
{
Curves, twists and extension fields
}
\
todo
{
Beter here of after the final theorem of the subsection?
}
\
fref
{
tikz:ProofHighLevel2
}
gives a highlevel view of the proofs presented here.
\begin{figure}
[h]
\begin{figure}
[h]
\centering
\centering
\include
{
tikz/highlevel2
}
\include
{
tikz/highlevel2
}
\caption
{
Instan
c
iation
s
and proof dependencies for the correctness of X25519
}
\caption
{
Instan
t
iation and proof dependencies for the correctness of X25519
}
\label
{
tikz:ProofHighLevel2
}
\label
{
tikz:ProofHighLevel2
}
\end{figure}
\end{figure}
To be able to use the above theorem we need to satisfy hypothesis
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
:
\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
.
$$
$$
\forall
x
\in
\K
,
\
x
^
2
\neq
a
^
2

4
.
$$
...
@@ 392,14 +389,12 @@ We instantiate \coqe{opt_montgomery} in two specific ways:\\
...
@@ 392,14 +389,12 @@ We instantiate \coqe{opt_montgomery} in two specific ways:\\
With
\tref
{
thm:montgomeryladdercorrect
}
we derive the following two lemmas:
With
\tref
{
thm:montgomeryladdercorrect
}
we derive the following two lemmas:
\begin{lemma}
\begin{lemma}
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
,
\\
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
,
\\
such that
$
P
\in
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
\\
such that
$
P
\in
M
_{
486662
,
1
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
% Given $n$ and $x$,
$$
Curve
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
$$
Curve
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
\end{lemma}
\end{lemma}
\begin{lemma}
\begin{lemma}
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
\\
For all
$
x
\in
\F
{
p
}
,
\
n
\in
\N
,
\
P
\in
\F
{
p
}
\times
\F
{
p
}$
\\
such that
$
P
\in
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
\\
such that
$
P
\in
M
_{
486662
,
2
}
(
\F
{
p
}
)
$
and
$
\chi
_
0
(
P
)
=
x
$
.
% Given $n$ and $x$,
$$
Twist
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
$$
Twist
25519
\_
Fp
(
n,x
)
=
\chi
_
0
(
n
\cdot
P
)
$$
\end{lemma}
\end{lemma}
As the Montgomery ladder does not depend on
$
b
$
, it is trivial to
As the Montgomery ladder does not depend on
$
b
$
, it is trivial to
...
@@ 505,9 +500,6 @@ of formulas by using rewrite rules:
...
@@ 505,9 +500,6 @@ of formulas by using rewrite rules:
\end{split}
\end{split}
\end{equation*}
\end{equation*}
The injection
$
a
\mapsto
(
a,
0
)
$
from
$
\F
{
p
}$
to
$
\F
{
p
^
2
}$
preserves
The injection
$
a
\mapsto
(
a,
0
)
$
from
$
\F
{
p
}$
to
$
\F
{
p
^
2
}$
preserves
$
0
,
1
,
+
,

,
\times
$
. Thus
$
(
a,
0
)
$
can be abbreviated as
$
a
$
without confusions.
$
0
,
1
,
+
,

,
\times
$
. Thus
$
(
a,
0
)
$
can be abbreviated as
$
a
$
without confusions.
...
...
paper/6conclusion.tex
View file @
374f9d0d
...
@@ 52,8 +52,6 @@ o[i] = aux1 + aux2;
...
@@ 52,8 +52,6 @@ o[i] = aux1 + aux2;
done with this architecture
\cite
{
2015Appel,coqfaq
}
.
done with this architecture
\cite
{
2015Appel,coqfaq
}
.
\end{itemize}
\end{itemize}
\todo
{
NEW
}
\subheading
{
Corrections in TweetNaCl.
}
\subheading
{
Corrections in TweetNaCl.
}
As a result of this verification, we removed superfluous code.
As a result of this verification, we removed superfluous code.
Indeed indexes 17 to 79 of the
\TNaCle
{
i64 x[80]
}
intermediate variable of
Indeed indexes 17 to 79 of the
\TNaCle
{
i64 x[80]
}
intermediate variable of
...
@@ 73,20 +71,18 @@ and thus solved this problem.
...
@@ 73,20 +71,18 @@ and thus solved this problem.
o[i]
&
=0xffff;
o[i]
&
=0xffff;
\end{lstlisting}
\end{lstlisting}
\todo
{
NEW
}
Aside from the modifications above mentioned, all subsequent alteration
Aside from the modications above mentionned, all subsequent alteration
such as the type change of loop indexes (
\TNaCle
{
int
}
instead of
\TNaCle
{
i64
}
)
such as the type change of loop indexes (
\TNaCle
{
int
}
instead of
\TNaCle
{
i64
}
)
were required for VST to parse properly the code. We believe those
were required for VST to parse properly the code. We believe those
adjustments do not impact the trust of our proof.
adjustments do not impact the trust of our proof.
We contacted the authors of TweetNaCl and expect that the changes above
We contacted the authors of TweetNaCl and expect that the changes above
mention
n
ed will soon be integrated in a new version of the library.
mentioned will soon be integrated in a new version of the library.
\subheading
{
Extending our work.
}
\subheading
{
Extending our work.
}
The highlevel definition (
\sref
{
sec:maths
}
) can easily be ported to any
The highlevel definition (
\sref
{
sec:maths
}
) can easily be ported to any
other Montgomery curves and with it the proof of the ladder's correctness
other Montgomery curves and with it the proof of the ladder's correctness
assuming the same for
u
mlas are used.
assuming the same form
u
las are used.
In addition to the curve equation, the field
\F
{
p
}
would need to be redefined
In addition to the curve equation, the field
\F
{
p
}
would need to be redefined
as
$
p
=
2
^{
255
}

19
$
is hardcoded in order to speed up some proofs.
as
$
p
=
2
^{
255
}

19
$
is hardcoded in order to speed up some proofs.
...
@@ 97,7 +93,7 @@ level verification similar to \tref{thm:montgomeryladdercorrect}.
...
@@ 97,7 +93,7 @@ level verification similar to \tref{thm:montgomeryladdercorrect}.
The verification
\eg
X448~
\cite
{
cryptoeprint:2015:625,rfc7748
}
in C would
The verification
\eg
X448~
\cite
{
cryptoeprint:2015:625,rfc7748
}
in C would
require the adaptation of most of the low level arithmetic (mainly the
require the adaptation of most of the low level arithmetic (mainly the
multiplication, carry propagation
s
and reductions).
multiplication, carry propagation and reductions).
Once the correctness and bounds of the basic operations are established,
Once the correctness and bounds of the basic operations are established,
reproving the full ladder would make use of our generic definition and lower
reproving the full ladder would make use of our generic definition and lower
the workload.
the workload.
...
...
paper/A4_reviews.tex
View file @
374f9d0d
\newpage
\section
{
Prior reviews
}
\section
{
Prior reviews
}
\label
{
appendix:pastreviews
}
\label
{
appendix:pastreviews
}
...
@@ 90,8 +91,9 @@ It lies in the assurance gained by the formalization of the X25519 from RFC~7748
...
@@ 90,8 +91,9 @@ It lies in the assurance gained by the formalization of the X25519 from RFC~7748
and its correctness with respect to the theory of elliptic curves.
and its correctness with respect to the theory of elliptic curves.
It is the first time, we have a link from the C code up to the mathematical
It is the first time, we have a link from the C code up to the mathematical
definitions of Curve25519.
definitions of Curve25519.
We removed the description of how verification of for loops are handled and the
While they are part of the main proof but not novel techniques we removed the
details of the proof by reflections.
description of how verification of for loops are handled and the details of the
proof by reflections.
We described in the Conclusion (
\sref
{
sec:Conclusion
}
) how our results can be
We described in the Conclusion (
\sref
{
sec:Conclusion
}
) how our results can be
extended or reused in future works.
extended or reused in future works.
...
@@ 130,11 +132,11 @@ the body on conceptual insights (see comments below).
...
@@ 130,11 +132,11 @@ the body on conceptual insights (see comments below).
\end{center}
\end{center}
I was confused that you did not seem have found any errors in an implementation.
I was confused that you did not seem have found any errors in an implementation.
I can believe that the implementers of
[2]
are proficient implementers,
but I
I can believe that the implementers of
\cite
{
BGJ+15
}
are proficient implementers,
would have expected some minor bugs/parsing issues to be found anyway.
What is
but I
would have expected some minor bugs/parsing issues to be found anyway.
your explanation that you haven't found any issues?
What is
your explanation that you haven't found any issues?
p.1: You discuss
[10]
as using heavy annotation of code, differently from your
p.1: You discuss
\cite
{
Ber06
}
as using heavy annotation of code, differently from your
own code. However, as far as I understand, your Coq implementation must also be
own code. However, as far as I understand, your Coq implementation must also be
typeannotated. Thus, I imagine that the difference lies in whether SATsolvers
typeannotated. Thus, I imagine that the difference lies in whether SATsolvers
are used or not? This did not become very clear, because you mostly describe
are used or not? This did not become very clear, because you mostly describe
...
@@ 178,11 +180,12 @@ interesting if the paper highlights the interesting aspects of the verification.
...
@@ 178,11 +180,12 @@ interesting if the paper highlights the interesting aspects of the verification.
Related work:
Related work:
In reference [13], the order of authors is different than in the original
In reference
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
, the order of authors
publication. I think that you might want to discuss [13] in the Related work
is different than in the original publication. I think that you might want to
discuss
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
in the Related work
section, since it seems quite close. I was wondering whether you consider the
section, since it seems quite close. I was wondering whether you consider the
approach in
[13] as synthesis or verification, because to me, it seemed a
approach in
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
as synthesis or
mix/neither.
verification, because to me, it seemed a
mix/neither.
Clarification in intro:
Clarification in intro:
...
@@ 197,10 +200,8 @@ whether this is careful quantification or not.
...
@@ 197,10 +200,8 @@ whether this is careful quantification or not.
Clarification in intro: VST has already been used to verify symmetric Cryptographic
Clarification in intro: VST has already been used to verify symmetric Cryptographic
primities, as mentioned later by
\cite
{
Beringer2015VerifiedCA
}
and
\cite
{
2015Appel
}
.
primities, as mentioned later by
\cite
{
Beringer2015VerifiedCA
}
and
\cite
{
2015Appel
}
.
We have not found errors in the implementation but we removed an
We have not found errors in the implementation but we removed an undefined
undefined behavior by the C standard.
behavior by the C standard.
\todo
{
Can I say that?
}
Compilers were smart enough to prevent problems in that instance.
...
@@ 233,9 +234,9 @@ that uses X25519 is provably secure, based on some cryptographic assumption on
...
@@ 233,9 +234,9 @@ that uses X25519 is provably secure, based on some cryptographic assumption on
the ECDH construction. It is rare to find papers that combine more than one of
the ECDH construction. It is rare to find papers that combine more than one of
these proof levels, and this paper does a creditable job of linking (a) with (b),
these proof levels, and this paper does a creditable job of linking (a) with (b),
relying on the Coq framework to soundly glue these proofs together. Although a
relying on the Coq framework to soundly glue these proofs together. Although a
similar goal was considered in
[12]
, this paper provides
a more satisfying
similar goal was considered in
\cite
{
Zinzindohoue2016AVE
}
, this paper provides
solution by not leaving any gaps between the formalizations,
and by relying on a
a more satisfying
solution by not leaving any gaps between the formalizations,
smaller trusted computing base.
and by relying on a
smaller trusted computing base.
\begin{center}
\begin{center}
...
@@ 243,12 +244,13 @@ smaller trusted computing base.
...
@@ 243,12 +244,13 @@ smaller trusted computing base.
\end{center}
\end{center}
X25519 implementations have now been verifying in multiple papers using multiple
X25519 implementations have now been verifying in multiple papers using multiple
verification frameworks, and [18] even uses Coq to verify a large portion of a C
verification frameworks, and
\cite
{
Erbsen2016SystematicSO
}
even uses Coq to
implementation of X25519 fully automatically. So, the main contribution here is
verify a large portion of a C implementation of X25519 fully automatically.
that that the authors verify an existing popular implementation (TweetNaCl)
So, the main contribution here is that that the authors verify an existing
without making many changes to the source code. Still, TweetNaCl is not necessarily
popular implementation (TweetNaCl) without making many changes to the source
the most complex (and certainly not the most efficient) implementation of X25519
code. Still, TweetNaCl is not necessarily the most complex (and certainly not
that has been verified, which makes the novelty of this work hard to justify.
the most efficient) implementation of X25519 that has been verified, which
makes the novelty of this work hard to justify.
\begin{center}
\begin{center}
...
...
paper/_files.tex
View file @
374f9d0d
...
@@ 100,11 +100,11 @@
...
@@ 100,11 +100,11 @@
\texttt
{
clamp
}
&
\texttt
{
Low/Prep
\_
n.v
}
&
Clamping
\\
\texttt
{
clamp
}
&
\texttt
{
Low/Prep
\_
n.v
}
&
Clamping
\\
\texttt
{
Unpack25519
}
&
\texttt
{
Low/Unpack25519.v
}
&
unpacking (mod
$
2
^{
255
}$
)
\\
\texttt
{
Unpack25519
}
&
\texttt
{
Low/Unpack25519.v
}
&
unpacking (mod
$
2
^{
255
}$
)
\\
\hline
\hline
\multicolumn
{
3
}{
c
}{
Instan
c
iation
s
of
\texttt
{
Ops
}}
\\
\multicolumn
{
3
}{
c
}{
Instan
t
iation of
\texttt
{
Ops
}}
\\
\hline
\hline
\texttt
{
Z25519
\_
Ops
}
&
\texttt
{
Mid/Instances.v
}
&
Instan
c
iation
s
over
\F
{
p
}
with
$
p
=
\p
$
\\
\texttt
{
Z25519
\_
Ops
}
&
\texttt
{
Mid/Instances.v
}
&
Instan
t
iation over
\F
{
p
}
with
$
p
=
\p
$
\\
\texttt
{
Z
\_
Ops
}
&
\texttt
{
Mid/Instances.v
}
&
Instan
c
iation
s
over
$
\Zfield
$
\\
\texttt
{
Z
\_
Ops
}
&
\texttt
{
Mid/Instances.v
}
&
Instan
t
iation over
$
\Zfield
$
\\
\texttt
{
List
\_
Z
\_
Ops
}
&
\texttt
{
Mid/Instances.v
}
&
Instan
c
iation
s
lists of
\Z
\\
\texttt
{
List
\_
Z
\_
Ops
}
&
\texttt
{
Mid/Instances.v
}
&
Instan
t
iation lists of
\Z
\\
\hline
\hline
\multicolumn
{
3
}{
c
}{
X25519 over
\Z
and list of
\Z
}
\\
\multicolumn
{
3
}{
c
}{
X25519 over
\Z
and list of
\Z
}
\\
\hline
\hline
...
...
paper/tikz/highlevel1.tex
View file @
374f9d0d
...
@@ 20,14 +20,14 @@
...
@@ 20,14 +20,14 @@
% M is a finite assoc group
% M is a finite assoc group
\begin{scope}
[yshift=0 cm,xshift=3 cm]
\begin{scope}
[yshift=0 cm,xshift=3 cm]
\draw
[fill=green!20] (0,0)  (3.25,0)  (3.25,0.75)  (0, 0.75)  cycle;
\draw
[fill=green!20] (0,0)  (3.25,0)  (3.25,0.75)  (0, 0.75)  cycle;
\draw
(1.675,0.375) node[textstyle, anchor=center]
{$
M
_{
a,b
}
(
\K
)
$
is an Assoc. Fin. Grp
}
;
\draw
(1.675,0.375) node[textstyle, anchor=center]
{$
M
_{
a,b
}
(
\K
)
$
is an Assoc. Fin. Grp
.
}
;
\end{scope}
\end{scope}
% Hypothesis x square is not 2
% Hypothesis x square is not 2
\begin{scope}
[yshift=1.5 cm,xshift=0 cm]
\begin{scope}
[yshift=1.5 cm,xshift=0 cm]
\draw
[fill=orange!20] (0,0)  (1.5,0)  (1.5,1.25)  (0, 1.25)  cycle;
\draw
[fill=orange!20] (0,0)  (1.5,0)  (1.5,1.25)  (0, 1.25)  cycle;
\draw
(0,0) node[textstyle, anchor=north west]
{
\textbf
{
Hyp:
}}
;
\draw
(0,0) node[textstyle, anchor=north west]
{
\textbf
{
Hyp:
}}
;
\draw
(0.75,0.375) node[textstyle, anchor=north]
{$
\forall
x
\in
\K
,
$
\\
$
x
^
2
\neq
2
$}
;
\draw
(0.75,0.375) node[textstyle, anchor=north]
{$
\forall
x
\in
\K
,
$
\\
$
x
^
2
\neq
a
^
2

4
$}
;
\end{scope}
\end{scope}
% Final theorem
% Final theorem
...
...
paper/tikz/highlevel2.tex
View file @
374f9d0d
...
@@ 13,25 +13,31 @@
...
@@ 13,25 +13,31 @@
\end{scope}
\end{scope}
\begin{scope}
[yshift=1 cm,xshift=1.5 cm]
\begin{scope}
[yshift=1 cm,xshift=1.5 cm]
\draw
[fill=green!20]
(0,0)  (1.25,0)  (1.25,0.75)  (0, 0.75)  cycle;
\draw
(0.615,0.375) node[textstyle, anchor=center]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
x
^
2
\neq
2
$}
;
\end{scope}
\begin{scope}
[yshift=1 cm,xshift=2.875 cm]
\draw
[fill=green!20]
(0,0)  (1.5,0)  (1.5,0.75)  (0, 0.75)  cycle;
\draw
[fill=green!20]
(0,0)  (1.5,0)  (1.5,0.75)  (0, 0.75)  cycle;
\draw
(0.75,0.375) node[textstyle, anchor=center]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
x
^
2
\neq
2
$}
;
\draw
(0.75,0.375) node[textstyle, anchor=center]
{$
\forall
x
\in
\F
{
p
}
,
$
\\
$
x
^
2
\neq
a
^
2

4
$}
;
\end{scope}
\end{scope}
\begin{scope}
[yshift=1 cm,xshift=4 cm]
\begin{scope}
[yshift=1 cm,xshift=4
.5
cm]
\draw
[fill=white]
(0,0)  (1
.5
,0)  (1
.5
,0.75)  (0, 0.75)  cycle;
\draw
[fill=white]
(0,0)  (1,0)  (1,0.75)  (0, 0.75)  cycle;
\draw
(0.
7
5,0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
}
)
$}
;
\draw
(0.5,0.375) node[textstyle, anchor=center]
{$
C
(
\F
{
p
}
)
$}
;
\end{scope}
\end{scope}