lowlevel.tex 26.4 KB
Newer Older
1
\section{Proving equivalence of X25519 in C and Coq}
Benoit Viguier's avatar
Benoit Viguier committed
2
\label{sec:C-Coq-RFC}
Benoit Viguier's avatar
Benoit Viguier committed
3

Benoit Viguier's avatar
Benoit Viguier committed
4
In this section we prove the following theorems:
Benoit Viguier's avatar
Benoit Viguier committed
5
\begin{theorem}
Benoit Viguier's avatar
Benoit Viguier committed
6
\label{thm:VST}
Benoit Viguier's avatar
Benoit Viguier committed
7
The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches our
8
functional specification in Coq.
Benoit Viguier's avatar
Benoit Viguier committed
9
10
\end{theorem}

Benoit Viguier's avatar
Benoit Viguier committed
11
12
13
14
\begin{theorem}
\label{thm:RFC}
Our functional specification in Coq matches the specifications of RFC~7748~\cite{rfc7748}.
\end{theorem}
15

Benoit Viguier's avatar
Benoit Viguier committed
16
We first describe the global structure of our proof (\ref{subsec:proof-structure}).
17
Then we introduce our specification, we specify the Hoare triple and prove it
Benoit Viguier's avatar
Benoit Viguier committed
18
19
correct with VST (\tref{thm:VST}).
Then we discuss techniques used to prove equivalence of operations between
20
21
different number representations,
proving the equivalence with the RFC (\tref{thm:RFC}).
Benoit Viguier's avatar
Benoit Viguier committed
22

Benoit Viguier's avatar
Benoit Viguier committed
23
24
25
26




Benoit Viguier's avatar
Benoit Viguier committed
27
28
29
30
31
32
33
34
35
36
37
\subsection{Structure of our proof}
\label{subsec:proof-structure}

In order to prove the correctness of X25519 in TweetNaCl code \TNaCle{crypto_scalarmult},
we use VST to prove that the code matches our functional Coq specification of \Coqe{Crypto_Scalarmult}
(sometimes abbreviated as \Coqe{CSM}). Then, we prove that our specification of the scalar
multiplication matches the mathematical definition of elliptic curves and Theorem 2.1 by
Bernstein~\cite{Ber06} (\tref{thm:Elliptic-CSM}).
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs considered.
The mathematical proof of our specification is presented
in \sref{sec:maths}.
Benoit Viguier's avatar
Benoit Viguier committed
38
\begin{figure}[h]
Benoit Viguier's avatar
Benoit Viguier committed
39
  \centering
Benoit Viguier's avatar
Benoit Viguier committed
40
  \include{tikz/proof}
Benoit Viguier's avatar
Benoit Viguier committed
41
  \caption{Overview of the proof}
Benoit Viguier's avatar
Benoit Viguier committed
42
  \label{tikz:ProofOverview}
Benoit Viguier's avatar
Benoit Viguier committed
43
\end{figure}
Benoit Viguier's avatar
Benoit Viguier committed
44

Benoit Viguier's avatar
Benoit Viguier committed
45
Verifying \TNaCle{crypto_scalarmult} also implies verifying all the functions
46
47
48
subsequently called: \TNaCle{unpack25519}; \TNaCle{A}; \TNaCle{Z}; \TNaCle{M};
\TNaCle{S}; \TNaCle{car25519}; \TNaCle{inv25519}; \TNaCle{set25519}; \TNaCle{sel25519};
\TNaCle{pack25519}.
Benoit Viguier's avatar
Benoit Viguier committed
49

50
We prove the implementation of X25519 is \textbf{sound}, \ie:
Benoit Viguier's avatar
Benoit Viguier committed
51
52
53
54
55
56
\begin{itemize}
\item absence of access out-of-bounds of arrays (memory safety).
\item absence of overflows/underflow on the arithmetic.
\end{itemize}
We also prove that TweetNaCl's code is \textbf{correct}:
\begin{itemize}
Benoit Viguier's avatar
Benoit Viguier committed
57
\item X25519 is correctly implemented (we get what we expect) .
Benoit Viguier's avatar
Benoit Viguier committed
58
59
\item Operations on \texttt{gf} (\texttt{A}, \texttt{Z}, \texttt{M}, \texttt{S})
are equivalent to operations ($+,-,\times,x^2$) in \Zfield.
Benoit Viguier's avatar
Benoit Viguier committed
60
61
\item The Montgomery ladder computes a scalar multiplication between a natural
number and a point.
Benoit Viguier's avatar
Benoit Viguier committed
62
63
\end{itemize}

