Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coqveriftweetnacl
Commits
5c5ac275
Commit
5c5ac275
authored
Jan 20, 2021
by
Peter Schwabe
Browse files
Edits in intro and preliminaries towards the cameraready version
parent
fc994792
Changes
4
Hide whitespace changes
Inline
Sidebyside
paper/abstract.tex
View file @
5c5ac275
...
...
@@ 7,7 +7,7 @@
Bernstein's 2006 paper, as standardized in RFC~7748,
as well as the absence of undefined behavior
like arithmetic overflows
and array out
of
bounds errors.
and array out

of

bounds errors.
We also formally prove, based on the work of Bartzia and Strub,
that X25519 is mathematically correct, i.e.,
that it correctly computes scalar multiplication on
...
...
paper/intro.tex
View file @
5c5ac275
...
...
@@ 15,7 +15,7 @@ prove correctness of any of the primitives implemented by the library.
One core component of TweetNaCl (and NaCl) is the keyexchange protocol X25519 presented
by Bernstein in~
\cite
{
Ber06
}
.
This protocol is standardized in RFC~7748 and used by a wide variety of applications~
\cite
{
thingsthatusecurve25519
}
such as SSH, Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over
such as SSH,
the
Signal Protocol, Tor, Zcash, and TLS to establish a shared secret over
an insecure channel.
The X25519 keyexchange protocol is an
\xcoord
only
ellipticcurve DiffieHellman key exchange using the Montgomery
...
...
@@ 25,7 +25,7 @@ but Bernstein suggested to rename the protocol to X25519 and to use the name
Curve25519 for the underlying elliptic curve~
\cite
{
Ber14
}
.
We use this updated terminology in this paper.
\subheading
{
Contribution of this paper.
}
\subheading
{
Contribution
s
of this paper.
}
In short, in this paper we provide a computerverified proof that the
X25519 implementation in TweetNaCl matches the mathematical definition
of the function given in~
\cite
[Sec.~2]
{
Ber06
}
.
...
...
@@ 113,7 +113,7 @@ In~\cite{Zinzindohoue2016AVE}, Zinzindohou{\'{e}}, Bartzia, and Bhargavan
describe a verified extensible library of elliptic curves~ in F*~
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
.
This served as ground work for the cryptographic library HACL*~
\cite
{
zinzindohoue2017hacl
}
used in the NSS suite from Mozilla. The approach they use is a combination
of proving and synthesi
s
ing: A fairly lowlevel implementation written in
of proving and synthesi
z
ing: A fairly lowlevel implementation written in
Low
$^
*
$
is proven to be equivalent to a highlevel specification in F
$^
*
$
.
The Low
$^
*
$
code is then compiled to C using an unverified and thus trusted
compiler called Kremlin.
...
...
@@ 148,7 +148,7 @@ structure of finite field and elliptic curves the actual proofs are quite differ
\subheading
{
Reproducing the proofs.
}
To maximize reusability of our results we place the code of our formal proof
presented in this paper into the public domain.
It is available at
\url
{
http://doi.org/10.5281/zenodo.4439686
}
It is available at
\url
{
http
s
://doi.org/10.5281/zenodo.4439686
}
with instructions of how to compile and verify our proof.
A description of the content of the code archive is provided in
Appendix~
\ref
{
appendix:prooffolders
}
.
...
...
@@ 157,10 +157,10 @@ Appendix~\ref{appendix:prooffolders}.
\sref
{
sec:preliminaries
}
gives the necessary background on Curve25519 and X25519
implementations and a brief explanation of how formal verification works.
\sref
{
sec:CoqRFC
}
provides our Coq formalization of X25519 as specified in RFC~7748~
\cite
{
rfc7748
}
.
\sref
{
sec:CCoq
}
provide
s the specifications of X25519 in TweetNaCl and some of the
\sref
{
sec:CCoq
}
detail
s the specifications of X25519 in TweetNaCl and some of the
proof techniques used to show the correctness with respect to RFC~7748~
\cite
{
rfc7748
}
.
\sref
{
sec:maths
}
describes our extension of the formal library by Bartzia
and Strub and the correctness of X25519 implementation with respect to Bernstein's
and Strub and the
proof of
correctness of
the
X25519 implementation with respect to Bernstein's
specifications~
\cite
{
Ber14
}
.
Finally in
\sref
{
sec:Conclusion
}
we discuss the trusted code base of our proofs
and conclude with some lessons learned about TweetNaCl and with sketching the
...
...
@@ 170,12 +170,12 @@ effort required to extend our work to other ellipticcurve software.
C source files are represented by
{
\color
{
doc@lstfunctions
}
.C
}
while
{
\color
{
doc@lstfunctions
}
.V
}
corresponds to Coq files.
In a nutshell, we formalize X25519 into a Coq function
\texttt
{
RFC
}
,
and we write a specification in
S
eparation logic with VST.
The first step of CompCert compilation (clightgen) is used to translate
s
and we write a specification in
s
eparation logic with VST.
The first step of CompCert compilation (clightgen) is used to translate
the C source code into a DSL in Coq (CLight). By using VST,
we step through the translated instructions and verify that the program satisfies the specifications.
Additionally we formally define the scalar multiplication over elliptic curves and show that,
under the same preconditions as used in the specification,
\texttt
{
RFC
}
computes the desired results
under the same preconditions as used in the specification,
\texttt
{
RFC
}
computes the desired results
.
\begin{figure}
[h]
\centering
...
...
paper/preliminaries.tex
View file @
5c5ac275
...
...
@@ 32,7 +32,7 @@ are isomorphic via $(x,y) \mapsto (x, \sqrt{b/b'} \cdot y)$.
a curve that is isomorphic over
$
\F
{
p
^
2
}$
~
\cite
{
cryptoeprint:2017:212
}
.
\end{dfn}
Points in
$
M
_{
a,b
}
(
\K
)
$
can be equipped with a structure of a
n
commutative group
Points in
$
M
_{
a,b
}
(
\K
)
$
can be equipped with a structure of a commutative group
with the addition operation
$
+
$
and with neutral element the point at infinity
$
\Oinf
$
.
For a point
$
P
\in
M
_{
a,b
}
(
\K
)
$
and a positive integer
$
n
$
we obtain the scalar product
$$
n
\cdot
P
=
\underbrace
{
P
+
\cdots
+
P
}_{
n
\text
{
times
}}
.
$$
...
...
@@ 51,7 +51,7 @@ We define the operation:
&
((X
_{
2
\cdot
P
}
:Z
_{
2
\cdot
P
}
), (X
_{
P + Q
}
:Z
_{
P + Q
}
))
\end{align*}
A pseudocode description of the Montgomery ladder
A pseudocode description of the Montgomery ladder
using this
\texttt
{
xDBL
\&
ADD
}
routine
is given in Algorithm~
\ref
{
alg:montgomeryladder
}
.
The main loop iterates over the bits of the scalar
$
n
$
.
The
$
k
^{
\text
{
th
}}$
iteration conditionally swaps
...
...
@@ 62,9 +62,6 @@ function while keeping the same body of the loop. \label{cswap}
Given a pair
$
(
P
_
0
, P
_
1
)
$
and a bit
$
b
$
,
\texttt
{
CSWAP
}
returns the pair
$
(
P
_
b, P
_{
1

b
}
)
$
.
By using the differential addition and doubling operations we define the Montgomery ladder
computing a
\xcoord
only scalar multiplication (see
\aref
{
alg:montgomeryladder
}
).
% \setlength{\textfloatsep}{1em}
\begin{algorithm}
\caption
{
Montgomery ladder for scalar mult.
}
...
...
@@ 98,13 +95,13 @@ The core of the X25519 keyexchange protocol is a scalar\hyp{}multiplication
function, which we will also refer to as X25519.
This function receives as input two arrays of
$
32
$
bytes each.
One of them is interpreted as the littleendian encoding of a
nonnegative 256bit integer
$
n
$
(see
\ref
{
sec:CoqRFC
}
).
nonnegative 256bit integer
$
n
$
(see
Section~
\ref
{
sec:CoqRFC
}
).
The other is interpreted as the littleendian encoding of
the
\xcoord
$
x
_
P
\in
\F
{
p
}$
of a point in
$
E
(
\F
{
p
^
2
}
)
$
,
using the standard mapping of integers modulo
$
p
$
to elements in
$
\F
{
p
}$
.
The X25519 function first computes a scalar
$
n'
$
from
$
n
$
by setting
bits at position 0, 1, 2 and 255 to
\texttt
{
0
}
; and at position 254
bits at position
s
0, 1, 2 and 255 to
\texttt
{
0
}
; and at position 254
to
\texttt
{
1
}
.
This operation is often called ``clamping'' of the scalar
$
n
$
.
Note that
$
n'
\in
2
^{
254
}
+
8
\{
0
,
1
,
\ldots
,
2
^{
251
}

1
\}
$
.
...
...
@@ 171,7 +168,7 @@ and squaring (\TNaCle{S}). After a multiplication, limbs of the result
\texttt
{
o
}
are too large to be used again as input. Two calls to
\TNaCle
{
car25519
}
at the end of
\TNaCle
{
M
}
takes care of the carry propagation.
Inverses in
$
\Ffield
$
are computed
with
\TNaCle
{
inv25519
}
.
Inverses in
$
\Ffield
$
are computed
in
\TNaCle
{
inv25519
}
.
This function uses exponentiation by
$
p

2
=
2
^{
255
}

21
$
,
computed with the squareandmultiply algorithm.
...
...
@@ 188,8 +185,8 @@ This function is considerably more complex as it needs to convert
to a
\emph
{
unique
}
representation, i.e., also fully reduce modulo
$
p
$
and remove the redundancy of the radix
$
2
^{
16
}$
representation.
The C definitions of th
o
se functions are available in
Appendix
\ref
{
verifiedCanddiff
}
.
The C definitions of
all
th
e
se functions are available in
Appendix
~
\ref
{
verifiedCanddiff
}
.
\subheading
{
The Montgomery ladder.
}
With these lowlevel arithmetic and helper functions defined,
...
...
@@ 247,8 +244,9 @@ int crypto_scalarmult(u8 *q,
}
\end{lstlisting}
Note that lines 10
\&
11 represent the ``clamping'' operation.
Note that lines 10
\&
11 represent the ``clamping'' operation;
the sequence of arithmetic operations in lines 22 through 39 implement the
\texttt
{
xDBL
\&
ADD
}
routine.
\subsection
{
Coq, separation logic, and VST
}
\label
{
subsec:CoqVST
}
...
...
@@ 280,8 +278,10 @@ For example, here is the rule for sequential composition:
\BinaryInfC
{$
\{
P
\}
C
_
1
;C
_
2
\{
R
\}
$}
\end{prooftree}
Separation logic is an extension of Hoare logic which allows reasoning about
pointers and memory manipulation. This logic enforces strict conditions on the
memory shared such as being disjoint.
pointers and memory manipulation.
%This logic enforces strict conditions on the memory shared such as being disjoint.
%Separation logic requires memory regions of different function arguments to be disjoint.
Reasoning in separation logic assumes that certain memory regions are nonoverlapping
We discuss this limitation further in
\sref
{
subsec:withVST
}
.
The Verified Software Toolchain (VST)~
\cite
{
cao2018vstfloyd
}
is a framework
...
...
@@ 289,8 +289,8 @@ which uses separation logic (proven correct with respect to CompCert semantics)
to prove the functional correctness of C programs.
The first step consists of translating the source code into Clight,
an intermediate representation used by CompCert.
For
such
purpose
on
e use
s
the parser of CompCert called
\texttt
{
clightgen
}
.
For
this
purpose
w
e use the parser of CompCert called
\texttt
{
clightgen
}
.
In a second step one defines the Hoare triple representing the specification of
the piece of software one wants to prove.
Then using VST, one uses a strongest
postcondition approach to prove the correctness of the triple.
the piece of software one wants to prove.
With the help of VST
we then use the strongest
postcondition approach to prove the correctness of the triple.
This can be seen as a forward symbolic execution of the program.
paper/tweetverif.tex
View file @
5c5ac275
...
...
@@ 23,10 +23,8 @@
\ifpublic
\author
{
\IEEEauthorblockN
{
Peter Schwabe
}
\IEEEauthorblockA
{
Max Planck Institute for Security and Privacy,
\\
Germany
\&\\
Radboud University
\\
The Netherlands
}
\IEEEauthorblockA
{
MPISP, Germany
\&\\
Radboud University, The Netherlands
}
\and
\IEEEauthorblockN
{
Beno
\^
it Viguier
}
\IEEEauthorblockA
{
Radboud University,
\\
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment