A4_reviews.tex 21.1 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
\newpage
Benoit Viguier's avatar
mods    
Benoit Viguier committed
2
3
4
~\\
\newpage

5
6
7
8
9
\section{Prior reviews}
\label{appendix:past-reviews}

This paper has been submitted to IEEE Symposium on Security and Privacy 2020.

10
11
12
We thank and really appreciate the reviewers who took time to provide us with
such detailed feedback.

13
14
\subsection{S\&P 2020 Review \#582A}

Benoit Viguier's avatar
Benoit Viguier committed
15
16
Overall merit: 3. Weak reject - The paper has flaws, but I will
not argue against it.
17
18
19
20
21

\begin{center}
  \subheading{===== Brief paper summary (2-3 sentences) =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
22
23
24
25
This paper presents a verification of the C implementation
of the X25519 key-exchange protocol in the TweetNaCl
library. Correctness properties including the C code implements
the algorithm correctly are verified in Coq, using the
Benoit Viguier's avatar
Benoit Viguier committed
26
Verified Software Toolchain (VST).
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41


\begin{center}
  \subheading{===== Strengths =====}
\end{center}

+ This paper produces a fully formally verified crypto library.

+ This paper presents solid technical work.


\begin{center}
  \subheading{===== Weaknesses =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
42
43
44
- The novelty of this paper is not well explained. It’s unclear
whether this paper has pushed the boundary in terms of what
can be formally verified.
45
46
47
48
49
50


\begin{center}
  \subheading{===== Detailed comments for the author(s) =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
51
52
53
54
55
I appreciate work on producing fully verified software. This
paper presents another instance: X25519 protocol. The result
here is very strong: it verified both safety properties and the
correctness of the C implementation.

Benoit Viguier's avatar
Benoit Viguier committed
56
57
One main weakness of this paper is that it is hard to extract
from the writing, what are the new discoveries in this
Benoit Viguier's avatar
Benoit Viguier committed
58
59
60
exercise. Are there new proof techniques developed for this
verification? Is there anything new about the way that loops
are handled? Is the application of reflection challenging? Are
Benoit Viguier's avatar
Benoit Viguier committed
61
there bugs found, in particular, in the mathematical operations?
Benoit Viguier's avatar
Benoit Viguier committed
62
63
64
65
66

\begin{answer}{EEEEEE}
The novelty of this work is not in the proof techniques. It
lies in the assurance gained by the formalization of the
X25519 from RFC 7748, and its correctness with respect to
Benoit Viguier's avatar
Benoit Viguier committed
67
68
69
the theory of elliptic curves. Additionally it is the first
time, a link from the C code up to the mathematical definitions of
Curve25519 using a single tool is presented.
Benoit Viguier's avatar
Benoit Viguier committed
70
71
72
73
74
75
76
77
78
79
\end{answer}

A related comment is that it is unclear from the paper
whether now we can re-use proofs in this paper to verify
mathematical operations of other protocols that use elliptic
curve.

\begin{answer}{EEEEEE}
We believe that parts of our proofs are reusable either by
their structure to give an intuition or by directly changing
Benoit Viguier's avatar
Benoit Viguier committed
80
some values (for e.g. X448). The mathematical definitions
Benoit Viguier's avatar
typos    
Benoit Viguier committed
81
82
are generic and may be instantiated over any fields (of characteristic
neither 2 or 3). The Ladder may be instantiated
Benoit Viguier's avatar
Benoit Viguier committed
83
84
85
over operations over different data structure for the underlying
arithmetic, making it reusable. The low level operations
\eg \TNaCle{A} are also reusable in the proof of ed25519.
Benoit Viguier's avatar
Benoit Viguier committed
86
87
88
89
90
91
92
93
94
\end{answer}

In the Corrections in TweetNaCl paragraph, two things
were discussed. It’s unclear how and whether either one of
them directly relate to the verification effort. It would be nice
if they are. Then the story for the usefulness of the verification
become stronger.

\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
95
96
97
98
99
100
101
102
103
104
The switch from \TNaCle{i64} to \TNaCle{int} in \texttt{for} loops and the
extraction of the computation outside of the function call in
\TNaCle{pack25519} are required by the VST but we believe those
change have no impact on the verification effort.

The only modification which made the verification easier
was the removal of the \textit{dead code} at the end of
\TNaCle{crypto_scalarmult}. Peter Wu and Jason A.
Donenfeld had also noticed this part and informed us after we
already fixed the code.
Benoit Viguier's avatar
Benoit Viguier committed
105
106
107
108
109
110
\end{answer}

It would be nice if the authors comment on the verification
effort: person month etc.

\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
111
112
113
114
115
116
117
In addition to the time required to get familiar with
research software, we faced a few bugs which we reported
to the developers of the VST to get them fixed.
It is very hard to work with a tool without being involved
in the development loop. Additionally newer versions often
broke some of our proofs and it was often needed to adapt
to the changes.
Benoit Viguier's avatar
Benoit Viguier committed
118
119
As a result we do not believe the metric person-month to be
a good representation of the verification effort.
Benoit Viguier's avatar
Benoit Viguier committed
120
121
122
123
124
125
\end{answer}

Also, did the verified version replace the version in use in
production software? If not, why not?

\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
126
127
128
129
We contacted the authors of TweetNaCl and expect that
the changes above mentioned will soon be integrated in a
new version of the library, mostly for \TNaCle{car25519} and the
simplification in \TNaCle{crypto_scalarmult}.
Benoit Viguier's avatar
Benoit Viguier committed
130
\end{answer}
131

Benoit Viguier's avatar
Benoit Viguier committed
132
133
134
135
Section V is extremely dry. What are the high-level insights?
Perhaps a picture representation of how the theorems
and lemmas fit together would be a better way to represent
this section.
136

Benoit Viguier's avatar
Benoit Viguier committed
137
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
typos    
Benoit Viguier committed
138
We provided overviews of the proof at the beginning of sections
Benoit Viguier's avatar
Benoit Viguier committed
139
140
V.1 and V.2. We hope this will give the reader an intuition
of how lemmas fit together.
Benoit Viguier's avatar
Benoit Viguier committed
141
142
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
143
144
145
In summary, this paper is in need of significant improvements
in the writing and providing detailed discussions of
high-level intellectual contributions in this verification effort.
146

Benoit Viguier's avatar
Benoit Viguier committed
147
{\color{gray}
148
149
150
151
152
153
154
Minor

On page 6: "each elements" => no s

On page 7, the beginning of the page, a half sentence is
dangling there.

Benoit Viguier's avatar
Benoit Viguier committed
155
On page 9: "each functions" => no s}
156

157

158
159
\subsection{S\&P 2020 Review \#582B}

Benoit Viguier's avatar
Benoit Viguier committed
160
161
Overall merit: 4. Weak accept - While flawed, the paper has
merit and we should consider accepting it.
162
163
164
165
166
167


\begin{center}
  \subheading{===== Brief paper summary (2-3 sentences) =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
168
169
170
171
172
In this paper, the authors verify the C implementation of the
X25519 elliptic curve key exchange in the TweetNaCl library,
a short implementation of the NaCl library. The X25519 key
exchange method is used in TLS 1.3, Signal, Tor, Zcash and
SSH. Within TLS 1.3 (and probably also in other protocols),
Benoit Viguier's avatar
typos    
Benoit Viguier committed
173
174
any implementation of X25519 may be used in an implementation
of the standard. Thus, the present work contributes
Benoit Viguier's avatar
Benoit Viguier committed
175
to a fully verified code-base for TLS 1.3 (and other crucial
176
177
protocols)

Benoit Viguier's avatar
Benoit Viguier committed
178
179
180
181
182
183
184
185
The verification itself is practically significant. The paper
makes a good effort to describe the approach, but I was, at
times, a little disappointed at the description. Performing this
type of verification yields substantial human understanding
and enables the authors to carry out a similar approach for
other primitives much more easily. I wish that the authors
would extract their conceptual insights on the technique and
communicate those to the readers. Regardless, I would very
Benoit Viguier's avatar
typos    
Benoit Viguier committed
186
187
much like to see this work at S\&P, but I would like to encourage
the authors to de-emphasize technical details (even more)
Benoit Viguier's avatar
Benoit Viguier committed
188
189
and spend more space of the body on conceptual insights (see
comments below).
190
191
192
193
194
195


\begin{center}
  \subheading{===== Detailed comments for the author(s) =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
I was confused that you did not seem have found any errors
in an implementation. I can believe that the implementers
of \cite{BGJ+15} are proficient implementers, but I would have expected
some minor bugs/parsing issues to be found anyway. What is
your explanation that you haven’t found any issues?

\begin{answer}{EEEEEE}
The implementation of TweetNaCl is straight forward and
simple, big number arithmetic is done without optimizations.
It is easy to get an intuition of how the code work by reading
it. The ladder is a direct mapping of RFC~7748. It does
not aim for speed optimizations. This reduce significantly
the complexity of the code compared to e.g., Fiat Crypto
generated optimized C code.

While we did not find errors in the implementation with
Benoit Viguier's avatar
typos    
Benoit Viguier committed
212
213
respect to functional correctness under the CompCert assumptions,
we removed an undefined behavior by the C
Benoit Viguier's avatar
Benoit Viguier committed
214
215
216
standard.
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
217
218
p.1: You discuss \cite{Ber06} as using heavy annotation of code,
differently from your own code. However, as far as I understand,
Benoit Viguier's avatar
Benoit Viguier committed
219
220
221
222
223
224
225
your Coq implementation must also be type-annotated. Thus,
I imagine that the difference lies in whether SAT-solvers are
used or not? This did not become very clear, because you
mostly describe names of tool while leaving out the details of
what these tools carry out conceptually.

\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
226
SMT solvers strategies are in need of annotation, often written
Benoit Viguier's avatar
typo    
Benoit Viguier committed
227
as parsable comment in the middle of the C code~\cite{acsl}
Benoit Viguier's avatar
Benoit Viguier committed
228
in order to ``guide'' the proof. In our case we only need to
Benoit Viguier's avatar
typos    
Benoit Viguier committed
229
annotate the beginning of the function and loop invariants
Benoit Viguier's avatar
Benoit Viguier committed
230
which allows us to get tighter bounds.
Benoit Viguier's avatar
Benoit Viguier committed
231
\end{answer}
232

Benoit Viguier's avatar
Benoit Viguier committed
233
234
235
236
237
238
239
240
p.2: Fig 1 is very nice. However, at this point, none of
the notation has been explained to the reader, and I imagine
that V stands for VST? It wasn't clear to me. Maybe, the
caption of the figure could explain what the details inside the
figures represent. In particular, the Figure seems to used a
nice abstraction of properties that is not used elsewhere in
the paper. I.e., elsewhere in the paper, there is usually a lot
of code details.
241

Benoit Viguier's avatar
Benoit Viguier committed
242
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
243
``.V'' is the file extension for Coq files (as opposed to ``.C'' for C
Benoit Viguier's avatar
Benoit Viguier committed
244
245
files). This allows us to emphasis that all our work is done
in a single framework. We clarified this in the introduction.
Benoit Viguier's avatar
Benoit Viguier committed
246
247
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
248
249
250
251
252
253
254
255
256
257
p.2-4: Subsection A took some mathematical background.
Obviously, not all of it could be covered, but the motivation
for why certain content was presented and not others was not
clear to me as a reader, which was quite frustrating. In Section
B, it was even less clear why particular details were presented,
e.g., the discussion of the computation of n’ was completely
unclear to me. Subsection D seemed a good idea, but was very
tough to follow, too much content in short time. Subsection D
seems to jump between implementation levels and discussing
high-level arguments such as Fermat’s little theorem.
258

Benoit Viguier's avatar
Benoit Viguier committed
259
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
260
261
262
263
264
265
266
267
We aim to give a quick view of how Montgomery curves are
defined and remind the reader of the ``twisting factor''. The
computation of n' is required for the security of X25519 as
it reduces the computations to a prime-order group, we use
this presentation to refer it later as ``clamping''. We
modified Subsection D to omit all the code definitions of small
functions to ease the reader experience. The C definitions
are now provided in the appendix.
Benoit Viguier's avatar
Benoit Viguier committed
268
269
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
270
271
272
273
274
275
276
p.3: I very much liked the discussion of the Diff between
TweetNaCl and your modifications! I imagine that many of
them are conceptually interesting in that they make verification
easier. I would have enjoyed reading a conceptual discussion
of the differences. Instead, Appendix A just contains a
Diff, and as a reader, I would need to perform the extraction
of insights myself.
277

Benoit Viguier's avatar
Benoit Viguier committed
278
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
typos    
Benoit Viguier committed
279
280
Due to page restrictions for IEEE S\&P, including appendices,
We had a condensed diff. We changed the format to
Benoit Viguier's avatar
Benoit Viguier committed
281
a ``diff -u'' to provide the context of the applied changes. We
Benoit Viguier's avatar
Benoit Viguier committed
282
283
also now describe the motivations of each changes below
the said Diff.
Benoit Viguier's avatar
Benoit Viguier committed
284
285
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
286
287
288
289
p.5: CSWAP: Maybe use a backward reference to p.3 where
CSWAP was defined, since in between, there was a lot of
content, and relying on the reader's memory does not really
work here (or at least, it did not work for me).
290

Benoit Viguier's avatar
Benoit Viguier committed
291
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
292
293
294
As we rewrote significantly section 2.4, the space between
the definition and the use of CSWAP decreased. We added a
backward reference to where it was originally defined.
Benoit Viguier's avatar
Benoit Viguier committed
295
296
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
297
298
299
300
301
p.7: I enjoyed the discussion on aliasing! This was the type
of conceptual discussion I find interesting. I was confused
about the mentioning that the case distinction k=0,1,2 does
not cover "all cases" - all cases of what? And why is this
distinction sufficient for the task at hand?
302

Benoit Viguier's avatar
Benoit Viguier committed
303
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
304
In that section we clarified the discussion of what
Benoit Viguier's avatar
typos    
Benoit Viguier committed
305
would be an unnecessary aliasing case and why such case do
Benoit Viguier's avatar
Benoit Viguier committed
306
not happen in TweetNaCl. For example, TweetNaCl never
Benoit Viguier's avatar
Benoit Viguier committed
307
308
309
has function calls where the 3 pointers are aliased (\texttt{o = a = b}),
as such we do not consider this aliasing case in the
specifications of the function.
Benoit Viguier's avatar
Benoit Viguier committed
310
311
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
312
313
314
315
Most of the rest of the paper felt hard to read, because it
read like a chronological enumeration of all steps. I think that
it would be much more interesting if the paper highlights the
interesting aspects of the verification.
316

Benoit Viguier's avatar
Benoit Viguier committed
317
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
318
319
320
321
We removed sections and details in order to simplify the
reading experience. We also added figures in section V in
order to provide the reader a mental image of how the lemmas,
definitions and theorems work together.
Benoit Viguier's avatar
Benoit Viguier committed
322
323
\end{answer}

324
325
Related work:

Benoit Viguier's avatar
Benoit Viguier committed
326
327
328
329
330
331
332
333
\newcommand{\rbar}{\cite{DBLP:journals/corr/BhargavanDFHPRR17}}

In reference \rbar, the order of authors is different than
in the original publication. I think that you might want to
discuss \rbar in the Related work section, since it seems quite
close. I was wondering whether you consider the approach
in \rbar as synthesis or verification, because to me, it seemed
a mix/neither.
334

Benoit Viguier's avatar
Benoit Viguier committed
335
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
336
337
338
339
The bibtex was from DBLP. We fixed the order of the
authors with respect to the original publication and contacted
DBLP to update their files.

Benoit Viguier's avatar
Benoit Viguier committed
340
341
342
\fref{tikz:LowVST} highlights the difference between Low*
and our approach.

Benoit Viguier's avatar
Benoit Viguier committed
343
344
345
\begin{figure}[H]
\centering
\include{tikz/low}
Benoit Viguier's avatar
Benoit Viguier committed
346
\caption{The VST vs Low*}
Benoit Viguier's avatar
Benoit Viguier committed
347
348
\label{tikz:LowVST}
\end{figure}
Benoit Viguier's avatar
Benoit Viguier committed
349
350
351

Low* generates C code, thus this is synthesis. We generate
Clight from C code, thus this is verification. Because Low*
Benoit Viguier's avatar
typos    
Benoit Viguier committed
352
also has a verification step with respect to some high-level
Benoit Viguier's avatar
Benoit Viguier committed
353
specifications, we consider their process to be a mix of the
Benoit Viguier's avatar
Benoit Viguier committed
354
355
356
357
358
two methods. Also to be noted that both the VST and Low*
allow the verification of memory safety.
% However Low* provides
% sidechannel securities while the VST allow verification
% of concurent programs.
Benoit Viguier's avatar
Benoit Viguier committed
359
360
\end{answer}

361
362
Clarification in intro:

Benoit Viguier's avatar
Benoit Viguier committed
363
364
The intro states that this is, to the authors knowledge, the
first use of Verifiable Software Toolchain (VST) in software
Benoit Viguier's avatar
typos    
Benoit Viguier committed
365
verification of an implementation of an asymmetric cryptographic
Benoit Viguier's avatar
Benoit Viguier committed
366
367
368
primitives. Does this mean that VST has been used
for symmetric cryptographic primitives before? From the text,
I wasn’t sure whether this is careful quantification or not.
369

Benoit Viguier's avatar
Benoit Viguier committed
370
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
371
This is indeed careful quantification. The VST has already
Benoit Viguier's avatar
typos    
Benoit Viguier committed
372
been used to verify symmetric Cryptographic primitives
Benoit Viguier's avatar
Benoit Viguier committed
373
(\eg SHA), as mentioned later by \cite{Beringer2015VerifiedCA} and \cite{2015-Appel}.
Benoit Viguier's avatar
Benoit Viguier committed
374
\end{answer}
375

Benoit Viguier's avatar
Benoit Viguier committed
376

377
378
\subsection{S\&P 2020 Review \#582C}

Benoit Viguier's avatar
Benoit Viguier committed
379
380
Overall merit: 3. Weak reject - The paper has flaws, but I will
not argue against it.
381
382
383
384
385
386


\begin{center}
  \subheading{===== Brief paper summary (2-3 sentences) =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
387
388
389
390
391
392
393
This paper presents a formalization of the X25519
(Curve25519) elliptic curve Diffie-Hellman (ECDH)
construction in Coq, and uses this formalization to verify the
functional correctness of a C implementation of this
construction taken from the TweetNaCl library. Going further than
prior work, the authors also link their Coq specification to a
mathematical theory of elliptic curves in Coq.
394
395
396
397
398
399


\begin{center}
  \subheading{===== Strengths =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
400
401
Proofs of cryptographic algorithms like X25519 tend to
mean different things in different communities: (a) one may
Benoit Viguier's avatar
typos    
Benoit Viguier committed
402
403
prove that X25519 implements a group based on the mathematical
theory of elliptic curves, (b) one may prove that an
Benoit Viguier's avatar
Benoit Viguier committed
404
X25519 implementation meets its mathematical spec, or (c)
Benoit Viguier's avatar
typos    
Benoit Viguier committed
405
406
one may prove that a protocol that uses X25519 is provably
secure, based on some cryptographic assumption on the ECDH
Benoit Viguier's avatar
Benoit Viguier committed
407
408
409
410
411
412
construction. It is rare to find papers that combine more than
one of these proof levels, and this paper does a creditable
job of linking (a) with (b), relying on the Coq framework to
soundly glue these proofs together. Although a similar goal
was considered in \cite{Zinzindohoue2016AVE}, this paper provides a more satisfying
solution by not leaving any gaps between the formalizations,
Benoit Viguier's avatar
Benoit Viguier committed
413
and by relying on a smaller trusted computing base.
414
415
416
417
418
419


\begin{center}
  \subheading{===== Weaknesses =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
420
421
422
423
X25519 implementations have now been verifying in multiple
papers using multiple verification frameworks, and \cite{Erbsen2016SystematicSO}
even uses Coq to verify a large portion of a C implementation
of X25519 fully automatically. So, the main contribution
Benoit Viguier's avatar
typos    
Benoit Viguier committed
424
425
here is that that the authors verify an existing popular
implementation (TweetNaCl) without making many changes to
Benoit Viguier's avatar
Benoit Viguier committed
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
the source code. Still, TweetNaCl is not necessarily the most
complex (and certainly not the most efficient) implementation
of X25519 that has been verified, which makes the novelty of
this work hard to justify.

\newcommand{\mitp}{\cite{Erbsen2016SystematicSO}}


\begin{answer}{EEEEEE}
Indeed \mitp's C code of X25519 is verified. However the
authors do not qualify their approach as verification but
as synthesis. They do not use Coq to verify C code, instead they
``synthesize'' (generate) C code from verified refinements of
the specification. Our approach goes from the C code up to the
specification.
 % which is completely different.

\begin{figure}[H]
\centering
\include{tikz/mit}
\caption{Our approach vs \mitp}
Benoit Viguier's avatar
Benoit Viguier committed
447
\label{tikz:MitVST}
Benoit Viguier's avatar
Benoit Viguier committed
448
449
450
\end{figure}

\end{answer}
451
452
453
454
455
456


\begin{center}
  \subheading{===== Detailed comments for the author(s) =====}
\end{center}

Benoit Viguier's avatar
Benoit Viguier committed
457
458
459
460
461
I like the approach taken in this paper and I think this work
has value and should be published. However, I am not sure
the current presentation of the work works well.

The paper can be essentially divided into two components:
Benoit Viguier's avatar
typos    
Benoit Viguier committed
462
463
464
the proof of TweetNaCl using VST, and the proof of equivalence
between the Coq spec of RFC7748 and the mathematical
theory of Curve25519. The details of both are interesting
Benoit Viguier's avatar
Benoit Viguier committed
465
to formalists but the Coq details are quite hard to parse and
Benoit Viguier's avatar
typos    
Benoit Viguier committed
466
467
distracting when trying to understand the text. This is a well-known
problem for formal verification papers, and I don’t
Benoit Viguier's avatar
Benoit Viguier committed
468
469
470
have great advice except to suggest that the authors separate
out the code fragments into figures and let the text focus on
the high-level ideas of the code.
471

Benoit Viguier's avatar
Benoit Viguier committed
472
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
473
We removed a significant part of the Coq details, especially
Benoit Viguier's avatar
typos    
Benoit Viguier committed
474
475
details about reflections in order to make the reading
experience smooth. As suggested, we also added a few figures to
Benoit Viguier's avatar
Benoit Viguier committed
476
477
give the reader an overview of how the proofs are linked
together.
Benoit Viguier's avatar
Benoit Viguier committed
478
479
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
480
481
482
483
484
485
At the end of Section IV, I would have loved to see some
high-level lessons on what the proof taught you, and what
part of this proof would be reusable if you decided to verify
Ed25519 or X448 or P-256, for example. This is particularly
important for this work, since prior papers have shown how
to share proof effort across multiple curves.
486

Benoit Viguier's avatar
Benoit Viguier committed
487
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
488
489
We added insights in \sref{subsec:with-VST} of how to improve
working with the VST verification framework. In section \sref{sec:Conclusion},
Benoit Viguier's avatar
typos    
Benoit Viguier committed
490
we described in further details how our work can
Benoit Viguier's avatar
Benoit Viguier committed
491
492
493
494
495
496
497
498
499
500
be extended to other curves. The TweetNaCl ed25519
implementation makes use of the same low level arithmetic
as X25519, reusing our proofs. For example, \TNaCle{pow2523} is
similar to \TNaCle{inv25519} and would allow us to reuse our
reflection abstraction. X448 would reuse the ladder but the
low level arithmetic would need to be proven again. P-256
is a different case as due to its short Weierstra\ss{} shape, this
implies that our ladder is not fit for it. However using \cite{BartziaS14}
and our proofs as example it is possible to prove a similar
ladder as ours.
Benoit Viguier's avatar
Benoit Viguier committed
501
502
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
503
504
505
It also appears that the authors do not verify the constant-time
guarantees of the TweetNaCl code. Could this be done
in their framework?
506

Benoit Viguier's avatar
Benoit Viguier committed
507
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
typos    
Benoit Viguier committed
508
509
Constant-timeness is not a property verifiable with the VST.
This is not verifiable with our framework.
Benoit Viguier's avatar
Benoit Viguier committed
510
% Related on CompCert: https://eprint.iacr.org/2019/926.pdf
Benoit Viguier's avatar
Benoit Viguier committed
511
512
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
513
514
515
516
517
518
519
520
Section V presents the proof of mathematical equivalence.
It appears to me that this proof is completely independent of
the TweetNaCl proof. Is that the case? Is there any lemma
from the first part that is needed in the second? More
importantly, could you claim that your proof of equivalence also
provides a justification for the implementations of Fiat Crypto
or HACL*, hence adding value to those other projects in addition
to your own?
521

Benoit Viguier's avatar
Benoit Viguier committed
522
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
523
524
525
526
527
528
529
Indeed those two proofs are completely independent. The
only link between \sref{sec:C-Coq} and \sref{sec:maths} is the definition
of \Coqe{RFC} and the preconditions on the inputs: 2 arrays of
32 bytes. We highlighted in \sref{sec:Conclusion} that our proof of
correctness of X25519 in RFC~7748 increases the confidence
in other implementations such as Fiat Crypto and HACL*
(under the assumption they correctly formalized the RFC).
Benoit Viguier's avatar
Benoit Viguier committed
530
531
\end{answer}

Benoit Viguier's avatar
Benoit Viguier committed
532
533
534
535
536
537
I was hoping to see where the ``clamping'' used in X25519
would appear in the formalization of Section V but was unable
to spot it. Does clamping affect the proofs in any way? Is there
a stronger property you could prove because of the clamping
(e.g. membership in the prime-order group)? Do you already
prove such a property?
Benoit Viguier's avatar
Benoit Viguier committed
538

Benoit Viguier's avatar
Benoit Viguier committed
539
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
540
541
542
543
544
The clamping by itself has no impact on the computations using the ladder.
It is thus normal to not see it appear in \sref{sec:maths} as our proofs work for any 255-bit $n$,
We prove the correctness of X25519 in RFC~7748, we do not prove its security.
The proof of a stronger property (e.g. membership in prime-order group)
shall be done separately before being applied to Curve25519.
Benoit Viguier's avatar
Benoit Viguier committed
545
\end{answer}
Benoit Viguier's avatar
Benoit Viguier committed
546

Benoit Viguier's avatar
Benoit Viguier committed
547
548
More generally, what about the proof of Section V is
specific to X25519 and what is generic?
Benoit Viguier's avatar
Benoit Viguier committed
549

Benoit Viguier's avatar
Benoit Viguier committed
550
\begin{answer}{EEEEEE}
Benoit Viguier's avatar
Benoit Viguier committed
551
552
Everything in \sref{subsec:ECC} is generic, anything left in \sref{subsec:curve_twist_fields}
is specific to X25519.
Benoit Viguier's avatar
Benoit Viguier committed
553
\end{answer}