Benoit Viguier's avatar
Benoit Viguier committed
64
In order to prove the soundness and correctness of \TNaCle{crypto_scalarmult},
Benoit Viguier's avatar
Benoit Viguier committed
65
we first create a skeleton of the Montgomery ladder with abstract operations which
Benoit Viguier's avatar
Benoit Viguier committed
66
67
can be instantiated over lists, integers, field elements...
A high level specification (over a generic field $\K$) allows us to prove the
Benoit Viguier's avatar
Benoit Viguier committed
68
correctness of the ladder with respect to the curves theory.
Benoit Viguier's avatar
Benoit Viguier committed
69
70
71
72
This high-level specification does not rely on the parameters of Curve25519.
By instantiating $\K$ with $\Zfield$, and the parameters of Curve25519 ($a = 486662, b = 1$),
we define a mid-level specification.
Additionally we also provide a low-level specification close to the \texttt{C} code
Benoit Viguier's avatar
Benoit Viguier committed
73
74
75
76
(over lists of $\Z$). We show this specification to be equivalent to the
\textit{semantic version} of C (\texttt{CLight}) with VST.
This low level specification gives us the soundness assurance.
By showing that operations over instances ($\K = \Zfield$, $\Z$, list of $\Z$) are
Benoit Viguier's avatar
Benoit Viguier committed
77
equivalent, we bridge the gap between the low level and the high level specification
Benoit Viguier's avatar
Benoit Viguier committed
78
with Curve25519 parameters.
Benoit Viguier's avatar
Benoit Viguier committed
79
As such, we prove all specifications to equivalent (\fref{tikz:ProofStructure}).
Benoit Viguier's avatar
Benoit Viguier committed
80
This guarantees us the correctness of the implementation.
Benoit Viguier's avatar
Benoit Viguier committed
81
82

\begin{figure}[h]
Benoit Viguier's avatar
Benoit Viguier committed
83
  \centering
Benoit Viguier's avatar
Benoit Viguier committed
84
85
  \include{tikz/specifications}
  \caption{Structural construction of the proof}
Benoit Viguier's avatar
Benoit Viguier committed
86
  \label{tikz:ProofStructure}
Benoit Viguier's avatar
Benoit Viguier committed
87
88
\end{figure}

Benoit Viguier's avatar
Benoit Viguier committed
89
90
91
92
93




\subsection{A Correct Specification}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
94

Benoit Viguier's avatar
Benoit Viguier committed
95
TweetNaCl implements X25519 with numbers represented as arrays.
Benoit Viguier's avatar
Benoit Viguier committed
96
RFC~7748 defines X25519 over field elements. In order to simplify our proofs,
97
we define operations used in the ladder over generic types
Benoit Viguier's avatar
Benoit Viguier committed
98
\coqe{T} and \coqe{T'}. Those types are later instantiated as natural numbers,
Benoit Viguier's avatar
Benoit Viguier committed
99
100
101
102
103
104
105
integers, field elements, list of integers...
The generic definition of the ladder (\coqe{montgomery_rec}) and its match with
the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}.
It has to be noted that the RFC uses an additional variable to optimize the number
of \texttt{CSWAP}:
\emph{``Note that these formulas are slightly different from Montgomery's
original paper.  Implementations are free to use any correct formulas.''}~\cite{rfc7748}.
Benoit Viguier's avatar
Benoit Viguier committed
106
We later prove our ladder correct in that respect (\sref{sec:maths}).
Benoit Viguier's avatar
Benoit Viguier committed
107

108
\coqe{montgomery_rec} only computes the ladder steps.
Benoit Viguier's avatar
Benoit Viguier committed
109
110
While the inversion, the packing, the unpacking (setting bit 255 to \texttt{0})
and the clamping are not defined in a generic manner, we show their equivalence
111
between the different representations.
Benoit Viguier's avatar
Benoit Viguier committed
112

Benoit Viguier's avatar
Benoit Viguier committed
113
114
Appendix~\ref{subsubsec:ZCryptoScalarmult} shows the instantiation of our ladder
over Integers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.
115
116
117
The modulo reduction is applied in \coqe{ZPack25519} translating every
underlying operations as over \Zfield. As a result this specification can be
interpreted as the formalization of X25519 in RFC~7748.
118

119
120
121
122
123
In appendix~\ref{subsubsec:CryptoScalarmult}, we show the the formalization of
\TNaCle{crypto_scalarmult} over lists of integers. We define it as
\Coqe{Crypto_Scalarmult} or \Coqe{CSM}. For the sake of space and simplicity we
do not display the definitions of each underlying functions.
The location of the definitions are listed in Appendix~\ref{appendix:proof-files}.
Benoit Viguier's avatar
Benoit Viguier committed
124
125
126
127

\subsection{With the Verifiable Software Toolchain}
\label{subsec:with-VST}

128
We now turn our focus to the specification of the Hoare triple with our
Benoit Viguier's avatar
Benoit Viguier committed
129
specifications of \TNaCle{crypto_scalarmult} over lists of integers and proving
130
131
its correctness.

