usenix-a.tex 19.1 KB
 Peter Schwabe committed Oct 01, 2020 1 \section*{Usenix Security 2020 Review \#324A}  Peter Schwabe committed Oct 01, 2020 2   Peter Schwabe committed Oct 01, 2020 3 \begin{tabular}{rrp{.6\textwidth}}  Peter Schwabe committed Oct 01, 2020 4  \toprule  benoit committed Oct 01, 2020 5 6 7 8  Review recommendation & 3. & Major revision \\ Writing quality & 3. & Adequate \\ Reviewer interest & 2. & I might go to a talk about this \\ Reviewer expertise & 3. & Knowledgeable \\  Peter Schwabe committed Oct 01, 2020 9  \bottomrule  Peter Schwabe committed Oct 01, 2020 10 11 12 13 14 15 \end{tabular} \begin{center}  Peter Schwabe committed Oct 01, 2020 16  \subheading{===== Paper summary =====}  Peter Schwabe committed Oct 01, 2020 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 \end{center} The Networking and Cryptography library (NaCl) admits a compact implementation, TweetNaCl, that leans toward clarity over efficiency. A key component of these libraries is the key exchange protocol poetically known as X25519, after the parameters of the elliptic curve over which it carries its computations. This paper presents a proof of correctness of the TweetNaCl implementation of X25519. This result is thorough and offers novel contributions in several aspects. First it is a formal proof conducted in the Coq Proof Assistant, hence relying on a minimalist trust base. Second, it proves the correctness of the existing C implementation of the protocol (except for minor technical necessary changes), as opposed to a re-implementation designed with its formal proof in mind. Finally, it not only prove the correctness of the C implementation against a purely functional formalization of the RFC standard of the protocol, but also the correctness of this formalized standard against (a formalization of) the purely "mathematical" definition of the protocol as introduced by Bernstein. The functional refinement of the C implementation is established using VST, the separation logic for C developed at Princeton. Beyond being the adequate tool for such a task, it also in principle allows for a compilation of TweetNaCl through CompCert guaranteeing the result to be transported down to the assembly. The equivalence between the RFC specification and the mathematical counterpart is conducted by (significantly) extending the work on formal elliptic curves by Bartzia and Strub. It relies on ssreflect and MathComp, but is overall a more traditional Coq proof. The complete formal development is provided as an artifact. \begin{center}  Peter Schwabe committed Oct 01, 2020 50  \subheading{===== Strengths =====}  Peter Schwabe committed Oct 01, 2020 51 52 53 \end{center} I believe this paper describes a valuable work and contribution, that I appreciated learning about. \begin{itemize}  Peter Schwabe committed Oct 01, 2020 54 55 56 57 58 59 60 61  \item The authors follow a thorough and valuable methodology, establishing excellent guarantees on the implementation considered. \item It is great to see a development such as VST being used in this context. \item Additionally, going the extra-mile to both refine the C code against RFC and prove this specification to be equivalent to the mathematical model is indeed I believe the right way to go. \item They position their paper in a quite dense corpus of work in a quite satisfactory way. \item The provided artifact showcase a significant proof effort. \item I found barely a couple of typos while reading the paper. \item The conclusion is particularly nice. \item The diff provided between the verified C code and the original code is excellent. Overall there is a great care in stating clearly and precisely what has been proved.  Peter Schwabe committed Oct 01, 2020 62 63 64 \end{itemize} \begin{center}  Peter Schwabe committed Oct 01, 2020 65  \subheading{===== Weaknesses =====}  Peter Schwabe committed Oct 01, 2020 66 67 68 69 \end{center} Such a paper is difficult to write. The authors have visibly devoted great efforts to tackle this difficulty, but it remains a challenging read. \begin{itemize}  Peter Schwabe committed Oct 01, 2020 70  \item The paper takes us from one technical point to another in a manner that seems arbitrary at times, and hinders the overall structure. The problem is quite global, but a typical example is Definition 2.3: as a non-expert, it is hard to understand why this notion is important to introduce here, and it is essentially not used anywhere in the paper.  Peter Schwabe committed Oct 01, 2020 71 \end{itemize}  Peter Schwabe committed Oct 01, 2020 72 \begin{answer}  Peter Schwabe committed Oct 01, 2020 73  The notion of the twist of Curve25519 is quite central in the proof of the second main theorem of our paper,  benoit committed Oct 01, 2020 74  which is linking our formalization of the RFC to the mathematical definition of Curve25519.  Peter Schwabe committed Oct 01, 2020 75 76  We therefore feel like it should not be omitted from the preliminaries, but we are of course open to suggestions how to motivate the definition better at this early point of the paper.  Peter Schwabe committed Oct 01, 2020 77 78 79 \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 80 81 82 83 84 85 86  \item Figure 1 and Figure 4 are great, and have the potential to help so much the reader against the previous issue. Unfortunately, they are not commenting, and hence fail to do so! \end{itemize} \begin{answer} We extended the discussion of Figures 1, 3, and 4 to address this point. \end{answer} \begin{itemize} \item The protocol considered is standard, and its implementation made to be of reasonable complexity. The paper should therefore really aim to:  benoit committed Oct 01, 2020 87 88 89 90 91  \begin{enumerate} \item promote a new approach (full stack, use of VST, use of the B\&S elliptic curve library,...) \item explain all specific difficulties and unexpected problems that came across to smooth the path to similar projects in the future; \item give a sense of whether it would scale and/or be reusable for similar/related projects. In particular, the choice of TweetNaCl is never really motivated. How much of a challenge would proving the same result over a more complex/efficient implementation be? \end{enumerate}  Peter Schwabe committed Oct 01, 2020 92   benoit committed Oct 01, 2020 93  The paper does a good job at 1, but unfortunately a quite poor at 2 and 3.  Peter Schwabe committed Oct 01, 2020 94  \item Skimming through the development convinces me that this is a consequent work. But the paper does not help evaluating this effort. It is always difficult to find relevant metrics to evaluate such things, but it would be great to get a sense of the aspects of the work that turned out difficult, and the extent of these difficulties.  Peter Schwabe committed Oct 01, 2020 95 \end{itemize}  Peter Schwabe committed Oct 01, 2020 96 97 98 99 \begin{answer} \todo{We should say something regarding these two points.} \end{answer}  Peter Schwabe committed Oct 01, 2020 100 101  \begin{center}  Peter Schwabe committed Oct 01, 2020 102  \subheading{===== Detailed comments for authors =====}  Peter Schwabe committed Oct 01, 2020 103 104 105 106 107 108 109 110 111 \end{center} My feelings are essentially summed up through the strengths and weaknesses described above. I find this work to be a great contribution, but regret having a hard time getting as much as I would like out of the paper. You mention in the rebuttal to a previous submission that constant time is not a property that fits in VST's Framework. This is indeed true, and absolutely fair not to cover it in this work, but a short discussion about constant time would nonetheless be interesting I think, for instance in the conclusion. In particular, we are getting quite close to having the adequate facilities for establishing Constant Time of real implementation in the style of this work: this year at POPL was presented an extension of CompCert proved to transport Constant Time from CLight to assembly: "Formal Verification of a Constant-Time Preserving C Compiler", POPL'20, Barthe et al. On a side note, I failed to compile the project: setting up an opam switch with Coq pinned to 8.8.2 as instructed, I had dependency issues with respect to coq-coqprimewhen running opam install --deps-only coq-verif-tweetnacl . Having installed manually coq-coqprime, I then ended up with the following error: {\footnotesize\texttt{  Peter Schwabe committed Oct 01, 2020 112 113 114 115 116  "The following dependencies couldn't be met:\\ - coq-verif-tweetnacl $\rightarrow$ coq-stdpp \\ unknown package\\ No solution found, exiting"}} \begin{answer}  benoit committed Oct 01, 2020 117  We were not able to reproduce this error, but  Peter Schwabe committed Oct 01, 2020 118 119 120  now make the code available in an anonymous GitHub repository that also contains a virtual-machine image with all software that is required to reproduce the proofs. \end{answer}  Peter Schwabe committed Oct 01, 2020 121 122 123 124  Here are a few linear comments: \begin{itemize}  Peter Schwabe committed Oct 01, 2020 125  \item \textbf{page 1, column 2:}\\  benoit committed Oct 01, 2020 126 127 128  - "the program satisfy" $\rightarrow$ "the program satisfies"\\ - "the result of this paper can readily be used in mechanized proofs of higher-level protocols (...)" This statement should probably be made more precise, it is quite unclear to me what you mean exactly.  Peter Schwabe committed Oct 01, 2020 129 \end{itemize}  Peter Schwabe committed Oct 01, 2020 130 \begin{answer}  benoit committed Oct 01, 2020 131 132 133 134  \begin{itemize} \item[$-$] Typo fixed (the satisfy/satisfies actually refers to the semantics of a program in this sentence). \item[$-$]We rephrased the second statement to (hopefully) clarify what we mean. \end{itemize}  Peter Schwabe committed Oct 01, 2020 135 136 137 \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 138  \item \textbf{page 2:}\\  benoit committed Oct 01, 2020 139  Figure 1 is great, but would deserve a lengthy explanation!  Peter Schwabe committed Oct 01, 2020 140 141 142 143 \end{itemize} \begin{answer} We added an additional description of the figure. \end{answer}  Peter Schwabe committed Oct 01, 2020 144   Peter Schwabe committed Oct 01, 2020 145 \begin{itemize}  Peter Schwabe committed Oct 01, 2020 146   Peter Schwabe committed Oct 01, 2020 147  \item \textbf{page 3, column 1:}\\  benoit committed Oct 01, 2020 148 149 150  Definition 2.3: It's been very unclear to me as a non-expert in cryptography and this protocole in particular what was the purpose of this definition.\\ {\color{gray}"depending of" $\rightarrow$ "depending on"}\\ "depending of the value of the kth bit" $\rightarrow$ unclear what k is at this point  Peter Schwabe committed Oct 01, 2020 151 152 \end{itemize} \begin{answer}  benoit committed Oct 01, 2020 153 154 155 156 157  \begin{itemize} \item[$-$] Regarding Definition 2.3 see our answer above. \item[$-$] Typo fixed. \item[$-$] We updated the text to clarify what we mean by the $k$th bit. \end{itemize}  Peter Schwabe committed Oct 01, 2020 158 \end{answer}  Peter Schwabe committed Oct 01, 2020 159   Peter Schwabe committed Oct 01, 2020 160 161 \begin{itemize} \item \textbf{page 3, column 2:}\\  benoit committed Oct 01, 2020 162 163  Algorithm 1: unclear what "m" is\\ "RFC 7748 standardize" $\rightarrow$ "RFC 7748 standardizes"  Peter Schwabe committed Oct 01, 2020 164 165 166 167 \end{itemize} \begin{answer} Clarified that $m$ is an upper bound on the bitlength of the scalar. Typo fixed. \end{answer}  Peter Schwabe committed Oct 01, 2020 168   Peter Schwabe committed Oct 01, 2020 169 170 \begin{itemize} \item \textbf{page 4, column 2:}\\  benoit committed Oct 01, 2020 171 172 173 174  It's minor, but it is more shiny nowadays to cite The Odd Order theorem that the Four Color theorem as a mathematical achievement in Coq\\ CompCert $\rightarrow$ Wrong hyphenation\\ Hoare-seq $\rightarrow$ It is clearly hard to find the balance with respect to what should be assumed on the crypto side, and what should be assumed on the verification side. I nonetheless think that this should be omitted.\\ "Separation logic is an extension of Hoare logic" $\rightarrow$ Minor, but the work "extension" does not quite sit right with me. The model is quite intrinsically different.  Peter Schwabe committed Oct 01, 2020 175 176 \end{itemize} \begin{answer}  Peter Schwabe committed Oct 01, 2020 177  \begin{itemize}  benoit committed Oct 01, 2020 178 179 180 181  \item[$-$] While the Odd Order theorem is shinier for the complexity of the work, it may not be as well known as the Four Color theorem. This lack of exposition makes its proof less impressive to readers not familiar with the subject. \item[$-$] We fixed the hyphenation. \item[$-$] The Hoare logic is not a known subject for most cryptographers not familiar with formal methods. In our opinion, the Hoare-Sec rule is the easiest rule with material (as opposed to Hoare-Skip) to understand by its composition nature and as it also relates to how instructions are read in the source code of a program. \item[$-$] The Separation Logic was introduced by their authors \emph{an extension of Hoare logic''}. See See \url{https://www.cs.cmu.edu/~jcr/seplogic.pdf}.  Peter Schwabe committed Oct 01, 2020 182  \end{itemize}  benoit committed Oct 01, 2020 183   Peter Schwabe committed Oct 01, 2020 184 \end{answer}  Peter Schwabe committed Oct 01, 2020 185   Peter Schwabe committed Oct 01, 2020 186 187 \begin{itemize} \item \textbf{page 5, column 2:}\\  benoit committed Oct 01, 2020 188  "'To implement (...)" $\rightarrow$ I am very confused by this. The whole paragraph is an unannounced quote, it would need context/explanation.  Peter Schwabe committed Oct 01, 2020 189 190 \end{itemize} \begin{answer}  benoit committed Oct 01, 2020 191  Fixed, we added an introduction sentence.  Peter Schwabe committed Oct 01, 2020 192 \end{answer}  Peter Schwabe committed Oct 01, 2020 193   Peter Schwabe committed Oct 01, 2020 194 195 \begin{itemize} \item \textbf{page 6, column 1:}\\  benoit committed Oct 01, 2020 196  In ListofZn\_fp $\rightarrow$ The use of fuel might deserve a comment. Don't you end up having to prove at some point that you can always compute ahead of time an overapproximation of the fuel needed? Wouldn't it have been simple to use the strong recursion principle of naturals to define the function?  Peter Schwabe committed Oct 01, 2020 197 \end{itemize}  benoit committed Oct 01, 2020 198 199 200 \begin{answer} In our case the fuel is used to garantee to have as an output a list of 32 elements. This allows us to prove that for all List of 32 bytes, ListofZn\_fp (ZofList L) = L. With this lemma at hand we can later simplify some of the expressions. \end{answer}  Peter Schwabe committed Oct 01, 2020 201   Peter Schwabe committed Oct 01, 2020 202 203 \begin{itemize} \item \textbf{page 6, column 2:}\\  benoit committed Oct 01, 2020 204 205  "and the same code as a pure Coq function" $\rightarrow$ I would rephrase, the term "same code" is misleading. Specification: I think explaining the structure of a VST statement would be necessary to help an unfamiliar reader understand this specification.  Peter Schwabe committed Oct 01, 2020 206 207 \end{itemize} \begin{answer}  benoit committed Oct 01, 2020 208 209  We rephrased this paragraph to avoid misleading the reader on the translations done.\\ \todo{add some more text before "In this specification we state preconditions like:" ?}  Peter Schwabe committed Oct 01, 2020 210 \end{answer}  Peter Schwabe committed Oct 01, 2020 211   Peter Schwabe committed Oct 01, 2020 212 \begin{itemize}  Peter Schwabe committed Oct 01, 2020 213  \item \textbf{page 7:}\\  benoit committed Oct 01, 2020 214 215 216 217 218  Discussion on memory aliasing is great, I would have liked more of this kind through the paper.\\ Figure 2: I had to fish back a little for the definition of "sh", but "Ews" has really never been defined I believe.\\ "Improving speed" $\rightarrow$ of what? This whole paragraph is quite hard to read. In particular be careful that it is not obvious to the reader whether you are speeding up the verification process or the runtime of the implementation. In particular it was unclear to me what you were referring to by saying "Optimizations of such definitions".\\ The following paragraph also is a bit cryptic. I assume you are saying that identifying finely the dependencies between definitions allow for parallelizing the work? Arguably, simply admitting temporarily on the fly any specification needed achieves the same.\\ "Numbers in gf" $\rightarrow$ Please remind the reader what "gf" is. Good section overall  Peter Schwabe committed Oct 01, 2020 219 220 \end{itemize} \begin{answer}  benoit committed Oct 01, 2020 221 222 223 224 225 226  \begin{itemize} \item[$-$] We added a description of "Ews" in the precondition paragraph, this should clarify the global memory share name. \item[$-$] We clarified that we improve the speed of the verification effort. Optimization of such definition'' refers to the will of some developers to use for example a fancy recursive definition of a function. \item[$-$] In order to verify a file, Coq need the compiled proof of dependencies. However in the case of VST it is possible to split the specification from the proof, as a result the proof of the full scalar multiplication does not require the proof of the the multiplication in \F{p}, only its specification. \item[$-$] We reminded the reader that "gf" is a C type. \end{itemize}  Peter Schwabe committed Oct 01, 2020 227 \end{answer}  Peter Schwabe committed Oct 01, 2020 228   Peter Schwabe committed Oct 01, 2020 229 \begin{itemize}  Peter Schwabe committed Oct 01, 2020 230  \item \textbf{page 8:}\\  benoit committed Oct 01, 2020 231 232  "Using reflection (...)" $\rightarrow$ Would deserve more explanations.\\ Figure 3: Please comment generously this figure, it looks great but it is frustrating to try to decipher it without help.  Peter Schwabe committed Oct 01, 2020 233 234 \end{itemize} \begin{answer}  benoit committed Oct 01, 2020 235 236 237 238  \begin{itemize} \item[$-$] We removed the reflection mention, more explanations would require too many implementation details. \item[$-$] We added a paragraph to describe the content of Figure 3. \end{itemize}  Peter Schwabe committed Oct 01, 2020 239 \end{answer}  Peter Schwabe committed Oct 01, 2020 240   Peter Schwabe committed Oct 01, 2020 241 \begin{itemize}  Peter Schwabe committed Oct 01, 2020 242  \item \textbf{page 9:}\\  benoit committed Oct 01, 2020 243 244  "the type of field which characteristic" $\rightarrow$ "whose characteristic"\\ "The value of add is proven to be on the curve (with coercion)" $\rightarrow$ This parenthesis is too cryptic, it should probably be dropped.  Peter Schwabe committed Oct 01, 2020 245 246 247 248 \end{itemize} \begin{answer} Fixed. \end{answer}  Peter Schwabe committed Oct 01, 2020 249   Peter Schwabe committed Oct 01, 2020 250 251 \begin{itemize} \item \textbf{page 11:}\\  benoit committed Oct 01, 2020 252  Figure 4: this one is the apex: it would deserve a full column of explanations  Peter Schwabe committed Oct 01, 2020 253 254 \end{itemize} \begin{answer}  benoit committed Oct 01, 2020 255 256  In addition to Figure 4, we added a full paragraph providing the red line of the proof of this theorem. We hope to provide suficiant insights of the dependencies between lemmas to arrive into the final theorem.  Peter Schwabe committed Oct 01, 2020 257 \end{answer}  Peter Schwabe committed Oct 01, 2020 258   Peter Schwabe committed Oct 01, 2020 259 260 \begin{itemize} \item \textbf{Conclusion:}\\  benoit committed Oct 01, 2020 261 262 263 264  Great wrap up overall.\\ CompCert: "However, when compiling (...)" $\rightarrow$ I am quite confused about this sentence. Do you mean when compiling the verified C code with gcc? If so, beyond the question whether CompCert matches C17 (which it doesn't, it matches C99), the real problem is to assume that gcc is bug free! I would expect with this whole approach that the expectation is to run a protocole compiled with CompCert.\\ clightGen: "VST does not support (...)" $\rightarrow$ Hard to undertand the relation between this sentence and the previous one.\\ Extending our work: What about proving other NaCl implementations?  Peter Schwabe committed Oct 01, 2020 265 266 \end{itemize}  Peter Schwabe committed Oct 01, 2020 267 \begin{answer}  Peter Schwabe committed Oct 01, 2020 268  \todo{Freek : which version of ISO.}  Peter Schwabe committed Oct 01, 2020 269 270 271 \end{answer} \begin{center}  Peter Schwabe committed Oct 01, 2020 272  \subheading{===== Requested changes =====}  Peter Schwabe committed Oct 01, 2020 273 274 \end{center} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 275  \item Please provide high level explanations to your three Figures describing the infrastructure.  Peter Schwabe committed Oct 01, 2020 276 277 \end{itemize} \begin{answer}  benoit committed Oct 01, 2020 278  We added high-level description of Figures 1, 3 and 4. They should help the reader to follow the line of the proof.  Peter Schwabe committed Oct 01, 2020 279 280 \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 281  \item Please reduce slightly the width of the technical material covered, and use the gained space to provide a bit more context to the one covered  Peter Schwabe committed Oct 01, 2020 282 283 284 285 286 287 \end{itemize} \begin{answer} We removed various technical details, in particular in Section 5. We used the space to extend the discussion of various other points raised by the reviewers. \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 288  \item Please provide more get away lessons from this development that would benefit new similar works  Peter Schwabe committed Oct 01, 2020 289 290 291 292 293 \end{itemize} \begin{answer} We added a lessons learned'' paragraph in the conclusion. \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 294  \item Please give a sense of the difficulties encountered during the formalization.  Peter Schwabe committed Oct 01, 2020 295 \end{itemize}  Peter Schwabe committed Oct 01, 2020 296 297 298 \begin{answer} Many difficulties were of technical nature; we cover some of this now in the lessons learned'' paragraph. \end{answer}  Peter Schwabe committed Oct 01, 2020 299 300  \begin{center}  Peter Schwabe committed Oct 01, 2020 301  \subheading{===== Questions for authors' response =====}  Peter Schwabe committed Oct 01, 2020 302 303 304 \end{center} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 305  \item What made TweetNaCl the right choice for this project?  Peter Schwabe committed Oct 01, 2020 306 307 \end{itemize}  Peter Schwabe committed Oct 01, 2020 308 \begin{answer}  Peter Schwabe committed Oct 01, 2020 309 310 311 312 313  One goal of the project was to investigate how suitable the combination of VST+Coq is for verifying correctness of existing C code for asymmetric crypto primitives. The X25519 implementation in TweetNaCl was chosen because it is relatively simple, it has some real-world use cases, and the original paper claims that the library should be verifiable.  Peter Schwabe committed Oct 01, 2020 314 315 316 \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 317  \item Would following the same approach for other implementation radically change the proof effort?  Peter Schwabe committed Oct 01, 2020 318 319 \end{itemize}  Peter Schwabe committed Oct 01, 2020 320 \begin{answer}  Peter Schwabe committed Oct 01, 2020 321 322 323 324 325  We would expect that the proof effort for another C implementation of X25519 does not change drastically, as long as it does not use any features that are not supported by VST (e.g., the 128-bit integers used by the donna64 implementation). The proof relating the RFC to the mathematical definition does not change for other implementations.  Peter Schwabe committed Oct 01, 2020 326 327 328 \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 329  \item Does compiling TweetNaCl with CompCert rather than gcc impact the performance beyond what is acceptable?  Peter Schwabe committed Oct 01, 2020 330 331 \end{itemize}  Peter Schwabe committed Oct 01, 2020 332 \begin{answer}  Peter Schwabe committed Oct 01, 2020 333 334 335 336 337  For the X25519 implementation in TweetNaCl, CompCert generates code that is about 6$\times$ slower than code generated with gcc. While this sounds like a lot, it may not be too much of an issue for projects that use TweetNaCl, because they chose for a library that prioritizes simplicity over performance in the first place. A more serious issue however can be the non-free CompCert license.  Peter Schwabe committed Oct 01, 2020 338 339 340 \end{answer} \begin{itemize}  Peter Schwabe committed Oct 01, 2020 341  \item If so, what trust do you consider this proof effort to bring to a gcc compiled implementation?  Peter Schwabe committed Oct 01, 2020 342 343 \end{itemize}  Peter Schwabe committed Oct 01, 2020 344 \begin{answer}  Peter Schwabe committed Oct 01, 2020 345 346 347 348 349  We are not aware of any bugs that were introduced into ECC software by bugs in gcc; so from a practical, crypto-engineering point of view we rule out all classes of bugs that users are typically concerned about. From a more theoretical point of view, relying on gcc (or any other unverified C compiler) massively expands the TCB and should be reason for concern.  Peter Schwabe committed Oct 01, 2020 350 \end{answer}