usenix-g.tex 2.61 KB
Newer Older
1
\newpage
2
\section*{Usenix Security 2020 Review \#324G}
3

4
\begin{tabular}{rrp{.6\textwidth}}
5
    \toprule
benoit's avatar
benoit committed
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                \\
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}
57

Peter Schwabe's avatar
Peter Schwabe committed
58
59
60
%\begin{answer}
%    \todo{Should add some reply here somewhere}
%\end{answer}
61