Benoit Viguier's avatar
Benoit Viguier committed
132
\subheading{Specifications.}
133
134
135
136
137
138
139
We show the soundness of TweetNaCl by proving the following specification matches
a pure Coq function.
% why "pure" ?
% A pure function is a function where the return value is only determined by its
% input values, without observable side effects (Side effect are e.g. printing)
This defines the equivalence between the Clight representation and our Coq
definition of the ladder (\coqe{CSM}).
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
140

Benoit Viguier's avatar
Benoit Viguier committed
141
\begin{lstlisting}[language=CoqVST]
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
Definition crypto_scalarmult_spec :=
DECLARE _crypto_scalarmult_curve25519_tweet
WITH
  v_q: val, v_n: val, v_p: val, c121665:val,
  sh : share,
  q : list val, n : list Z, p : list Z
(*------------------------------------------*)
PRE [ _q OF (tptr tuchar),
     _n OF (tptr tuchar),
     _p OF (tptr tuchar) ]
PROP (writable_share sh;
      Forall (fun x => 0 <= x < 2^8) p;
      Forall (fun x => 0 <= x < 2^8) n;
      Zlength q = 32; Zlength n = 32;
      Zlength p = 32)
LOCAL(temp _q v_q; temp _n v_n; temp _p v_p;
      gvar __121665 c121665)
SEP  (sh [{ v_q }] <<(uch32)-- q;
      sh [{ v_n }] <<(uch32)-- mVI n;
      sh [{ v_p }] <<(uch32)-- mVI p;
      Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665)
(*------------------------------------------*)
POST [ tint ]
PROP (Forall (fun x => 0 <= x < 2^8) (CSM n p);
      Zlength (CSM n p) = 32)
