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
7faffc34
Commit
7faffc34
authored
Jul 22, 2019
by
Benoit Viguier
Browse files
improve Preliminaries + correct typos
parent
b16f57e0
Changes
1
Hide whitespace changes
Inline
Sidebyside
paper/preliminaries.tex
View file @
7faffc34
...
@@ 7,38 +7,39 @@ We then provide a brief description of the formal tools we use in our proofs.
...
@@ 7,38 +7,39 @@ We then provide a brief description of the formal tools we use in our proofs.
\subsection
{
The X25519 key exchange
}
\subsection
{
The X25519 key exchange
}
\label
{
preliminaries:A
}
\label
{
preliminaries:A
}
% \begin{definition}
% Let $E$ be the elliptic curve defined by $y^2 = x^3 + 486662 x^2 + x$.
% \end{definition}
% \begin{lemma}
% For any value $x \in \F{p}$, for the elliptic curve $E$ over $\F{p^2}$
% defined by $y^2 = x^3 + 486662 x^2 + x$, there exist a point $P$ over $E(\F{p^2})$
% \end{lemma}
For any value
$
x
\in
\F
{
p
}$
, for the elliptic curve
$
E
$
over
$
\F
{
p
^
2
}$
For any value
$
x
\in
\F
{
p
}$
, for the elliptic curve
$
E
$
over
$
\F
{
p
^
2
}$
defined by
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
, there exist a point
$
P
$
over
$
E
(
\F
{
p
^
2
}
)
$
defined by
$
y
^
2
=
x
^
3
+
486662
x
^
2
+
x
$
, there exist a point
$
P
$
over
$
E
(
\F
{
p
^
2
}
)
$
such that
$
x
$
is the
$
x
$
coordinate of
$
P
$
. Remark that
$
x
$
is also the
$
x
$
coordinate of
$

P
$
.
such that
$
x
$
is the
$
x
$
coordinate of
$
P
$
. Remark that
$
x
$
is also the
$
x
$
coordinate of
$

P
$
.
Given a natural number
$
n
$
and
$
x
$
, X25519 returns the
$
x
$
coordinate of the
Given a natural number
$
n
$
and
$
x
$
, X25519 returns the
$
x
$
coordinate of the
scalar multiplication of
$
P
$
by
$
n
$
. Note that the result would is the same with
$

