@@ -364,7 +364,7 @@ We first pose $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equati
We prove the primality of $p$ and define the field $\F{p}$.
Subsequently, we show that neither $2$ nor $a^2-2$ are square in $\F{p}$.
We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$.
We prove that for all $x \in\F{p}$ there exist a point of \xcoord$x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$.
We prove that for all $x \in\F{p}$ there exists a point of \xcoord$x$ either on $C(\F{p})$ or on the quadratic twist $T(\F{p})$.
We prove that all points in $M(\F{p})$ and $T(\F{p})$ can be projected in $M(\F{p^2})$ and derive that computations done in $M(\F{p})$ and $T(\F{p})$ yield to the same results if projected to $M(\F{p^2})$.
Using \tref{thm:montgomery-ladder-correct} we prove that the ladder is correct for $M(\F{p})$ and $T(\F{p})$; with the previous results, this results in the correctness of the ladder for $M(\F{p^2})$, in other words the correctness of X25519.
This paper describes a mechanized proof (within the Coq proof assistant) of the
correctness of the implementation of a cryptographic primitive (scalar
multiplication on Curve25519) against its mathematical specification. Since this
theorem relies on the semantics of CompCert-C, the source language of the
CompCert verified compiler, this result extends to the assembly code.
This achievement combines formal reasoning in programming language semantics and
separation logic on one hand and in algebra and arithmetic on the other hand.
This highlights the versatility of the proof assistants and that they are mature
enough to describe with advanced mathematics the behavior of an assembly program
dealing with bits and pointers.
In addition to this concrete result (one proof of one program), the paper makes
some contributions that could be used as basis for other works: formalization of
Montgomery curves in Coq, formal correctness proof of the Montgomery ladder.
Finally, formal verification of cryptographic implementations is an active research topic:
this result is therefore an interesting data point in the landscape of high-assurance cryptography.
Strengths
---------
- First mechanized proof of an implementation of scalar multiplication against its mathematical specification.
- Mechanized correctness proof of the Montgomery ladder
- Large case study of using VST for verifying real C code
Weaknesses
----------
- No quantification of the engineering effort.
Comments for author
-------------------
Please report about how big is the effort required to verify these hundred lines
of C. Is it “reasonable”? Would you recommend using VST for a similar
verification task? Or would it be more efficient to write/generate new code from
scratch (à la FiatCrypto, for instance)?
Could the mathematical proof of the Montgomery ladder be applied to other
implementations (e.g., FiatCrypto)?
Make it clear that since CompCert-C is not a portable language, the proof is
tied to a specific architecture (here 32-bit x86).
Section §II.A could be improved by adding more details (there is plenty of room
if you get rid of the big Coq listings at the beginning of §III): why do we care
about quadratic twists, what is the “u-coordinate” that the RFC refers to, what
is the purpose of the xDBL&ADD operation (or more generally give an intuition
about the working of ladder).
About the “memory aliasing” trick described in §IV.A, a few things are unclear
when reading the text: is the extra parameter “k” added in the C code? is the M
function incorrect in arbitrary aliasing configuration or just unnecessarily
hard to prove? Also, I would like to know if this is a general methodology or an
ad-hoc workaround.
About implementation security, the statement “working on the C language level
[…] is not helpful” is wrong. Verification of constant-time security can be done
at the C level (first reference below) and such a verification is meaningful as
the result can be propagated down to assembly level (second reference below).
- Sandrine Blazy, David Pichardie, and Alix Trieu. ‘Verifying Constant-time Implementations by Abstract Interpretation’. 1 Jan. 2019 : 137–163.
- Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, and Alix Trieu. 2019. Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4, POPL, Article 7 (January 2020), 30 pages. DOI:https://doi.org/10.1145/3371075
---
Recommendations about the Coq development, most important first:
1. Use released versions of CompCert and VST instead of customized versions of them.
Indeed, using custom versions of the major tools suggests that they may not be readily usable without patching them,
X25519 is a cryptographic key-exchange protocol, defined in RFC 7748. It performs operations on a particular elliptic curve,
called Curve25519. X25519 has been previously implemented in the C language as part of the TweetNaCl library.
This paper presents:
1) a revision of the TweetNaCl C program implementing X25519, suitable for conversion to the Clight language of the verified
compiler CompCert.
2) a formalization in Coq of the X25519 RFC.
3) a formalization in Coq of the elliptic curve, Curve25519, associated with the RFC.
4) a Hoare-style partial correctness specification in Coq using VST for Clight versions of 1) using the RFC formalization in 2).
5) a formal proof using VST in Coq that the specification in 4) is satisfied by the Clight version of 1).
6) a formal proof in Coq that the RFC formalization in 2) is consistent with the formalization of the curve in 3).
By leveraging the general VST and CompCert correctness proofs, this means that the authors have established a formal connection
between mathematical operations on the elliptic curve and the (functional) behavior of the machine code (assembly) produced by
CompCert when compiling the program given in 1). This significantly increases the trustworthiness of the (revised) TweetNaCl C
program, in particular of the binary obtained when the C code is compiled by CompCert.
Specifically, a user need in principle only read and understand the Coq specification of the elliptic curve and the contracts
for the C program functions to trust that the protocol is correctly implemented in a compiled program.
Strengths
---------
+ This work reduces the trusted computing base (TCB) significantly for the revised C implementation of X25519 from TweetNaCl,
and reduces it even more when it is compiled by CompCert. This is generally important for achieving wide and safe use of
cryptographic protocols.
+ The authors formalize in Coq the X25519 RFC, but also reduce the implementation correctness to statements about Coq encodings of
elliptic curves, which uses a previous independent Coq library on elliptic curves. This means that we do not simply have to rely on
the faithfulness of their RFC formalization to believe paper claims.
+ I have been able to independently check their artifact with Coq and do some sampling to validate absence of unmentioned axioms in
formal proofs and the meaningfulness of the Coq specifications.
Weaknesses
----------
- The paper is highly disorganized and switches frequently between abstraction levels (Coq vs. mathematics/crypto vs. C), which will likely make it nearly unreadable to those unfamiliar with Coq and VST.
- The title and abstract is misleading in that only functional partial correctness is proven for the X25519 implementation.
In particular, the formal proofs do not establish any non-functional properties or termination.
- The authors do no accurately describe what their TCB actually is. The VST framework is in principle not part the TCB when properly
used - it simply provides a convenient way of expressing properties about the assembly code produced by CompCert. Moreover, they do not
mention that the unverified extraction mechanism of Coq is part of the TCB when compiling with CompCert.
Comments for author
-------------------
Some more detailed points about the disorganization of the paper:
- There is no clear statement of the contribution, akin to the bullet summary in this review.
- Section V is a mess of different notations talking both about abstract mathematics, Coq, and C.
- The TCB is only mentioned in the "Conclusion".
- The related work is only discussed at a very superficial level in the introduction section, when very little has been explained
about what the work is about.
VST provides a framework for reasoning about partial functional correctness of Clight programs. This means that the Hoare-style
specifications do not cover termination or non-functional correctness properties. I find that this is not clear from the paper.
To me, using "correctness" without qualification when one means "functional correctness only" is inaccurate.
The subsection about "Improving verification speed" essentially contributes nothing and should be removed.
Verification in Coq of the correctness of the TweetNaCl implementation of an elliptic curve key-exchange with respect to the RFC and the actual mathematical definition.