LOCAL(temp ret_temp (Vint Int.zero))
SEP  (sh [{ v_q }] <<(uch32)-- mVI (CSM n p);
      sh [{ v_n }] <<(uch32)-- mVI n;
      sh [{ v_p }] <<(uch32)-- mVI p;
      Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665
Benoit Viguier's avatar
Benoit Viguier committed
172
\end{lstlisting}
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
173
174
175
176

In this specification we state as preconditions:
\begin{itemize}
  \item[] \VSTe{PRE}: \VSTe{_p OF (tptr tuchar)}\\
177
  The function \TNaCle{crypto_scalarmult} takes as input three pointers to
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
  arrays of unsigned bytes (\VSTe{tptr tuchar}) \VSTe{_p}, \VSTe{_q} and \VSTe{_n}.
  \item[] \VSTe{LOCAL}: \VSTe{temp _p v_p}\\
  Each pointer represent an address \VSTe{v_p},
  \VSTe{v_q} and \VSTe{v_n}.
  \item[] \VSTe{SEP}: \VSTe{sh [{ v_p $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI p}\\
  In the memory share \texttt{sh}, the address \VSTe{v_p} points
  to a list of integer values \VSTe{mVI p}.
  \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\
  In order to consider all the possible inputs, we assumed each
  elements of the list \texttt{p} to be bounded by $0$ included and $2^8$
  excluded.
  \item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\
  We also assumed that the length of the list \texttt{p} is 32. This defines the
  complete representation of \TNaCle{u8[32]}.
\end{itemize}

As Post-condition we have:
\begin{itemize}
  \item[] \VSTe{POST}: \VSTe{tint}\\
197
  The function \TNaCle{crypto_scalarmult} returns an integer.
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
198
199
200
201
202
203
204
205
206
207
208
  \item[] \VSTe{LOCAL}: \VSTe{temp ret_temp (Vint Int.zero)}\\
  The returned integer has value $0$.
  \item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (CSM n p)}\\
  In the memory share \texttt{sh}, the address \VSTe{v_q} points
  to a list of integer values \VSTe{mVI (CSM n p)} where \VSTe{CSM n p} is the
  result of the \VSTe{crypto_scalarmult} over \VSTe{n} and \VSTe{p}.
  \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (CSM n p)}\\
  \VSTe{PROP}: \VSTe{Zlength (CSM n p) = 32}\\
  We show that the computation for \VSTe{CSM} fits in  \TNaCle{u8[32]}.
\end{itemize}

209
This specification shows that \TNaCle{crypto_scalarmult} in C computes the same
Benoit Viguier's avatar
WIP    
Benoit Viguier committed
210
result as \VSTe{CSM} in Coq provided that inputs are within their respective
Benoit Viguier's avatar
Benoit Viguier committed
211
bounds: arrays of 32 bytes.
212
The location of the proof of this Hoare triple can be found in Appendix~\ref{appendix:proof-files}.
213

214
% We now bring the attention of the reader to details of verifications using the VST.
Benoit Viguier's avatar
Benoit Viguier committed
215

216
217
218
219
220
221
222
223
224
225
%% BLABLA about VST. Does not belong here.

% The Verifiable Software Toolchain uses a strongest postcondition strategy.
% The user must first write a formal specification of the function he wants to verify in Coq.
% This should be as close as possible to the C implementation behavior.
% This will simplify the proof and help with stepping through the CLight version of the software.
% With the range of inputs defined, VST mechanically steps through each instruction
% and ask the user to verify auxiliary goals such as array bound access, or absence of overflows/underflows.
% We call this specification a low level specification. A user will then have an easier
% time to prove that his low level specification matches a simpler higher level one.
Benoit Viguier's avatar
Benoit Viguier committed
226

227
228
229
230
231
232
233
234
% In order to further speed-up the verification process, it has to be know that to
% prove the specification \TNaCle{crypto_scalarmult}, a user only need the specification of e.g. \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.

\subheading{Memory aliasing.}
In the VST, a simple specification of \texttt{M(o,a,b)} will assume three
Benoit Viguier's avatar
Benoit Viguier committed
235
distinct memory share. When called with three memory shares (\texttt{o, a, b}),
236
237
238
the three of them will be consumed. However assuming this naive specification
when \texttt{M(o,a,a)} is called (squaring), the first two memory shares (\texttt{o, a})
are consumed and VST will expect a third memory share (\texttt{a}) which does not \textit{exist} anymore.
Benoit Viguier's avatar
Benoit Viguier committed
239
Examples of such cases are illustrated in \fref{tikz:MemSame}.
Benoit Viguier's avatar
Benoit Viguier committed
240
241
242
243
244
245
246
\begin{figure}[h]
  \centering
  \include{tikz/memory_same_sh}
  \caption{Aliasing and Separation Logic}
  \label{tikz:MemSame}
\end{figure}

247
248
249
250
As a result, a function must either have multiple specifications or specify which
aliasing case is being used.
The first option would require us to do very similar proofs multiple times for a same function.
We chose the second approach: for functions with 3 arguments, named hereafter \texttt{o, a, b},
Benoit Viguier's avatar
Benoit Viguier committed
251
we define an additional parameter $k$ with values in $\{0,1,2,3\}$:
Benoit Viguier's avatar
Benoit Viguier committed
252
253
254
255
256
257
\begin{itemize}
  \item if $k=0$ then \texttt{o} and \texttt{a} are aliased.
  \item if $k=1$ then \texttt{o} and \texttt{b} are aliased.
  \item if $k=2$ then \texttt{a} and \texttt{b} are aliased.
  \item else there is no aliasing.
\end{itemize}
258
259
260
In the proof of our specification, we do a case analysis over $k$ when needed.
This solution does not cover all cases (e.g. all arguments are aliased) but it
is enough for our needs.
Benoit Viguier's avatar
Benoit Viguier committed
261

Benoit Viguier's avatar
Benoit Viguier committed
262
\subheading{Verifying \texttt{for} loops.}
Benoit Viguier's avatar
Benoit Viguier committed
263
Final state of \texttt{for} loops are usually computed by simple recursive functions.
Benoit Viguier's avatar
Benoit Viguier committed
264
However we must define invariants which are true for each iteration step.
Benoit Viguier's avatar
Benoit Viguier committed
265
266

Assume we want to prove a decreasing loop where indexes go from 3 to 0.
Benoit Viguier's avatar
Benoit Viguier committed
267
Define a function $g : \N \rightarrow State  \rightarrow State $ which takes as
Benoit Viguier's avatar
Benoit Viguier committed
268
269
input an integer for the index and a state, then returns a state.
It simulates the body of the \texttt{for} loop.
Benoit Viguier's avatar
Benoit Viguier committed
270
Assume its recursive call: $f : \N \rightarrow State \rightarrow State $ which
Benoit Viguier's avatar
Benoit Viguier committed
271
iteratively applies $g$ with decreasing index:
Benoit Viguier's avatar
Benoit Viguier committed
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
\begin{equation*}
  f ( i , s ) =
  \begin{cases}
  s & \text{if } s = 0 \\
  f( i - 1 , g ( i - 1  , s )) & \text{otherwise}
  \end{cases}
\end{equation*}
Then we have :
\begin{align*}
  f(4,s) &= g(0,g(1,g(2,g(3,s))))
  % \\
  % f(3,s) &= g(0,g(1,g(2,s)))
\end{align*}
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.
Benoit Viguier's avatar
Benoit Viguier committed
287
288
289
290
Due to the computation order of recursive function, our loop invariant for
$i\in\{0;1;2;3;4\}$ cannot use $f(i)$.
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.
Benoit Viguier's avatar
Benoit Viguier committed
291

Benoit Viguier's avatar
Benoit Viguier committed
292
293
294
We then prove for the complete number of steps, the function with the accumulator
and without returns the same result.
We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.
Benoit Viguier's avatar
Benoit Viguier committed
295
296

Using this formalization, we prove that the 255 steps of the Montgomery ladder
297
in C provide the same computations as in \coqe{CSM}.
Benoit Viguier's avatar
Benoit Viguier committed
298

299
300
301



Benoit Viguier's avatar
Benoit Viguier committed
302
303
\subsection{Number Representation and C Implementation}

Benoit Viguier's avatar
Benoit Viguier committed
304
As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented
305
306
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,
Benoit Viguier's avatar
Benoit Viguier committed
307
we need to convert this number to a full integer.
308
309
310
311
312
\begin{dfn}
Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list} \Z \rightarrow \Z$,
a parameterized map by $n$ between a list $l$ and its little endian representation
with a radix $2^n$.
\end{dfn}
313
314
315
316
317
318
319
320
321
322
323
324
We define it in Coq as:
\begin{lstlisting}[language=Coq]
Fixpoint ZofList {n:Z} (a:list Z) : Z :=
  match a with
  | [] => 0
  | h :: q => h + (pow 2 n) * ZofList q
  end.
