### Various small edits for camera-ready version.

parent b62693bb
 ... ... @@ -5,7 +5,7 @@ Any formal system relies on a trusted base. In this section we describe our chain of trust. \subheading{Trusted Code Base of the proof.} Our proof relies on a trusted base, i.e. a foundation of definitions that must be Our proof relies on a trusted base, i.e., a foundation of definitions that must be correct. One should not be able to prove a false statement in that system, \eg by proving an inconsistency. ... ... @@ -13,8 +13,8 @@ In our case we rely on: \begin{itemize} \item \textbf{Calculus of Inductive Constructions}. The intuitionistic logic used by Coq must be consistent in order to trust the proofs. As an axiom, we assume that the functional extensionality is also consistent with that logic. $$\forall x, f(x) = g(x) \implies f = g$$ we assume that the functional extensionality is also consistent with that logic: $$\forall x, f(x) = g(x) \implies f = g.$$ % \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] % Lemma f_ext: forall (A B:Type), % forall (f g: A -> B), ... ... @@ -22,7 +22,7 @@ In our case we rely on: % \end{lstlisting} \item \textbf{Verifiable Software Toolchain}. This framework developed at Princeton allows a user to prove that a Clight code matches pure Coq Princeton allows a user to prove that a Clight code matches a pure Coq specification. \item \textbf{CompCert}. When compiling with CompCert we only need to trust ... ... @@ -48,7 +48,7 @@ o[i] = aux1 + aux2; \item Finally, we must trust the \textbf{Coq kernel} and its associated libraries; the \textbf{Ocaml compiler} on which we compiled Coq; the \textbf{Ocaml Runtime} and the \textbf{CPU}. Those are common to all proofs done with this architecture \cite{2015-Appel,coq-faq}. done with this architecture~\cite{2015-Appel,coq-faq}. \end{itemize} \subheading{Corrections in TweetNaCl.} ... ... @@ -70,7 +70,7 @@ and thus solved this problem. o[i]&=0xffff; \end{lstlisting} Aside from this modifications, all subsequent alterations to the TweetNaCl code% Aside from these modifications, all subsequent alterations to the TweetNaCl code% ---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})---% were required for VST to step through the code properly. We believe that those adjustments do not impact the trust of our proof. ... ... @@ -101,7 +101,7 @@ written in a not particularly verification-friendly language using a set of tools (VST and Coq) whose development we are not actively involved in. TweeNaCl comes with a claim of verifiability, but it became clear TweetNaCl comes with a claim of verifiability, but it became clear rather quickly that this claim is only based on the overall simplicity of the library and not supported by code written carefully such that it can efficiently be verified with existing tools. The difference between ... ... @@ -109,10 +109,10 @@ our verified version of TweetNaCl and the original TweetNaCl in Appendix~\ref{verified-C-and-diff} gives an idea of some minimal changes we had to apply to work with VST; many more small changes would have made the proof much easier and more elegant. As one example, in \TNaCle{pack25519} the substraction of $p$ and the carry example, in \TNaCle{pack25519} the subtraction of $p$ and the carry propagation are done in a single \TNaCle{for} loop; had they been splitted into two loops, the final result would have been the same with a verification effort significantly lessen. had they been split into two loops, the final result would have been the same but with a much smaller verification effort. There were many positive lessons to be learned from this verification effort; most importantly that it is possible to prove legacy'' cryptographic ... ... @@ -127,7 +127,7 @@ At least in the VST versions we worked with, this approach did not quite work and at various stages in the proofs we had to look into the underlying lemmas. This was due to the provided tactics not terminating, for example in the last few steps \coqe{pack25519}'s VST proof. for example in the last few steps of \coqe{pack25519}'s VST proof. Some struggle with VST also taught us another very pleasant lesson, namely that the VST development team is very responsive and helpful. Various of our issues were sorted out with their help and we hope ... ... @@ -135,19 +135,19 @@ that some of the experience we brought in also helped improve VST. \subheading{Extending our work.} The high-level definition (\sref{sec:maths}) can easily be ported to any other Montgomery curves and with it the proof of the ladder's correctness other Montgomery curve and with it the proof of the ladder's correctness assuming the same formulas are used. In addition to the curve equation, the field \F{p} would need to be redefined as $p=2^{255}-19$ is hard-coded in order to speed up some proofs. With respect to the C code verification (\sref{sec:C-Coq}), the extension of the verification effort to Ed25519 would make directly use of the low-level arithmetic. The ladder steps formula being different this would require a high the verification effort to Ed25519 would make direct use of the low-level arithmetic. As the ladder-steps formula is different, this would require a high level verification similar to \tref{thm:montgomery-ladder-correct}; also, a full correctness verification of Ed25519 signatures would require verifying correctness of SHA-512. The verification of \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would The verification of, \eg X448~\cite{cryptoeprint:2015:625,rfc7748} in C would require the adaptation of most of the low-level arithmetic (mainly the multiplication, carry propagation and reduction). Once the correctness and bounds of the basic operations are established, ... ... @@ -160,9 +160,9 @@ We first formalized X25519 from RFC~7748~\cite{rfc7748} in Coq. We then proved that TweetNaCl's implementation of X25519 matches our formalization. In a second step we extended the Coq library for elliptic curves \cite{BartziaS14} by Bartzia and Strub to support Montgomery curves. Using this extension we proved that the X25519 from the RFC matches the Using this extension we proved that the the X25519 specification from the RFC matches the mathematical definitions as given in~\cite[Sec.~2]{Ber06}. Therefore in addition to proving the mathematical correctness of TweetNaCl, we also increases the trust of other works such as \cite{zinzindohoue2017hacl,Erbsen2016SystematicSO} which rely on RFC~7748. \vspace{-0.3cm} \ No newline at end of file we also increase the trust of other works such as \cite{zinzindohoue2017hacl,Erbsen2016SystematicSO}, which rely on RFC~7748. \vspace{-0.3cm}
 ... ... @@ -42,7 +42,7 @@ the green tiles represent major lemmas and theorems. We consider the field $\K$ and formalize the Montgomery curves ($M_{a,b}(\K)$). Then, by using the equivalent Weierstra{\ss} form ($E_{a',b'}(\K)$) from the library of Bartzia and Strub, we prove that $M_{a,b}(\K)$ forms a commutative group. Under the hypothesis that Under the hypotheses that $a^2 - 4$ is not a square in $\K$, we prove the correctness of the ladder (\tref{thm:montgomery-ladder-correct}). \begin{figure}[h] ... ... @@ -60,8 +60,8 @@ We now turn our attention to the details of the proof of the ladder's correctnes Given a field $\K$, using an appropriate choice of coordinates, an elliptic curve $E$ is a plane cubic algebraic curve defined by an equation $E(x,y)$ of the form: $$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6$$ is a plane cubic algebraic curve defined by an equation $E(x,y)$ of the form $$E : y^2 + a_1 xy + a_3 y = x^3 + a_2 x^2 + a_4 x + a_6,$$ where the $a_i$'s are in \K\ and the curve has no singular point (\ie no cusps or self-intersections). The set of points defined over \K, written $E(\K)$, is formed by the solutions $(x,y)$ of $E$ together with a distinguished point $\Oinf$ called point at infinity: ... ... @@ -84,8 +84,8 @@ Then, this equation $E(x,y)$ can be reduced into its short Weierstra{\ss} form. In this setting, Bartzia and Strub defined the parametric type \texttt{ec} which represents the points on a specific curve. It is parameterized by a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neither 2 nor 3--- and \texttt{E : ecuType} ---a record that packs the curve parameters $a$ and $b$--- a \texttt{K : ecuFieldType}---the type of fields whose characteristic is neither 2 nor 3---% and \texttt{E : ecuType}---a record that packs the curve parameters $a$ and $b$---% along with the proof that $\Delta(a,b) \neq 0$. \begin{lstlisting}[language=Coq] Inductive point := EC_Inf | EC_In of K * K. ... ... @@ -102,7 +102,7 @@ Inductive ec : Type := EC p of oncurve p. Points on an elliptic curve form an abelian group when equipped with the following structure.% \begin{itemize} \item The negation of a point $P = (x,y)$ is defined by reflection over the $x$-axis, \ie $-P = (x, -y)$. \item The negation of a point $P = (x,y)$ is defined by reflection about the $x$-axis, \ie $-P = (x, -y)$. \item The addition of two points $P$ and $Q$ is defined as the negation of the third intersection point of the line passing through $P$ and $Q$, or tangent to $P$ if $P = Q$. \item $\Oinf$ is the neutral element under this law: if 3 points are collinear, their sum is equal to $\Oinf$. ... ... @@ -139,17 +139,19 @@ than the Weierstra{\ss} form. We consider the Montgomery form \cite{MontgomerySp \begin{dfn} Let $a \in \K \backslash \{-2, 2\}$, and $b \in \K \backslash \{ 0\}$. The \textit{elliptic curve} $M_{a,b}$ is defined by the equation: $$by^2 = x^3 + ax^2 + x,$$ $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying the $M_{a,b}$ along with an additional formal point $\Oinf$, at infinity''. The \textit{elliptic curve} $M_{a,b}$ is defined by the equation $$by^2 = x^3 + ax^2 + x.$$ $M_{a,b}(\K)$ is the set of all points $(x,y) \in \K^2$ satisfying $M_{a,b}$ along with an additional formal point $\Oinf$ at infinity''. \end{dfn} Similar to the definition of \texttt{ec}, we define the parametric type \texttt{mc} which represents the points on a specific Montgomery curve. It is parameterized by a \texttt{K : ecuFieldType} ---the type of fields whose characteristic is neither 2 nor 3--- and \texttt{M : mcuType} ---a record that packs the curve parameters $a$ and $b$ along with the proofs that $b \neq 0$ and $a^2 \neq 4$. a \texttt{K : ecuFieldType}---% the type of fields whose characteristic is neither 2 nor 3---% and \texttt{M : mcuType}---% a record that packs the curve parameters $a$ and $b$---% along with the proofs that $b \neq 0$ and $a^2 \neq 4$. \begin{lstlisting}[language=Coq,belowskip=-0.1 \baselineskip] Record mcuType := { cA : K; cB : K; _: cB != 0; _: cA^2 != 4}. Definition oncurve (p : point K) := ... ... @@ -176,7 +178,7 @@ Definition add (p1 p2 : point K) := (| xs, - s * (xs - x1) - y1 |) end. \end{lstlisting} And again we prove the result is on the curve: And again we prove that the result is on the curve: \begin{lstlisting}[language=Coq] Lemma addO (p q : mc) : oncurve (add p q). ... ... @@ -193,7 +195,7 @@ After having verified the group properties, it follows that the bijection is a g \label{lemma:bij-ecc} Let $M_{a,b}$ be a Montgomery curve, define \vspace{-0.3em} $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3}.$$ $$a' = \frac{3-a^2}{3b^2} \text{\ \ \ \ and\ \ \ \ } b' = \frac{2a^3 - 9a}{27b^3},$$ then $E_{a',b'}$ is a Weierstra{\ss} curve, and the mapping $\varphi : M_{a,b} \mapsto E_{a',b'}$ defined as: \vspace{-0.5em} ... ... @@ -222,7 +224,7 @@ After having verified the group properties, it follows that the bijection is a g \subsubsection{Projective coordinates} \label{subsec:ECC-projective} In a projective plane, points are represented by the triples $(X:Y:Z)$ excluding $(0:0:0)$. In a projective plane, points are represented by triples $(X:Y:Z)$ excluding $(0:0:0)$. Scalar multiples of triples are identified with each other, \ie for all $\lambda \neq 0$, the triples $(X:Y:Z)$ and $(\lambda X:\lambda Y:\lambda Z)$ represent the same point in the projective plane. ... ... @@ -269,8 +271,8 @@ Using projective coordinates we prove the formula for differential addition.% (\ Define \vspace{-0.5em} \begin{align*} X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2 \\[-0.5ex] Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2 X_3 & = Z_4((X_1 - Z_1)(X_2+Z_2) + (X_1+Z_1)(X_2-Z_2))^2, \\[-0.5ex] Z_3 & = X_4((X_1 - Z_1)(X_2+Z_2) - (X_1+Z_1)(X_2-Z_2))^2, \end{align*} then for any point $P_1$ and $P_2$ in $M_{a,b}(\K)$ such that $X_1/Z_1 = \chi(P_1), X_2/Z_2 = \chi(P_2)$, and $X_4/Z_4 = \chi(P_1 - P_2)$, ... ... @@ -359,7 +361,7 @@ The white tiles are definitions while green tiles are important lemmas and theor \end{figure} A brief overview of the complete proof is described below. We first pose $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equations $C = M_{a,b}$, and $T = M_{a,b'}$. We first set $a = 486662$, $b = 1$, $b' = 2$, $p = 2^{255}-19$, with the equations $C = M_{a,b}$, and $T = M_{a,b'}$. We prove the primality of $p$ and define the field $\F{p}$. Subsequently, we show that neither $2$ nor $a^2 - 2$ is a square in $\F{p}$. We consider $\F{p^2}$ and define $C(\F{p})$, $T(\F{p})$, and $C(\F{p^2})$. ... ... @@ -437,7 +439,7 @@ $M_{486662,2}(\F{p})$ are the same. % curve25519_Fp_ladder n x = twist25519_Fp_ladder n x. % \end{lstlisting} Because $2$ is not a square in $\F{p}$, it allows us to split $\F{p}$ into two sets. Because $2$ is not a square in $\F{p}$, we can partition $\F{p}$ as follows: \begin{lemma} \label{lemma:square-or-2square} For all $x$ in $\F{p}$, there exists a $y$ in $\F{p}$ such that ... ... @@ -528,9 +530,9 @@ The injection $a \mapsto (a,0)$ from $\F{p}$ to $\F{p^2}$ preserves $0, 1, +, -, \times$. Thus $(a,0)$ can be abbreviated as $a$ without confusion. We define $M_{486662,1}(\F{p^2})$. With the rewrite rule above, it is straightforward to prove that any point on the curve $M_{486662,1}(\F{p})$ is also on the curve $M_{486662,1}(\F{p^2})$. Similarly, any point on the quadratic twist $M_{486662,2}(\F{p})$ also corresponds to a point on the curve $M_{486662,1}(\F{p^2})$. to prove that any point in $M_{486662,1}(\F{p})$ is also in $M_{486662,1}(\F{p^2})$. Similarly, any point in $M_{486662,2}(\F{p})$ also corresponds to a point in $M_{486662,1}(\F{p^2})$. As direct consequence, using \lref{lemma:curve-or-twist}, we prove that for all $x \in \F{p}$, there exists a point $P \in \F{p^2}\times\F{p^2}$ on $M_{486662,1}(\F{p^2})$ such that $\chi_0(P) = (x,0) = x$. ... ... @@ -556,7 +558,7 @@ We now study the case of the scalar multiplication and show similar proofs. \begin{lemma} \label{lemma:proj} For all $n \in \N$, for all point $P\in\F{p}\times\F{p}$ on the curve For all $n \in \N$, for any point $P\in\F{p}\times\F{p}$ on $M_{486662,1}(\F{p})$ (respectively on the quadratic twist $M_{486662,2}(\F{p})$), we have \vspace{-0.3em} \begin{align*} ... ... @@ -602,5 +604,5 @@ in other words between \coqe{Zmodp} and \coqe{:GF}. This allows us to show that given a clamped value $n$ and normalized \xcoord of $P$, \coqe{RFC} gives the same results as $Curve25519\_Fp$. All put together, this finishes the proof of the mathematical correctness of X25519: the fact that the code in X25519, both in the RFC~7748 and in TweetNaCl versions, correctly computes multiplication in the elliptic curve. All put together, this finishes the proof of the mathematical correctness of X25519: the fact that the code in X25519, both in RFC~7748 and in the TweetNaCl implementation, correctly computes scalar multiplication in the elliptic curve.
 ... ... @@ -83,13 +83,13 @@ SEP (sh [{ v_q }] <<(uch32)-- mVI (RFC n p); Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665 \end{lstlisting} In this specification we state preconditions like: In this specification we state preconditions as follows: \begin{itemize} \item[] \VSTe{PRE}: \VSTe{_p OF (tptr tuchar)}\\ The function \TNaCle{crypto_scalarmult} takes as input three pointers to arrays of unsigned bytes (\VSTe{tptr tuchar}) \VSTe{_p}, \VSTe{_q} and \VSTe{_n}. \item[] \VSTe{LOCAL}: \VSTe{temp _p v_p}\\ Each pointer represent an address \VSTe{v_p}, Each pointer represents an address \VSTe{v_p}, \VSTe{v_q} and \VSTe{v_n}. \item[] \VSTe{SEP}: \VSTe{sh [{ v_p $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI p}\\ In the memory share \texttt{sh}, the address \VSTe{v_p} points ... ... @@ -106,7 +106,7 @@ In this specification we state preconditions like: complete representation of \TNaCle{u8}. \end{itemize} As postcondition we have conditions like: As postcondition we have conditions as follows: \begin{itemize} \item[] \VSTe{POST}: \VSTe{tint}\\ The function \TNaCle{crypto_scalarmult} returns an integer. ... ... @@ -169,7 +169,7 @@ Examples of such cases are illustrated in \fref{tikz:MemSame}. \end{figure} As a result, a function must either have multiple specifications or specify which aliasing case is being used. The first option would require us to do very similar proofs multiple times for a same function. The first option would require us to do very similar proofs multiple times for the same function. We chose the second approach: for functions with 3 arguments, named hereafter \texttt{o, a, b}, we define an additional parameter $k$ with values in $\{0,1,2,3\}$: \begin{itemize} ... ... @@ -247,11 +247,11 @@ This solution does not cover all the possible cases of aliasing over 3 pointers As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} (array of 16 \TNaCle{long long}) are represented in base $2^{16}$ and we use a direct mapping to represent that array as a list integers in Coq. However, in order to show the correctness of the basic operations, of integers in Coq. However, in order to show the correctness of the basic operations, we need to convert this number to an integer. We reuse the mapping $\text{\coqe{ZofList}} : \Z \rightarrow \texttt{list}~\Z \rightarrow \Z$ from \sref{sec:Coq-RFC} and define a notation where $n$ is $16$, placing us with a radix of $2^{16}$. and define a notation where $n$ is $16$, to fix a a radix of $2^{16}$. \begin{lstlisting}[language=Coq] Notation "Z16.lst A" := (ZofList 16 A). \end{lstlisting} ... ... @@ -266,9 +266,9 @@ Using these two definitions, we prove intermediate lemmas such as the correctnes multiplication \Coqe{Low.M} where \Coqe{Low.M} replicates the computations and steps done in C. \begin{lemma} \label{lemma:mult_correct} \Coqe{Low.M} correctly implements the multiplication over $\Zfield$. \Coqe{Low.M} correctly implements the multiplication in $\Zfield$. \end{lemma} And specified in Coq as follows: This is specified in Coq as follows: \begin{lstlisting}[language=Coq] Lemma mult_GF_Zlength : forall (a:list Z) (b:list Z), ... ... @@ -277,16 +277,16 @@ Lemma mult_GF_Zlength : (Z16.lst (Low.M a b)):GF = (Z16.lst a * Z16.lst b):GF. \end{lstlisting} However for our purpose, simple functional correctness is not enough. However, for our purpose, simple functional correctness is not enough. We also need to define the bounds under which the operation is correct, allowing us to chain them, guaranteeing us the absence of overflow. allowing us to chain them, guaranteeing the absence of overflows. \begin{lemma} \label{lemma:mult_bounded} if all the values of the input arrays are constrained between $-2^{26}$ and $2^{26}$, then the output of \coqe{Low.M} will be constrained between $-38$ and $2^{16} + 38$. \end{lemma} And seen in Coq as follows: This is seen in Coq as follows: \begin{lstlisting}[language=Coq] Lemma M_bound_Zlength : forall (a:list Z) (b:list Z), ... ... @@ -311,7 +311,7 @@ Lemma M_bound_Zlength : By using each function \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub}; \coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{Inv25519}; \coqe{car25519}; \coqe{montgomery_rec}, we defined \coqe{Crypto_Scalarmult} in Coq and with VST proved it matches the exact behavior of X25519 in TweetNaCl. proved that it matches the exact behavior of X25519 in TweetNaCl. \end{sloppypar} \begin{sloppypar} ... ... @@ -333,9 +333,9 @@ Lemma Crypto_Scalarmult_RFC_eq : Crypto_Scalarmult n p = RFC n p. \end{lstlisting} Using this equality, we can directly replace \coqe{Crypto_Scalarmult} in our Using this equality, we can direct replace \coqe{Crypto_Scalarmult} in our specification by \coqe{RFC}, proving that TweetNaCl's X25519 implementation respect RFC~7748. respects RFC~7748. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!