2_preliminaries.tex 13.5 KB
Newer Older
1
\section{Preliminaries}
Benoit Viguier's avatar
Benoit Viguier committed
2
\label{sec:preliminaries}
Benoit Viguier's avatar
Benoit Viguier committed
3

Peter Schwabe's avatar
Peter Schwabe committed
4
5
6
7
In this section, we first give a brief summary of the mathematical background
on elliptic curves. We then describe X25519 and its implementation in TweetNaCl.
Finally, we provide a brief description of the formal tools we use in our proofs.

8

Peter Schwabe's avatar
Peter Schwabe committed
9
\subsection{Arithmetic on Montgomery curves}
Benoit Viguier's avatar
Benoit Viguier committed
10
\label{subsec:arithmetic-montgomery}
Peter Schwabe's avatar
Peter Schwabe committed
11

Benoit Viguier's avatar
Benoit Viguier committed
12
\begin{dfn}
13
  Given a field \K, let $a,b \in \K$ such that $a^2 \neq 4$ and $b \neq 0$,
Peter Schwabe's avatar
Peter Schwabe committed
14
15
  $M_{a,b}$ is the Montgomery curve defined over $\K$ with equation
  $$M_{a,b}: by^2 = x^3 + ax^2 + x.$$
Benoit Viguier's avatar
Benoit Viguier committed
16
\end{dfn}
Benoit Viguier's avatar
Benoit Viguier committed
17

Benoit Viguier's avatar
Benoit Viguier committed
18
\begin{dfn}
Peter Schwabe's avatar
Peter Schwabe committed
19
20
21
22
  For any algebraic extension $\L \supseteq	\K$, we call
  $M_{a,b}(\L)$ the set of $\L$-rational points defined as
  $$M_{a,b}(\L) = \{\Oinf\} \cup \{(x,y) \in \L \times \L~|~by^2 = x^3 + ax^2 + x\}.$$
  Here, the additional element $\Oinf$ denotes the point at infinity.
Benoit Viguier's avatar
Benoit Viguier committed
23
24
\end{dfn}
Details of the formalization can be found in \sref{subsec:ECC-Montgomery}.
Benoit Viguier's avatar
Benoit Viguier committed
25

26

Peter Schwabe's avatar
Peter Schwabe committed
27
For $M_{a,b}$ over a finite field $\F{p}$, the parameter $b$ is known as the ``twisting factor''.
28
For $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$
29
30
are isomorphic via $(x,y) \mapsto (x, \sqrt{b'/b} \cdot y)$.

Benoit Viguier's avatar
Benoit Viguier committed
31
\begin{dfn}
Peter Schwabe's avatar
Peter Schwabe committed
32
33
  When $b'/b$ is not a square in \F{p}, $M_{a,b'}$ is a \emph{quadratic twist} of $M_{a,b}$, i.e.,
  a curve that is isomorphic over $\F{p^2}$~\cite{cryptoeprint:2017:212}.
Benoit Viguier's avatar
Benoit Viguier committed
34
\end{dfn}
Benoit Viguier's avatar
Benoit Viguier committed
35

Peter Schwabe's avatar
Peter Schwabe committed
36
Points in $M_{a,b}(\K)$ can be equipped with a structure of an abelian group
37
with the addition operation $+$ and with neutral element the point at infinity $\Oinf$.
Peter Schwabe's avatar
Peter Schwabe committed
38
39
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}}.$$
Benoit Viguier's avatar
Benoit Viguier committed
40

41
In order to efficiently compute the scalar multiplication we use an algorithm
42
similar to square-and-multiply: the Montgomery ladder where the basic operations
Peter Schwabe's avatar
Peter Schwabe committed
43
are differential addition and doubling~\cite{MontgomerySpeeding}.
44

