Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Benoit Viguier
coq-verif-tweetnacl
Commits
b8792cdc
Commit
b8792cdc
authored
Oct 01, 2019
by
Benoit Viguier
Browse files
some more fixes
parent
78b21d53
Changes
3
Hide whitespace changes
Inline
Side-by-side
paper/0_abstract.tex
View file @
b8792cdc
...
@@ -10,10 +10,10 @@
...
@@ -10,10 +10,10 @@
and array out of bounds errors.
and array out of bounds errors.
We also formally prove, based on the work of Bartzia and Strub,
We also formally prove, based on the work of Bartzia and Strub,
that X25519 is mathematically correct, i.e.,
that X25519 is mathematically correct, i.e.,
that it correctly computes scalar multiplication on
that it correctly computes scalar multiplication on
the elliptic curve Curve25519.
the elliptic curve Curve25519.
The proofs are all computer-verified using the Coq theorem prover.
The proofs are all computer-verified using the Coq theorem prover.
To establish the link between C and Coq we use the
To establish the link between C and Coq we use the
Verified Software Toolchain (VST).
Verified Software Toolchain (VST).
\end{abstract}
\end{abstract}
paper/2_preliminaries.tex
View file @
b8792cdc
...
@@ -195,8 +195,10 @@ sv M(gf o,const gf a,const gf b) {
...
@@ -195,8 +195,10 @@ sv M(gf o,const gf a,const gf b) {
}
}
\end{lstlisting}
\end{lstlisting}
After the actual multiplication, the limbs of the result
\texttt
{
o
}
are
After the multiplication, the limbs of the result
\texttt
{
o
}
are
too large to be used again as input, which is why the two calls to
too large to be used again as input.
% which is why
The two calls to
\TNaCle
{
car25519
}
at the end of
\TNaCle
{
M
}
propagate the carries through the limbs:
\TNaCle
{
car25519
}
at the end of
\TNaCle
{
M
}
propagate the carries through the limbs:
\begin{lstlisting}
[language=Ctweetnacl]
\begin{lstlisting}
[language=Ctweetnacl]
sv car25519(gf o)
sv car25519(gf o)
...
...
paper/4_lowlevel.tex
View file @
b8792cdc
...
@@ -186,41 +186,41 @@ is enough for our needs.
...
@@ -186,41 +186,41 @@ is enough for our needs.
% This is not the case here: you compute idx 255 before 254...
% This is not the case here: you compute idx 255 before 254...
% Can we shorten the next paragraph?
% Can we shorten the next paragraph?
\subheading
{
Verifying
\texttt
{
for
}
loops.
}
%
\subheading{Verifying \texttt{for} loops.}
Final states of
\texttt
{
for
}
loops are usually computed by simple recursive functions.
%
Final states of \texttt{for} loops are usually computed by simple recursive functions.
However, we must define invariants which are true for each iteration step.
%
However, we must define invariants which are true for each iteration step.
%
Assume that we want to prove a decreasing loop where indexes go from 3 to 0.
%
Assume that 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
%
Define a function $g : \N \rightarrow State \rightarrow State $ which takes as
input an integer for the index and a state, then returns a state.
%
input an integer for the index and a state, then returns a state.
It simulates the body of the
\texttt
{
for
}
loop.
%
It simulates the body of the \texttt{for} loop.
Define the recursion:
$
f :
\N
\rightarrow
State
\rightarrow
State
$
which
%
Define the recursion: $f : \N \rightarrow State \rightarrow State $ which
iteratively applies
$
g
$
with decreasing index:
%
iteratively applies $g$ with decreasing index:
\begin{equation*}
%
\begin{equation*}
f ( i , s ) =
%
f ( i , s ) =
\begin{cases}
%
\begin{cases}
s
&
\text
{
if
}
s = 0
\\
%
s & \text{if } s = 0 \\
f( i - 1 , g ( i - 1 , s ))
&
\text
{
otherwise
}
%
f( i - 1 , g ( i - 1 , s )) & \text{otherwise}
\end{cases}
%
\end{cases}
\end{equation*}
%
\end{equation*}
Then we have:
%
Then we have:
\begin{align*}
%
\begin{align*}
f(4,s)
&
= g(0,g(1,g(2,g(3,s))))
%
f(4,s) &= g(0,g(1,g(2,g(3,s))))
\end{align*}
%
\end{align*}
To prove the correctness of
$
f
(
4
,s
)
$
, we need to prove that intermediate steps
%
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.
%
$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
%
Due to the computation order of recursive function, our loop invariant for
$
i
\in\{
0
,
1
,
2
,
3
,
4
\}
$
cannot use
$
f
(
i
)
$
.
%
$i\in\{0,1,2,3,4\}$ cannot use $f(i)$.
To solve this, we define an auxiliary function with an accumulator such that
%
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.
%
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
%
We then prove for the complete number of steps, the function with the accumulator
and without returns the same result.
%
and without returns the same result.
We formalized this result in a generic way in Appendix~
\ref
{
subsubsec:for
}
.
%
We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
%
Using this formalization, we prove that the 255 steps of the Montgomery ladder
%
Using this formalization, we prove that the 255 steps of the Montgomery ladder
in C provide the same computations as in
\coqe
{
RFC
}
.
%
in C provide the same computations as in \coqe{RFC}.
%
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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