\end{lstlisting}
We define a notation where $n$ is $16$.
\begin{lstlisting}[language=Coq]
Notation "Z16.lst A" := (ZofList 16 A).
\end{lstlisting}
325
To facilitate working in \Zfield, we define the \coqe{:GF} notation.
326
327
328
\begin{lstlisting}[language=Coq]
Notation "A :GF" := (A mod (2^255-19)).
\end{lstlisting}
329
330
Later in \sref{sec:maths}, we formally define \F{\p}.
Equivalence between operations under \coqe{:GF} and in \F{\p} are easily proven.
331
332

Using these two definitions, we proved intermediates lemmas such as the correctness of the
333
multiplication \Coqe{Low.MM} where \Coqe{Low.M} replicate the computations and steps done in C.
334
\begin{lemma}
335
336
  \label{lemma:mult_correct}
  \Coqe{Low.M} implements correctly the multiplication over \Zfield.
337
338
\end{lemma}
And seen in Coq as follows:
339
\begin{lstlisting}[language=Coq]
340
341
342
343
Lemma mult_GF_Zlength :
  forall (a:list Z) (b:list Z),
  Zlength a = 16 ->
  Zlength b = 16 ->
344
   (Z16.lst (Low.M a b)) :GF =
345
   (Z16.lst a * Z16.lst b) :GF.
346
347
348
349
\end{lstlisting}

However for our purpose, simple functional correctness is not enough.
We also need to define the bounds under which the operation is correct,
Benoit Viguier's avatar
aspell    
Benoit Viguier committed
350
allowing us to chain them, guaranteeing us the absence of overflow.
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366

\begin{lemma}
  \label{lemma:mult_bounded}
  if all the values of the input arrays are constrained between $-2^{26}$ and $2^{26}$,
  then the output of \coqe{Low.M} will be constrained between $-38$ and $2^{16} + 38$.
\end{lemma}
And seen in Coq as follows:
\begin{lstlisting}[language=Coq]
Lemma M_bound_Zlength :
  forall (a:list Z) (b:list Z),
  Zlength a = 16 ->
  Zlength b = 16 ->
  Forall (fun x => -2^26 < x < 2^26) a ->
  Forall (fun x => -2^26 < x < 2^26) b ->
    Forall (fun x => -38 <= x < 2^16 + 38) (Low.M a b).
\end{lstlisting}
367

368
369
370



Benoit Viguier's avatar
Benoit Viguier committed
371
\subsection{Inversions, Reflections and Packing}
372

373
We now turn our attention to the inversion in \Zfield and techniques to
Benoit Viguier's avatar
aspell    
Benoit Viguier committed
374
increase the verification speed of complex formulas.
375

Benoit Viguier's avatar
Benoit Viguier committed
376
\subheading{Inversions in \Zfield.}
Benoit Viguier's avatar
Benoit Viguier committed
377
We define a Coq version of the inversion mimicking
378
the behavior of \TNaCle{inv25519} (see below) over \Coqe{list Z}.
379
\begin{lstlisting}[language=Ctweetnacl]
380
sv inv25519(gf o,const gf i)
381
382
{
  gf c;
383
384
385
  int a;
  set25519(c,i);
  for(a=253;a>=0;a--) {
386
    S(c,c);
387
    if(a!=2&&a!=4) M(c,c,i);
388
  }
389
  FOR(a,16) o[a]=c[a];
390
391
}
\end{lstlisting}
392
393
We specify this with 2 functions: a recursive \Coqe{pow_fn_rev}
to simulate the \texttt{for} loop and a simple \Coqe{step_pow} containing the body.
394
\begin{lstlisting}[language=Coq]
395
396
Definition step_pow (a:Z)
  (c:list Z) (g:list Z) : list Z :=