45
We consider \xcoord-only operations. Throughout the computation,
Peter Schwabe's avatar
Peter Schwabe committed
46
47
48
these $x$-coordinates are kept in projective representation
$(X : Z)$, with $x = X/Z$; the point at infinity is represented as $(1:0)$.
See \sref{subsec:ECC-projective} for more details.
49
We define two operations:
Benoit Viguier's avatar
Benoit Viguier committed
50
\begin{align*}
Peter Schwabe's avatar
Peter Schwabe committed
51
  \texttt{xADD} &: (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\
52
53
&(X_{P + Q}:Z_{P + Q})\\
\texttt{xDBL} &: (X_P:Z_P) \mapsto (X_{2 \cdot P}:Z_{2 \cdot P})
Benoit Viguier's avatar
Benoit Viguier committed
54
\end{align*}
55
56
In the Montgomery ladder, % notice that
the arguments of \texttt{xADD} and \texttt{xDBL}
Benoit Viguier's avatar
Benoit Viguier committed
57
are swapped depending of the value of the $k^{th}$ bit. We use a conditional
Benoit Viguier's avatar
Benoit Viguier committed
58
59
swap \texttt{CSWAP} to change the arguments of the above function while keeping
the same body of the loop.
Peter Schwabe's avatar
Peter Schwabe committed
60
61
Given a pair $(P_0, P_1)$ and a bit $b$, \texttt{CSWAP} returns the pair
$(P_b, P_{1-b})$.
Benoit Viguier's avatar
Benoit Viguier committed
62
63

By using the differential addition and doubling operations we define the Montgomery ladder
64
computing a \xcoord-only scalar multiplication (see \aref{alg:montgomery-ladder}).
Benoit Viguier's avatar
Benoit Viguier committed
65
66
\begin{algorithm}
\caption{Montgomery ladder for scalar mult.}
Benoit Viguier's avatar
Benoit Viguier committed
67
\label{alg:montgomery-ladder}
Benoit Viguier's avatar
Benoit Viguier committed
68
\begin{algorithmic}
Peter Schwabe's avatar
Peter Schwabe committed
69
70
71
72
73
74
75
76
77
78
79
  \REQUIRE{\xcoord $x_P$ of a point $P$, scalar $n$ with $n < 2^m$}
  \ENSURE{\xcoord $x_Q$ of $Q = n \cdot P$}
  \STATE $Q = (X_Q:Z_Q) \leftarrow (1:0)$
  \STATE $R = (X_R:Z_R) \leftarrow (x_P:1)$
  \FOR{$k$ := $m$ down to $1$}
    \STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
    \STATE $Q \leftarrow \texttt{xDBL}(Q)$
    \STATE $R \leftarrow \texttt{xADD}(x_P,Q,R)$
    \STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$
  \ENDFOR
  \RETURN $X_Q/Z_Q$
Benoit Viguier's avatar
Benoit Viguier committed
80
81
\end{algorithmic}
\end{algorithm}
Benoit Viguier's avatar
Benoit Viguier committed
82

83
84


85
\subsection{The X25519 key exchange}
Benoit Viguier's avatar
Benoit Viguier committed
86
\label{subsec:X25519-key-exchange}
Benoit Viguier's avatar
Benoit Viguier committed
87

Peter Schwabe's avatar
Peter Schwabe committed
88
89
From now on let $\F{p}$ be the field with $p=2^{255}-19$ elements.
We consider the elliptic curve $E$ over $\F{p}$ defined by the
90
equation $y^2 = x^3 + 486662 x^2 + x$.
Peter Schwabe's avatar
Peter Schwabe committed
91
For every $x \in \F{p}$ there exist a point $P$ in $E(\F{p^2})$
92
such that $x$ is the \xcoord of $P$.
93

Peter Schwabe's avatar
Peter Schwabe committed
94
The core of the X25519 key-exchange protocol is a scalar-multiplication
95
function, which we will also refer to as X25519.
Peter Schwabe's avatar
Peter Schwabe committed
96
This function receives as input two arrays of $32$ bytes each.
97
98
One of them is interpreted as the little-endian encoding of a
non-negative integer $n$ (see \ref{subsec:integer-bytes}).
Peter Schwabe's avatar
Peter Schwabe committed
99
100
101
102
103
104
105
106
107
The other is interpreted as the little-endian 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'$ by setting bit 255 of $n$
to \texttt{0}; setting bit 254 to \texttt{1} and setting the lower 3 bits to \texttt{0}.
This operation is often called ``clamping'' of the scalar $n$.
Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$.
X25519 then computes the \xcoord of $n'\cdot P$.
108

109
110
111
112
RFC~7748~\cite{rfc7748} standardized the X25519 Diffie–Hellman key-exchange algorithm.
Given the base point $B$ where $X_B=9$, each party generate a secret random number
$s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the
\xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$).
113
The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret with
Peter Schwabe's avatar
Peter Schwabe committed
114
X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).
115