P
$
.
scalar multiplication of
$
P
$
by
$
n
$
, thus
$
[
n
]
P
$
. Note that the result is the
same with
$
[
n
](
P
)
=
[
n
]
P
$
.
Using X25519,
RFC~7748~
\cite
{
rfc7748
}
formalized
a
Diffie–Hellman keyexchange algorithm.
RFC~7748~
\cite
{
rfc7748
}
formalized
the X25519
Diffie–Hellman keyexchange algorithm.
E
ach party generate a secret random number
$
S
_
a
$
(respectively
$
S
_
b
$
), and computes
$
P
_
a
$
(respectively
$
P
_
b
$
),
Given the base point
$
B
$
where
$
x
=
9
$
, e
ach party generate a secret random number
the resulting
$
x
$
coordinate of the scalar multiplication of the base poin
t
$
s
_
a
$
(respectively
$
s
_
b
$
), and computes
$
P
_
a
$
(respectively
$
P
_
b
$
), the resul
t
where
$
x
=
9
$
and
$
S
_
a
$
(respectively
$
S
_
b
$
).
of the scalar multiplication between
$
B
$
and
$
s
_
a
$
(respectively
$
s
_
b
$
).
The party exchanges
$
P
_
a
$
and
$
P
_
b
$
and computes their shared secret with X25519
The party exchanges
$
P
_
a
$
and
$
P
_
b
$
and computes their shared secret with X25519
over
$
S
_
a
$
and
$
P
_
b
$
(respectively
$
S
_
b
$
and
$
P
_
a
$
).
over
$
s
_
a
$
and
$
P
_
b
$
(respectively
$
s
_
b
$
and
$
P
_
a
$
).
\subsection
{
X25519 in TweetNaCl
}
\subsection
{
X25519 in TweetNaCl
}
\label
{
preliminaries:B
}
\label
{
preliminaries:B
}
\subheading
{
Arithmetic in
\Ffield
}
In X25519, all computations are done over
$
\F
{
p
}$
.
In order to gain space, TweetNaCl uses a few shortcuts.
Numbers in that field can be represented with 256 bits.
\begin{lstlisting}
[language=Ctweetnacl]
We represent them in 8bit limbs (respectively 16bit limbs),
#define FOR(i,n) for (i = 0;i < n;++i)
making use of a base
$
2
^
8
$
(respectively
$
2
^{
16
}$
).
#define sv static void
Consequently, inputs of the X25519 function are seen as arrays of bytes
typedef unsigned char u8;
in a littleendian format.
\end{lstlisting}
Computations inside this function makes use of the 16bit limbs representation.
The subsequent blocks of code are valid C.
\subheading
{
Arithmetic in
\Ffield
.
}
In X25519, all computations are done over
$
\F
{
p
}$
.
Numbers in that field can be represented with 256 bits packed in 8bit limbs
(respectively 16bit limbs), making use of a base
$
2
^
8
$
(respectively
$
2
^{
16
}$
).
Consequently, inputs of the X25519 function are seen as bytes arrays in littleendian format.
Computations inside the crypto scalar multiplication and intermediates function
makes use of the 16bit limbs representation.
Those are placed into 64bits signed container in order to mitigate overflows or underflows.
Those are placed into 64bits signed container in order to mitigate overflows or underflows.
\begin{lstlisting}
[language=Ctweetnacl]
\begin{lstlisting}
[language=Ctweetnacl]
typedef long long i64;
typedef long long i64;
...
@@ 115,7 +116,7 @@ It first performs 3 carry propagations in order to guarantee
...
@@ 115,7 +116,7 @@ It first performs 3 carry propagations in order to guarantee
that each 16bit limbs values are between
$
0
$
and
$
2
^{
16
}$
.
that each 16bit limbs values are between
$
0
$
and
$
2
^{
16
}$
.
Then computes a modulo reduction by
$
\p
$
using iterative substraction and
Then computes a modulo reduction by
$
\p
$
using iterative substraction and
conditional swapping. This guarantees a unique representation in
$
\Zfield
$
.
conditional swapping. This guarantees a unique representation in
$
\Zfield
$
.
After which
each 16bit limbs are splitted into 8bit limbs.
Then,
each 16bit limbs are splitted into 8bit limbs.
\begin{lstlisting}
[language=Ctweetnacl]
\begin{lstlisting}
[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
sv pack25519(u8 *o,const gf n)
{
{
...
@@ 144,13 +145,13 @@ sv pack25519(u8 *o,const gf n)
...
@@ 144,13 +145,13 @@ sv pack25519(u8 *o,const gf n)
}
}
\end{lstlisting}
\end{lstlisting}
\subheading
{
The Montgomery ladder
}
\subheading
{
The Montgomery ladder
.
}
In order to compute scalar multiplication
s
, X25519 uses the Montgomery
In order to compute scalar multiplication, X25519 uses the Montgomery
$
x
$
coordinate doubleandadd formulas.
$
x
$
coordinate doubleandadd formulas.
First extract and clamp the value of
$
n
$
. Then unpack the value of
$
p
$
.
First extract and clamp the value of
$
n
$
. Then unpack the value of
$
p
$
.
As per RFC~7748~
\cite
{
rfc7748
}
, set its most significant bit to 0.
As per RFC~7748~
\cite
{
rfc7748
}
, set its most significant bit to 0.
Finally compute the Montgomery ladder over the clamped
$
n
$
and
$
p
$
,
Finally compute the Montgomery ladder over the clamped
$
n
$
and
$
p
$
,
pack the result into
$
q
$
.
and
pack the result into
$
q
$
.
\begin{lstlisting}
[language=Ctweetnacl]
\begin{lstlisting}
[language=Ctweetnacl]
int crypto
_
scalarmult(u8 *q,
int crypto
_
scalarmult(u8 *q,
const u8 *n,
const u8 *n,
...
@@ 208,15 +209,16 @@ int crypto_scalarmult(u8 *q,
...
@@ 208,15 +209,16 @@ int crypto_scalarmult(u8 *q,
Coq~
\cite
{
coqfaq
}
is an interactive theorem prover. It provides an expressive
Coq~
\cite
{
coqfaq
}
is an interactive theorem prover. It provides an expressive
formal language to write mathematical definitions, algorithms and theorems coupled
formal language to write mathematical definitions, algorithms and theorems coupled
with their proofs. As opposed to other systems such as F*~
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
,
with their proofs. As opposed to other systems such as F*~
\cite
{
DBLP:journals/corr/BhargavanDFHPRR17
}
,
Coq does not rely on the trust of
a
SMT solver. It uses its type
Coq does not rely on the trust of
an
SMT solver. It uses its type
system to verify the applications of hypothesis, lemmas
,
theorems~
\cite
{
Howard1995HOWTFN
}
.
system to verify the applications of hypothesis, lemmas
and
theorems~
\cite
{
Howard1995HOWTFN
}
.
The
Hoare logic is a formal system which allows
to
reason about programs.
Hoare logic is a formal system which allows reason
ing
about programs.
It uses trip
p
les such as
It uses triples such as
$$
\{
{
\color
{
doc@lstnumbers
}
\textbf
{
Pre
}}
\}\texttt
{
~Prog~
}
\{
{
\color
{
doc@lstdirective
}
\textbf
{
Post
}}
\}
$$
$$
\{
{
\color
{
doc@lstnumbers
}
\textbf
{
Pre
}}
\}\texttt
{
~Prog~
}
\{
{
\color
{
doc@lstdirective
}
\textbf
{
Post
}}
\}
$$
where
${
\color
{
doc@lstnumbers
}
\textbf
{
Pre
}}$
and
${
\color
{
doc@lstdirective
}
\textbf
{
Post
}}$
where
${
\color
{
doc@lstnumbers
}
\textbf
{
Pre
}}$
and
${
\color
{
doc@lstdirective
}
\textbf
{
Post
}}$
are assertions and
\texttt
{
Prog
}
is a piece of Code.
are assertions and
\texttt
{
Prog
}
is a piece of code.
It is read as ``when the precondition
$
Pre
$
is met, executing
\texttt
{
Prog
}
while yield to postcondition
$
Post
$
''.
It is read as ``when the precondition
$
Pre
$
is met, executing
\texttt
{
Prog
}
will
yield postcondition
$
Post
$
''.
We use compositional rules to prove the truth value of a Hoare tripple.
We use compositional rules to prove the truth value of a Hoare tripple.
For example, here is the rule for sequential composition:
For example, here is the rule for sequential composition:
\begin{prooftree}
\begin{prooftree}
...
@@ 225,10 +227,10 @@ For example, here is the rule for sequential composition:
...
@@ 225,10 +227,10 @@ For example, here is the rule for sequential composition:
\LeftLabel
{
HoareSeq
}
\LeftLabel
{
HoareSeq
}
\BinaryInfC
{$
\{
P
\}
C
_
1
;C
_
2
\{
R
\}
$}
\BinaryInfC
{$
\{
P
\}
C
_
1
;C
_
2
\{
R
\}
$}
\end{prooftree}
\end{prooftree}
Separation
L
ogic is an extension of
the
Hoare logic which allows
to
reason about
Separation
l
ogic is an extension of Hoare logic which allows reason
ing
about
pointers and memory manipulation. This
provides the
strict condition
that considered
pointers and memory manipulation. This
logic enforces
strict condition
s on the
memory share
s are disjoint, forcing nonalias
in
g
. We discuss
further about
this limitation in Section~
\ref
{
usingVST
}
.
memory share
d such as being disjo
in
t
. We discuss this limitation
further
in Section~
\ref
{
usingVST
}
.
The Verified Software Toolchain (VST)~
\cite
{
cao2018vstfloyd
}
is a framework which uses
The Verified Software Toolchain (VST)~
\cite
{
cao2018vstfloyd
}
is a framework which uses
the
Separation logic to prove the functional correctness of C programs.
Separation logic to prove the functional correctness of C programs.
It
s
can be seen as a forward symbolic execution of the program.
It can be seen as a forward symbolic execution of the program.
Its uses a strongest postcondition approach to prove that a
code
matches its specification.
Its uses a strongest postcondition approach to prove that a
program
matches its specification.
Write
Preview
Supports
Markdown
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