397
  let c := Sq c in
398
    if a <>? 2 && a <>? 4
399
400
401
    then M c g
    else c.

402
403
Function pow_fn_rev (a:Z) (b:Z)
  (c: list Z) (g: list Z)
404
405
406
407
408
  {measure Z.to_nat a} : (list Z) :=
  if a <=? 0
    then c
    else
      let prev := pow_fn_rev (a - 1) b c g in
409
        step_pow (b - a) prev g.
410
411
\end{lstlisting}
This \Coqe{Function} requires a proof of termination. It is done by proving the
Benoit Viguier's avatar
Benoit Viguier committed
412
well-foundedness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling
413
414
415
416
417
\Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the \texttt{Clight} definition.
\begin{lstlisting}[language=Coq]
Definition Inv25519 (x:list Z) : list Z :=
  pow_fn_rev 254 254 x x.
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
418
Similarly we define the same function over $\Z$.
419
420
421
\begin{lstlisting}[language=Coq]
Definition step_pow_Z (a:Z) (c:Z) (g:Z) : Z :=
  let c := c * c in
422
  if a <>? 2 && a <>? 4
423
424
425
426
427
428
429
430
431
    then c * g
    else c.

Function pow_fn_rev_Z (a:Z) (b:Z) (c:Z) (g: Z)
  {measure Z.to_nat a} : Z :=
  if (a <=? 0)
    then c
    else
      let prev := pow_fn_rev_Z (a - 1) b c g in
432
        step_pow_Z (b - a) prev g.
433
434
435
436

Definition Inv25519_Z (x:Z) : Z :=
  pow_fn_rev_Z 254 254 x x.
\end{lstlisting}
437
438
439
440
By using \lref{lemma:mult_correct}, we prove their equivalence in $\Zfield$.
\begin{lemma}
\label{lemma:Inv_equivalence}
The function \coqe{Inv25519} over list of integers computes the same
Benoit Viguier's avatar
aspell    
Benoit Viguier committed
441
result at \coqe{Inv25519_Z} over integers in \Zfield.
442
443
\end{lemma}
This is formalized in Coq as follows:
444
445
446
447
448
449
\begin{lstlisting}[language=Coq]
Lemma Inv25519_Z_GF : forall (g:list Z),
  length g = 16 ->
  (Z16.lst (Inv25519 g)) :GF =
  (Inv25519_Z (Z16.lst g)) :GF.
\end{lstlisting}
450

Benoit Viguier's avatar
Benoit Viguier committed
451
In TweetNaCl, \TNaCle{inv25519} computes an inverse in $\Zfield$.
Benoit Viguier's avatar
Benoit Viguier committed
452
It uses Fermat's little theorem by doing an exponentiation to $2^{255}-21$.
453
This is done by applying a square-and-multiply algorithm. The binary representation
Benoit Viguier's avatar
Benoit Viguier committed
454
of $p-2$ implies to always do multiplications except for bits 2 and 4.
455
456
To prove the correctness of the result we can use multiple strategies such as:
\begin{itemize}
Benoit Viguier's avatar
Benoit Viguier committed
457
  \item Proving it is a special case of square-and-multiply algorithm applied to $2^{255}-21$.
458
459
460
461
462
463
464
465
466
  \item Unrolling the for loop step-by-step and applying the equalities
  $x^a \times x^b = x^{(a+b)}$ and $(x^a)^2 = x^{(2 \times a)}$. We prove that
  the resulting exponent is $2^{255}-21$.
\end{itemize}
We use the second method for the benefits of simplicity. However it requires to
apply the unrolling and exponentiation formulas 255 times. This can be automated
in Coq with tacticals such as \Coqe{repeat}, but it generates a proof object which
will take a long time to verify.

Benoit Viguier's avatar
Benoit Viguier committed
467

468
469
470
\subheading{Speeding up with Reflections.} This technique provides us with
flexibility, \eg we don't need to know the number of times nor the order
in which the lemmas needs to be applied (chapter 15 in \cite{CpdtJFR}).
471
472

The idea is to \textit{reflect} the goal into a decidable environment.
Benoit Viguier's avatar
Benoit Viguier committed
473
We show that for a property $P$, we can define a decidable Boolean property
474
475
476
477
478
479
480
$P_{bool}$ such that if $P_{bool}$ is \Coqe{true} then $P$ holds.
$$reify\_P : P_{bool} = true \implies P$$
By applying $reify\_P$ on $P$ our goal become $P_{bool} = true$.
We then compute the result of $P_{bool}$. If the decision goes well we are
left with the tautology $true = true$.