Peter Schwabe's avatar
Peter Schwabe committed
116
\subsection{TweetNaCl specifics}
Benoit Viguier's avatar
Benoit Viguier committed
117
\label{subsec:Number-TweetNaCl}
118

Peter Schwabe's avatar
Peter Schwabe committed
119
As its name suggests, TweetNaCl aims for code compactness (\emph{``a crypto library in 100 tweets''}).
120
As a result it uses a few defines and typedefs to gain precious bytes while
Benoit Viguier's avatar
Benoit Viguier committed
121
still remaining readable.
122
123
124
125
\begin{lstlisting}[language=Ctweetnacl]
#define FOR(i,n) for (i = 0;i < n;++i)
#define sv static void
typedef unsigned char u8;
Peter Schwabe's avatar
Peter Schwabe committed
126
typedef long long i64;
127
\end{lstlisting}
128

129
130
TweetNaCl functions take pointers as arguments. By convention the first one
points to the output array. It is then followed by the input arguments.
131
132
133

Due to some limitations of VST, indexes used in \TNaCle{for} loops have to be
of type \TNaCle{int} instead of \TNaCle{i64}. We change the code to allow our
134
135
proofs to carry through. We believe this does not affect the correctness of the
original code. A complete diff of our modifications to TweetNaCl can be found in
136
137
Appendix~\ref{verified-C-and-diff}.

138

Peter Schwabe's avatar
Peter Schwabe committed
139
\subsection{X25519 in TweetNaCl}
Benoit Viguier's avatar
Benoit Viguier committed
140
\label{subsec:X25519-TweetNaCl}
Peter Schwabe's avatar
Peter Schwabe committed
141

Benoit Viguier's avatar
Benoit Viguier committed
142
We now describe the implementation of X25519 in TweetNaCl.
143
144

\subheading{Arithmetic in \Ffield.}
Peter Schwabe's avatar
Peter Schwabe committed
145
In X25519, all computations are performed in $\F{p}$.
Benoit Viguier's avatar
Benoit Viguier committed
146
147
Throughout the computation, elements of that field
are represented in radix $2^{16}$,
Peter Schwabe's avatar
Peter Schwabe committed
148
i.e., an element $A$ is represented as $(a_0,\dots,a_{15})$,
Peter Schwabe's avatar
Peter Schwabe committed
149
150
151
with $A = \sum_{i=0}^{15}a_i2^{16i}$.
The individual ``limbs'' $a_i$ are represented as
64-bit \TNaCle{long long} variables:
152
153
154
155
\begin{lstlisting}[language=Ctweetnacl]
typedef i64 gf[16];
\end{lstlisting}

156
157
Conversion from the input byte array to this representation in radix $2^{16}$ is
done as follows:
Benoit Viguier's avatar
Benoit Viguier committed
158
159
160
161
162
163
164
165
\begin{lstlisting}[language=Ctweetnacl]
sv unpack25519(gf o, const u8 *n)
{
  int i;
  FOR(i,16) o[i]=n[2*i]+((i64)n[2*i+1]<<8);
  o[15]&=0x7fff;
}
\end{lstlisting}
Peter Schwabe's avatar
Peter Schwabe committed
166
167

