0-todo.tex 4.41 KB
Newer Older
Benoit Viguier's avatar
Benoit Viguier committed
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
\todo{

- Get down to 12 pages: "no more than 12 pages long, excluding the bibliography,
well-marked appendices, and supplementary material."

- Emphasize:\\
+ the added confidence between in X25519 Correctness\\
+ proof of real world software\\

- Add section to describe what would need to be done to adapt the code for e.g.
curve448 (give reference) and X448.\\
+ we can reuse the code of the elliptic abstraction.\\
+ the ladder would need few adaptation with respect to the bound propagations.\\
+ the ladder is generic so can be easily instanciated over \F{2^{448} - 2^{224}
   - 1}.\\
+ the Addition and subtraction are simple and bounds carries easily.\\
+ Multiplication needs to be redefined.\\
+ Squaring can be easily ported.\\
+ Inversion is easily ported with the use of reflections, idem for the packing.\\

- Remove reflection section.\\
+ simplify writting.\\
+ Still mention reflection but don't describe more than that.\\

- Changed made to TweetNaCl:\\
+ we contacted the authors.\\
+ only change made are the one required by VST\\
+ Should have a look at the Multiplication}

With respect to the reviews:

\todo{

- Give number of person-hours

- "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."\\
+ anotation have to be carried out through the proof to help the smt-solver,
not in our case as we direct the proof.

- "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."\\
+ I don't know what to do on that one.

- "the discussion of the computation of n’ was completely unclear to me."\\
+ describe the process of clamping better.

- "Instead, Appendix A just contains a Diff, and as a reader, I
would need to perform the extraction of insights myself."\\
+ => changed the Appendix A format to diff -u to give more context

- "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)"

- "all cases of what? And why is this distinction sufficient for
the task at hand?"\\
+ remove the sentence or show by example which aliasing case is not needed?

- "[13], the order of authors is different than in the original publication."\\
- "I was wondering whether you consider the approach in [13] as synthesis or
verification, because to me, it seemed a mix/neither."\\
+ [13] is "Verified Low-Level Programming Embedded in F*",\\
+ \strikethrough{fixed authors order}.\\
+ reread [13] and answer in the "our answer part"

- "[18] even uses Coq to verify a large portion of a C implementation of X25519
fully automatically."\\
+ This is not verification, this is synthesis. The approach is completely different.

- "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."\\
+ True, but all the other works have been from a spec and generate correct code
approach, here we go the opposite way. While the code of other libraries are
different, the montgomery ladder are often similar and the optimizations comes
mostly from the big number computations.\\

- "This is a well-known problem for formal
verification papers, and I don’t 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."\\
+ How to address that ?

- "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."\\
+ see second Todo

- "It also appears that the authors do not verify the constant-time
guarantees of the TweetNaCl code. Could this be done in their
framework?"
+ Nope => mention in limitation at the end of the paper?

- Clamping and section V.\\
+ The clamping allows to reduce the group to prime elements, we do not provide
such proofs.\\
- We prove that for all n the computations on the ladder holds.

- "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?"
+ Peter ?
}