To prove that the \Coqe{Inv25519_Z} is computing $x^{2^{255}-21}$,
481
482
we define a Domain Specific Language (DSL).
\begin{dfn}
483
484
485
Let \Coqe{expr_inv} denote an expression which is either a term;
a multiplication of expressions; a squaring of an expression or a power of an expression.
And Let \Coqe{formula_inv} denote an equality between two expressions.
486
\end{dfn}
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
\begin{lstlisting}[language=Coq]
Inductive expr_inv :=
  | R_inv : expr_inv
  | M_inv : expr_inv -> expr_inv -> expr_inv
  | S_inv : expr_inv -> expr_inv
  | P_inv : expr_inv -> positive -> expr_inv.

Inductive formula_inv :=
  | Eq_inv : expr_inv -> expr_inv -> formula_inv.
\end{lstlisting}
The denote functions are defined as follows:
\begin{lstlisting}[language=Coq]
Fixpoint e_inv_denote (m:expr_inv) : Z :=
  match m with
  | R_inv     =>
    term_denote
  | M_inv x y =>
    (e_inv_denote x) * (e_inv_denote y)
  | S_inv x =>
    (e_inv_denote x) * (e_inv_denote x)
  | P_inv x p =>
    pow (e_inv_denote x) (Z.pos p)
  end.

Definition f_inv_denote (t : formula_inv) : Prop :=
  match t with
  | Eq_inv x y => e_inv_denote x = e_inv_denote y
  end.
\end{lstlisting}
All denote functions also take as an argument the environment containing the variables.
517
518
We do not show it here for the sake of readability,
given that an environment, \Coqe{term_denote} returns the appropriate variable.
Benoit Viguier's avatar
Benoit Viguier committed
519
With this Domain Specific Language we have the following equality:
520
521
522
523
524
525
526
527
\begin{lstlisting}[backgroundcolor=\color{white}]
f_inv_denote
 (Eq_inv (M_inv R_inv (S_inv R_inv))
         (P_inv R_inv 3))
  = (x * x^2 = x^3)
\end{lstlisting}
On the right side, \Coqe{(x * x^2 = x^3)} depends on $x$. On the left side,
\texttt{(Eq\_inv (M\_inv R\_inv (S\_inv R\_inv)) (P\_inv R\_inv 3))} does not depend on $x$.
Benoit Viguier's avatar
Benoit Viguier committed
528
This allows us to use computations in our decision procedure.
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545

We define \Coqe{step_inv} and \Coqe{pow_inv} to mirror the behavior of
\Coqe{step_pow_Z} and respectively \Coqe{pow_fn_rev_Z} over our DSL and
we prove their equality.
\begin{lstlisting}[language=Coq]
Lemma step_inv_step_pow_eq :
  forall (a:Z) (c:expr_inv) (g:expr_inv),
  e_inv_denote (step_inv a c g) =
  step_pow_Z a (e_inv_denote c) (e_inv_denote g).

Lemma pow_inv_pow_fn_rev_eq :
  forall (a:Z) (b:Z) (c:expr_inv) (g:expr_inv),
  e_inv_denote (pow_inv a b c g) =
  pow_fn_rev_Z a b (e_inv_denote c) (e_inv_denote g).
\end{lstlisting}
We then derive the following lemma.
\begin{lemma}
546
547
\label{lemma:reify}
With an appropriate choice of variables, \Coqe{pow_inv} denotes \Coqe{Inv25519_Z}.
548
549
550
551
552
553
\end{lemma}

In order to prove formulas in \Coqe{formula_inv},
we have the following a decidable procedure.
We define \Coqe{pow_expr_inv}, a function which returns the power of an expression.
We then compare the two values and decide over their equality.
554
\begin{lstlisting}[language=Coq]
555
556
557
Fixpoint pow_expr_inv (t:expr_inv) : Z :=
  match t with
  (* power of a term is 1. *)
558
559
  | R_inv   => 1
  (* x^a * x^b = x^{a+b}. *)
560
561
  | M_inv x y =>
    (pow_expr_inv x) + (pow_expr_inv y)
562
    (* (x^a)^2 = x^{2a}. *)
563
564
  | S_inv x =>
    2 * (pow_expr_inv x)
565
    (* (x^b)^a = x^{a*b}. *)
566
567
568
569
570
571
572
573
574
575
576
  | P_inv x p =>
    (Z.pos p) * (pow_expr_inv x)
  end.

Definition decide_e_inv (l1 l2:expr_inv) : bool :=
  (pow_expr_inv l1) ==? (pow_expr_inv l2).

Definition decide_f_inv (f:formula_inv) : bool :=
  match f with
  | Eq_inv x y => decide_e_inv x y
  end.
577
\end{lstlisting}
578