The radix-$2^{16}$ representation in limbs of $64$ bits is
Benoit Viguier's avatar
Benoit Viguier committed
168
highly redundant; for any element $A \in \Ffield$ there are
Peter Schwabe's avatar
Peter Schwabe committed
169
multiple ways to represent $A$ as $(a_0,\dots,a_{15})$.
170
This is used to avoid carry handling in the implementations of addition
Benoit Viguier's avatar
Benoit Viguier committed
171
(\TNaCle{A}) and subtraction (\TNaCle{Z}) in $\Ffield$:
Benoit Viguier's avatar
Benoit Viguier committed
172
173
174
175
176
177
178
179
180
181
\begin{lstlisting}[language=Ctweetnacl]
sv A(gf o,const gf a,const gf b) {
  int i;
  FOR(i,16) o[i]=a[i]+b[i];
}

sv Z(gf o,const gf a,const gf b) {
  int i;
  FOR(i,16) o[i]=a[i]-b[i];
}
Peter Schwabe's avatar
Peter Schwabe committed
182
183
184
185
186
\end{lstlisting}

Also multiplication (\TNaCle{M}) is heavily exploiting the redundancy
of the representation to delay carry handling.
\begin{lstlisting}[language=Ctweetnacl]
Benoit Viguier's avatar
Benoit Viguier committed
187
188
189
190
191
192
193
194
195
196
sv M(gf o,const gf a,const gf b) {
  i64 i,j,t[31];
  FOR(i,31) t[i]=0;
  FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j];
  FOR(i,15) t[i]+=38*t[i+16];
  FOR(i,16) o[i]=t[i];
  car25519(o);
  car25519(o);
}
\end{lstlisting}
197

Peter Schwabe's avatar
Peter Schwabe committed
198
199
200
After the actual multiplication, the limbs of the result \texttt{o} are
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:
Benoit Viguier's avatar
Benoit Viguier committed
201
202
203
204
205
206
207
\begin{lstlisting}[language=Ctweetnacl]
sv car25519(gf o)
{
  int i;
  FOR(i,16) {
    o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16);
    o[i]&=0xffff;
208
  }
Benoit Viguier's avatar
Benoit Viguier committed
209
210
}
\end{lstlisting}
211

Benoit Viguier's avatar
Benoit Viguier committed
212
In order to simplify the verification of this function,
213
we treat the last iteration of the loop $i = 15$ as a separate step.
Benoit Viguier's avatar
Benoit Viguier committed
214

215
216
217
Inverses in $\Ffield$ are computed with \TNaCle{inv25519}.
This function uses exponentiation by $2^{255}-21$,
computed with the square-and-multiply algorithm.
Peter Schwabe's avatar
Peter Schwabe committed
218
Fermat's little theorem gives the correctness.
Benoit Viguier's avatar
Benoit Viguier committed
219
Notice that in this case the inverse of $0$ is defined as $0$.
220
221
222
223
224
225
226
227
228
229
230
231
232
\begin{lstlisting}[language=Ctweetnacl]
sv inv25519(gf o,const gf i)
{
  gf c;
  int a;
  set25519(c,i);
  for(a=253;a>=0;a--) {
    S(c,c);
    if(a!=2&&a!=4) M(c,c,i);
  }
  FOR(a,16) o[a]=c[a];
}
\end{lstlisting}
Benoit Viguier's avatar
Benoit Viguier committed
233

Benoit Viguier's avatar
Benoit Viguier committed
234
235
\TNaCle{sel25519} implements a constant-time conditional swap (\texttt{CSWAP}) by
applying a mask between two fields elements.
Benoit Viguier's avatar
Benoit Viguier committed
236
237
238
239
240
241
242
243
244
245
246
247
\begin{lstlisting}[language=Ctweetnacl]
sv sel25519(gf p,gf q,i64 b)
{
  int i;
  i64 t,c=~(b-1);
  FOR(i,16) {
    t= c&(p[i]^q[i]);
    p[i]^=t;
    q[i]^=t;
  }
}
\end{lstlisting}
Peter Schwabe's avatar
Peter Schwabe committed
248

