usenix-g.tex 2.53 KB
 Peter Schwabe committed Oct 01, 2020 1 \newpage  Peter Schwabe committed Oct 01, 2020 2 \section*{Usenix Security 2020 Review \#324G}  Peter Schwabe committed Oct 01, 2020 3   Peter Schwabe committed Oct 01, 2020 4 \begin{tabular}{rrp{.6\textwidth}}  Peter Schwabe committed Oct 01, 2020 5  \toprule  Peter Schwabe committed Oct 01, 2020 6 7 8 9  Review recommendation & 4.& Minor revision \\ Writing quality & 4.& Well-written \\ Reviewer interest & 2.& I might go to a talk about this \\ Reviewer expertise & 2.& Some familiarity \\  Peter Schwabe committed Oct 01, 2020 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  \bottomrule \end{tabular} \begin{center} \subheading{===== Paper summary =====} \end{center} The paper takes a C implementation of the X25519 DH operation in the TweetNaCl library and proves it is correct. This proof ocurrs in two stages. Firstly, the paper formalises RFC 7748, which standardised X25519, in Coq. Then it goes on to show the C code, the Coq reference and the mathematical definition coincide. \begin{center} \subheading{===== Strengths =====} \end{center} \begin{itemize} \item Clearly Written \item Comprehensive with respect to the studied object \item Most formally verified cryptography code is generated or written with verification in mind, so verifying arbitrary code is impressive. \end{itemize} \begin{center} \subheading{===== Weaknesses =====} \end{center} \begin{itemize} \item TweetNaCl is explicitly written as a simple and easy to audit library, compared to faster, more complex implementations. \item The paper does not extend tooling or provide general techniques. \end{itemize} \begin{center} \subheading{===== Detailed comments for authors =====} \end{center} I found the paper easy to read, especially for relativel complex topic. Although I am not an expect on the implementation of cryptographic primitives, I found the mathematical explanation and verification in particular easy to follow. However, I found it very difficult to evaluate the scientific value of this paper. It gave me no new insights into proof methodology, the benefits or drawbacks of this particular approach, or the effort required. If the paper was proposing a new technique which could be applied more generally, attempted to show the same technique scaled to multiple X25519 implementations or otherwise compared different techniques for verification this would significantly improve it. \begin{center} \subheading{===== Requested changes =====} \end{center} \begin{itemize} \item Better clarify effort required for this undertaking. \item Describe challenges for proving statements about the more complex (faster) implementations. \item Describe which parts of the contributions could possibly be applied more generally. \end{itemize}