579
580
We prove our decision procedure correct.
\begin{lemma}
581
\label{lemma:decide}
582
583
584
585
For all formulas $f$, if the decision over $f$ returns \Coqe{true},
then the denoted equality by $f$ is true.
\end{lemma}
Which is formalized as:
586
\begin{lstlisting}[language=Coq]
587
588
589
Lemma decide_formula_inv_impl :
  forall (f:formula_inv),
  decide_f_inv f = true ->
590
    f_inv_denote f.
591
\end{lstlisting}
592

593
594
By reification to over DSL (\lref{lemma:reify}) and by applying our decision
(\lref{lemma:decide}), we prove the following corollary.
Benoit Viguier's avatar
Benoit Viguier committed
595
\begin{lemma}
596
\label{lemma:inv_comput_inv}
597
\Coqe{Inv25519_Z} computes an inverse in \Zfield.
Benoit Viguier's avatar
Benoit Viguier committed
598
\end{lemma}
599
Which is formalized as:
600
\begin{lstlisting}[language=Coq]
601
602
603
Theorem Inv25519_Z_correct :
  forall (x:Z),
  Inv25519_Z x = pow x (2^255-21).
604
\end{lstlisting}
605

Benoit Viguier's avatar
aspell    
Benoit Viguier committed
606
607
% From \Coqe{Inv25519_Z_GF} (\lref{lemma:Inv_equivalence}) and \Coqe{Inv25519_Z_correct} (Corollary~\ref{lemma:inv_comput_inv}),
From \lref{lemma:Inv_equivalence} and Corollary~\ref{lemma:inv_comput_inv},
608
we conclude the functional correctness of the inversion over \Zfield.
609
\begin{corollary}
Benoit Viguier's avatar
Benoit Viguier committed
610
\label{cor:inv_comput_field}
611
612
\Coqe{Inv25519} computes an inverse in \Zfield.
\end{corollary}
613
Which is formalized as:
614
\begin{lstlisting}[language=Coq]
615
616
617
618
619
Corollary Inv25519_Zpow_GF :
  forall (g:list Z),
  length g = 16 ->
  Z16.lst (Inv25519 g) :GF  =
  (pow (Z16.lst g) (2^255-21)) :GF.
620
\end{lstlisting}
621

Benoit Viguier's avatar
Benoit Viguier committed
622
\subheading{Another applications of reflections: packing}
623
This reflection technique can also be used where proofs requires some computing
Benoit Viguier's avatar
Benoit Viguier committed
624
over a small and finite domain of variables to test e.g. for all $i$ such that $0 \le i < 16$.
625
626
627
628
629
630
631
Using reflection we prove that we can split the for loop in \TNaCle{pack25519} into two parts.
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
  m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
  m[i-1]&=0xffff;
}
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
632
The first loop is computing the subtraction while the second is applying the carries.
633
634
635
636
\begin{lstlisting}[language=Ctweetnacl]
for(i=1;i<15;i++) {
  m[i]=t[i]-0xffff
}
Benoit Viguier's avatar
Benoit Viguier committed
637

638
639
640
641
642
for(i=1;i<15;i++) {
  m[i]=m[i]-((m[i-1]>>16)&1);
  m[i-1]&=0xffff;
}
\end{lstlisting}
643

Benoit Viguier's avatar
Benoit Viguier committed
644
This loop separation allows simpler proofs. The first loop is seen as the subtraction of a number in \Zfield.
Benoit Viguier's avatar
Benoit Viguier committed
645
We then prove that with the iteration of the second loop, the number represented in $\Zfield$ stays the same.
Benoit Viguier's avatar
Benoit Viguier committed
646
This leads to the proof that \TNaCle{pack25519} is effectively reducing modulo $\p$ and returning a number in base $2^8$.
647
\begin{lstlisting}[language=Coq]
648
Lemma Pack25519_mod_25519 :
Benoit Viguier's avatar
Benoit Viguier committed
649
650
651
652
653
  forall (l:list Z),
  Zlength l = 16 ->
  Forall (fun x => -2^62 < x < 2^62) l ->
  ZofList 8 (Pack25519 l) =
  (Z16.lst l) mod (2^255-19).
654
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
655

656
657
658
659
By proving that each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub};
\coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{car25519} are behaving over \coqe{list Z}
as their equivalent over \coqe{Z} in \coqe{:GF} (in \Zfield), we prove the correctness of
\tref{thm:RFC}. This is formalized as follows in Coq:
Benoit Viguier's avatar
Benoit Viguier committed
660
661
662
663
664
665
666
667
668
669
\begin{lstlisting}[language=Coq]
Theorem Crypto_Scalarmult_Eq :
  forall (n p:list Z),
  Zlength n = 32 ->
  Zlength p = 32 ->
  Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n ->
  Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p ->
  ZofList 8 (Crypto_Scalarmult n p) =
  ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p).
\end{lstlisting}