249
Finally, we need the \TNaCle{pack25519} function,
Peter Schwabe's avatar
Peter Schwabe committed
250
which converts from the internal redundant radix-$2^{16}$
Peter Schwabe's avatar
Peter Schwabe committed
251
252
representation to a unique byte array representing an
integer in $\{0,\dots,p-1\}$ in little-endian format.
Benoit Viguier's avatar
Benoit Viguier committed
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
\begin{lstlisting}[language=Ctweetnacl]
sv pack25519(u8 *o,const gf n)
{
  int i,j;
  i64 b;
  gf t,m={0};
  set25519(t,n);
  car25519(t);
  car25519(t);
  car25519(t);
  FOR(j,2) {
    m[0]=t[0]- 0xffed;
    for(i=1;i<15;i++) {
      m[i]=t[i]-0xffff-((m[i-1]>>16)&1);
      m[i-1]&=0xffff;
268
    }
Benoit Viguier's avatar
Benoit Viguier committed
269
270
271
272
    m[15]=t[15]-0x7fff-((m[14]>>16)&1);
    m[14]&=0xffff;
    b=1-((m[15]>>16)&1);
    sel25519(t,m,b);
273
  }
Benoit Viguier's avatar
Benoit Viguier committed
274
275
276
  FOR(i,16) {
    o[2*i]=t[i]&0xff;
    o[2*i+1]=t[i]>>8;
277
  }
Benoit Viguier's avatar
Benoit Viguier committed
278
279
}
\end{lstlisting}
Peter Schwabe's avatar
Peter Schwabe committed
280
As we can see, this function is considerably more complex than the
Benoit Viguier's avatar
Benoit Viguier committed
281
unpacking function. The reason is that it needs to convert
Peter Schwabe's avatar
Peter Schwabe committed
282
283
to a \emph{unique} representation, i.e., also fully reduce modulo
$p$ and remove the redundancy of the radix-$2^{16}$ representation.
Peter Schwabe's avatar
Peter Schwabe committed
284

285
\subheading{The Montgomery ladder.}
286
With these low-level arithmetic and helper functions defined,
Peter Schwabe's avatar
Peter Schwabe committed
287
288
289
290
we can now turn our attention to the core of the X25519 computation:
the \TNaCle{crypto_scalarmult} API function of TweetNaCl,
which is implemented through the Montgomery ladder.

Benoit Viguier's avatar
Benoit Viguier committed
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
\begin{lstlisting}[language=Ctweetnacl]
int crypto_scalarmult(u8 *q,
                      const u8 *n,
                      const u8 *p)
{
  u8 z[32];
  i64 r;
  int i;
  gf x,a,b,c,d,e,f;
  FOR(i,31) z[i]=n[i];
  z[31]=(n[31]&127)|64;
  z[0]&=248;
  unpack25519(x,p);
  FOR(i,16) {
    b[i]=x[i];
    d[i]=a[i]=c[i]=0;
  }
  a[0]=d[0]=1;
  for(i=254;i>=0;--i) {
    r=(z[i>>3]>>(i&7))&1;
    sel25519(a,b,r);
    sel25519(c,d,r);
    A(e,a,c);
    Z(a,a,c);
    A(c,b,d);
    Z(b,b,d);
    S(d,e);
    S(f,a);
    M(a,c,a);
    M(c,b,e);
    A(e,a,c);
    Z(a,a,c);
    S(b,a);
    Z(c,d,f);
    M(a,c,_121665);
    A(a,a,d);
    M(c,c,a);
    M(a,d,f);
    M(d,b,x);
    S(b,e);
    sel25519(a,b,r);
    sel25519(c,d,r);
333
  }
Benoit Viguier's avatar
Benoit Viguier committed
334
335
336
337
338
339
  inv25519(c,c);
  M(a,a,c);
  pack25519(q,a);
  return 0;
}
\end{lstlisting}
Peter Schwabe's avatar
Peter Schwabe committed
340
341
%XXX: I really want line numbers here to link lines in this code to
% the pseudocode description
342
343


344
\subsection{Coq, separation logic, and VST}
Benoit Viguier's avatar
Benoit Viguier committed
345
\label{subsec:Coq-VST}
Benoit Viguier's avatar
Benoit Viguier committed
346

347
348
Coq~\cite{coq-faq} is an interactive theorem prover based on type theory. It
provides an expressive formal language to write mathematical definitions,
349
350
351
352
algorithms, and theorems together with their proofs. It has been used in the proof
of the four-color theorem~\cite{gonthier2008formal} and it is also the system
underlying the CompCert formally verified C compiler~\cite{Leroy-backend}.
Unlike systems like F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},
Benoit Viguier's avatar
Benoit Viguier committed
353
354
Coq does not rely on an SMT solver in its trusted code base.
It uses its type system to verify the applications of hypotheses,
Peter Schwabe's avatar
Peter Schwabe committed
355
lemmas, and theorems~\cite{Howard1995-HOWTFN}.
Benoit Viguier's avatar
Benoit Viguier committed
356

357
358
Hoare logic is a formal system which allows reasoning about programs.
It uses triples such as
Benoit Viguier's avatar
Benoit Viguier committed
359
360
$$\{{\color{doc@lstnumbers}\textbf{Pre}}\}\texttt{~Prog~}\{{\color{doc@lstdirective}\textbf{Post}}\}$$
where ${\color{doc@lstnumbers}\textbf{Pre}}$ and ${\color{doc@lstdirective}\textbf{Post}}$
361
are assertions and \texttt{Prog} is a fragment of code.
Benoit Viguier's avatar
Benoit Viguier committed
362
363
It is read as
``when the precondition  ${\color{doc@lstnumbers}\textbf{Pre}}$ is met,
Peter Schwabe's avatar
Peter Schwabe committed
364
365
executing \texttt{Prog} will yield postcondition ${\color{doc@lstdirective}\textbf{Post}}$''.
We use compositional rules to prove the truth value of a Hoare triple.
Benoit Viguier's avatar
Benoit Viguier committed
366
367
368
369
370
371
372
For example, here is the rule for sequential composition:
\begin{prooftree}
  \AxiomC{$\{P\}C_1\{Q\}$}
  \AxiomC{$\{Q\}C_2\{R\}$}
  \LeftLabel{Hoare-Seq}
  \BinaryInfC{$\{P\}C_1;C_2\{R\}$}
\end{prooftree}
373
374
Separation logic is an extension of Hoare logic which allows reasoning about
pointers and memory manipulation. This logic enforces strict conditions on the
Benoit Viguier's avatar
Benoit Viguier committed
375
memory shared such as being disjoint.
Benoit Viguier's avatar
Benoit Viguier committed
376
We discuss this limitation further in \sref{subsec:with-VST}.
377

Benoit Viguier's avatar
Benoit Viguier committed
378
The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework
379
380
which uses Separation logic proven correct with respect to CompCert semantics
to prove the functional correctness of C programs.
Benoit Viguier's avatar
Benoit Viguier committed
381
The first step consists of translating the source code into Clight,
Benoit Viguier's avatar
Benoit Viguier committed
382
an intermediate representation used by CompCert.
383
For such purpose one uses the parser of CompCert called \texttt{clightgen}.
384
385
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
Benoit Viguier's avatar
Benoit Viguier committed
386
387
postcondition approach to prove the correctness of the triple.
This approach can be seen as a forward symbolic execution of the program.