Commit aca27411 authored by Benoit Viguier's avatar Benoit Viguier
Browse files

more of Freek's comment

parent d4fa4057
...@@ -39,7 +39,7 @@ This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-A ...@@ -39,7 +39,7 @@ This part of the proof uses the Verifiable Software Toolchain (VST)~\cite{2012-A
to establish a link between C and Coq. to establish a link between C and Coq.
VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic} VST uses separation logic~\cite{1969-Hoare,Reynolds02separationlogic}
to show that the semantics of the program satisfy a functional specification in Coq. to show that the semantics of the program satisfy a functional specification in Coq.
To the best of our knowledge, this is the first time that VST To the best of our knowledge, this is the first time that the VST
is used in the formal proof of correctness of an implementation is used in the formal proof of correctness of an implementation
of an asymmetric cryptographic primitive. of an asymmetric cryptographic primitive.
...@@ -65,13 +65,13 @@ to strengthen our trust into cryptographic constructions and cryptographic softw ...@@ -65,13 +65,13 @@ to strengthen our trust into cryptographic constructions and cryptographic softw
has seen massive progress in the recent past. This progress, the state of the art, has seen massive progress in the recent past. This progress, the state of the art,
and future challenges have recently been compiled in a SoK paper by Barbosa, and future challenges have recently been compiled in a SoK paper by Barbosa,
Barthe, Bhargavan, Blanchet, Cremers, Liao, and Parno~\cite{BBB+19}. Barthe, Bhargavan, Blanchet, Cremers, Liao, and Parno~\cite{BBB+19}.
This SoK paper, in Section III.C, also gives an overview of verification efforts of This SoK paper, in Section III.C, also gives an overview of verification efforts of
X25519 software. What all the previous approaches have in common is that they X25519 software. What all the previous approaches have in common is that they
prove correctness by verifying that some low-level implementation matches a prove correctness by verifying that some low-level implementation matches a
higher-level specification. This specification is kept in terms of a sequence higher-level specification. This specification is kept in terms of a sequence
of finite-field operations, typically close to the pseudocode in RFC 7748. of finite-field operations, typically close to the pseudocode in RFC 7748.
There are two general approaches to establish this link There are two general approaches to establish this link
between low-level code and higher-level specification: between low-level code and higher-level specification:
Synthesize low-level code from the specification Synthesize low-level code from the specification
or write the low-level code by hand and prove that it or write the low-level code by hand and prove that it
...@@ -93,9 +93,9 @@ matches the specification. ...@@ -93,9 +93,9 @@ matches the specification.
All of these X25519 verification efforts listed in~\cite{BBB+19} use a clean-slate All of these X25519 verification efforts listed in~\cite{BBB+19} use a clean-slate
approach to obtain code and proofs. approach to obtain code and proofs.
Our effort targets existing software and we are aware of only one earlier Our effort targets existing software and we are aware of only one earlier
work in the context of X25519 following a similar approach. work in the context of X25519 following a similar approach.
In~\cite{Chen2014VerifyingCS}, Chen, Hsu, Lin, Schwabe, Tsai, Wang, Yang, and Yang present In~\cite{Chen2014VerifyingCS}, Chen, Hsu, Lin, Schwabe, Tsai, Wang, Yang, and Yang present
a mechanized proof of two assembly-level implementations of the core function of X25519. a mechanized proof of two assembly-level implementations of the core function of X25519.
The proof in~\cite{Chen2014VerifyingCS} takes a different approach from ours. The proof in~\cite{Chen2014VerifyingCS} takes a different approach from ours.
...@@ -105,8 +105,8 @@ not make the link to the mathematical definition from~\cite{Ber06}. ...@@ -105,8 +105,8 @@ not make the link to the mathematical definition from~\cite{Ber06}.
Finally, in terms of languages and tooling the work closest to what we present here Finally, in terms of languages and tooling the work closest to what we present here
is the proof of correctness of OpenSSL's is the proof of correctness of OpenSSL's
implementations of HMAC~\cite{Beringer2015VerifiedCA}, implementations of HMAC~\cite{Beringer2015VerifiedCA},
and mbedTLS' implementations of and mbedTLS' implementations of
HMAC-DRBG~\cite{2017-Ye} and SHA-256~\cite{2015-Appel}. HMAC-DRBG~\cite{2017-Ye} and SHA-256~\cite{2015-Appel}.
\subheading{Reproducing the proofs.} \subheading{Reproducing the proofs.}
...@@ -127,7 +127,7 @@ proof techniques used to show the correctness with respect to RFC~7748~\cite{rfc ...@@ -127,7 +127,7 @@ proof techniques used to show the correctness with respect to RFC~7748~\cite{rfc
and Strub and the correctness of X25519 implementation with respect to Bernstein's and Strub and the correctness of X25519 implementation with respect to Bernstein's
specifications~\cite{Ber14}. specifications~\cite{Ber14}.
Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs Finally in \sref{sec:Conclusion} we discuss the trusted code base of our proofs
and conclude with some lessons learned about TweetNaCl and with sketching the and conclude with some lessons learned about TweetNaCl and with sketching the
effort required to extend our work to other elliptic-curve software. effort required to extend our work to other elliptic-curve software.
\fref{tikz:ProofOverview} shows a graph of dependencies of the proofs. \fref{tikz:ProofOverview} shows a graph of dependencies of the proofs.
......
...@@ -32,7 +32,7 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{ ...@@ -32,7 +32,7 @@ We discuss the plot twist (\ref{subsec:Zmodp}) of Curve25519 and solve it (\ref{
\subsection{Formalization of elliptic Curves} \subsection{Formalization of elliptic Curves}
\label{subsec:ECC} \label{subsec:ECC}
\fref{tikz:ProofHighLevel1} presents an intuition of the proof of the ladder's \fref{tikz:ProofHighLevel1} presents the structure of the proof of the ladder's
correctness. correctness.
\begin{figure}[h] \begin{figure}[h]
\centering \centering
...@@ -149,7 +149,7 @@ Inductive mc : Type := MC p of oncurve p. ...@@ -149,7 +149,7 @@ Inductive mc : Type := MC p of oncurve p.
Lemma oncurve_mc: forall p : mc, oncurve p. Lemma oncurve_mc: forall p : mc, oncurve p.
\end{lstlisting} \end{lstlisting}
We define the addition on Montgomery curves in the similar way as in the Weierstra{\ss} form. We define the addition on Montgomery curves in a similar way as for the Weierstra{\ss} form.
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Definition add (p1 p2 : point K) := Definition add (p1 p2 : point K) :=
match p1, p2 with match p1, p2 with
...@@ -165,7 +165,7 @@ Definition add (p1 p2 : point K) := ...@@ -165,7 +165,7 @@ Definition add (p1 p2 : point K) :=
(| xs, - s * (xs - x1) - y1 |) (| xs, - s * (xs - x1) - y1 |)
end. end.
\end{lstlisting} \end{lstlisting}
And again we prove the result is on the curve (again with coercion): And again we prove the result is on the curve: % (again with coercion):
\begin{lstlisting}[language=Coq] \begin{lstlisting}[language=Coq]
Lemma addO (p q : mc) : oncurve (add p q). Lemma addO (p q : mc) : oncurve (add p q).
Definition addmc (p1 p2 : mc) : mc := Definition addmc (p1 p2 : mc) : mc :=
...@@ -239,7 +239,7 @@ We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve. ...@@ -239,7 +239,7 @@ We define $\chi$ and $\chi_0$ to return the \xcoord of points on a curve.
-- $\chi_0 : M_{a,b}(\K) \to \K$\\ -- $\chi_0 : M_{a,b}(\K) \to \K$\\
such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$. such that $\chi_0(\Oinf) = 0$ and $\chi_0((x,y)) = x$.
\end{dfn} \end{dfn}
Using projective coordinates we prove the formula for differential addition (\lref{lemma:xADD}). Using projective coordinates we prove the formula for differential addition.% (\lref{lemma:xADD}).
\begin{lemma} \begin{lemma}
\label{lemma:xADD} \label{lemma:xADD}
Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
...@@ -254,11 +254,10 @@ then for any point $P_1$ and $P_2$ in $M_{a,b}(\K)$ such that ...@@ -254,11 +254,10 @@ 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)$, $X_1/Z_1 = \chi(P_1), X_2/Z_2 = \chi(P_2)$, and $X_4/Z_4 = \chi(P_1 - P_2)$,
we have $X_3/Z_3 = \chi(P_1+P_2)$.\\ we have $X_3/Z_3 = \chi(P_1+P_2)$.\\
\textbf{Remark:} \textbf{Remark:}
%For any $x \in \K \backslash\{0\}, x/0$ should be understood as $\infty$.
These definitions should be understood in $\K \cup \{\infty\}$. These definitions should be understood in $\K \cup \{\infty\}$.
If $x\ne 0$ then we define $x/0 = \infty$. If $x\ne 0$ then we define $x/0 = \infty$.
\end{lemma} \end{lemma}
Similarly we also prove the formula for point doubling (\lref{lemma:xDBL}). Similarly we also prove the formula for point doubling.% (\lref{lemma:xDBL}).
\begin{lemma} \begin{lemma}
\label{lemma:xDBL} \label{lemma:xDBL}
Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and Let $M_{a,b}$ be a Montgomery curve such that $a^2-4$ is not a square in \K, and
...@@ -331,7 +330,7 @@ final proof of \coqe{Theorem RFC_Correct}. ...@@ -331,7 +330,7 @@ final proof of \coqe{Theorem RFC_Correct}.
\begin{figure}[h] \begin{figure}[h]
\centering \centering
\include{tikz/highlevel2} \include{tikz/highlevel2}
\caption{Instantiation and proof dependencies for the correctness of X25519} \caption{Proof dependencies for the correctness of X25519.}
\label{tikz:ProofHighLevel2} \label{tikz:ProofHighLevel2}
\end{figure} \end{figure}
...@@ -444,10 +443,8 @@ elements here. ...@@ -444,10 +443,8 @@ elements here.
For this reason we decided to formalize a definition of $\F{p^2}$ ourselves. For this reason we decided to formalize a definition of $\F{p^2}$ ourselves.
We can represent $\F{p^2}$ as the set $\F{p} \times \F{p}$, We can represent $\F{p^2}$ as the set $\F{p} \times \F{p}$,
%with $\delta = 2$, % in other words,
%we haven't introduced this delta? representing polynomials with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way
in other words,
the polynomial with coefficients in $\F{p}$ modulo $X^2 - 2$. In a similar way
as for $\F{p}$ we use a module in Coq. as for $\F{p}$ we use a module in Coq.
\begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip] \begin{lstlisting}[language=Coq,belowskip=-0.25 \baselineskip]
Module Zmodp2. Module Zmodp2.
...@@ -481,7 +478,7 @@ $\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse. ...@@ -481,7 +478,7 @@ $\F{p^2}\backslash\{0\}$, there exists a multiplicative inverse.
For all $x \in \F{p^2}\backslash\{0\}$ and $a,b \in \F{p}$ such that $x = (a,b)$, For all $x \in \F{p^2}\backslash\{0\}$ and $a,b \in \F{p}$ such that $x = (a,b)$,
$$x^{-1} = \Big(\frac{a}{a^2-2b^2}\ , \frac{-b}{a^2-2b^2}\Big)$$ $$x^{-1} = \Big(\frac{a}{a^2-2b^2}\ , \frac{-b}{a^2-2b^2}\Big)$$
\end{lemma} \end{lemma}
Similarly as in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}. As in $\F{p}$, we define $0^{-1} = 0$ and prove \lref{lemma:Zmodp2_field}.
\begin{lemma} \begin{lemma}
\label{lemma:Zmodp2_field} \label{lemma:Zmodp2_field}
$\F{p^2}$ is a commutative field. $\F{p^2}$ is a commutative field.
......
...@@ -6,7 +6,7 @@ chain of trust. ...@@ -6,7 +6,7 @@ chain of trust.
\subheading{Trusted Code Base of the proof.} \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 correct. One should not be able to prove a false statement in that system, \eg by
proving an inconsistency. proving an inconsistency.
In our case we rely on: In our case we rely on:
...@@ -26,7 +26,7 @@ Lemma f_ext: forall (A B:Type), ...@@ -26,7 +26,7 @@ Lemma f_ext: forall (A B:Type),
specification. specification.
\item \textbf{CompCert}. When compiling with CompCert we only need to trust \item \textbf{CompCert}. When compiling with CompCert we only need to trust
CompCert's {assembly} semantics, because it has been formally proven correct. CompCert's {assembly} semantics, as the compilation chain has been formally proven correct.
However, when compiling with other C compilers like Clang or GCC, we need to However, when compiling with other C compilers like Clang or GCC, we need to
trust that the CompCert's Clight semantics matches the C17 standard. trust that the CompCert's Clight semantics matches the C17 standard.
...@@ -71,7 +71,7 @@ o[i]&=0xffff; ...@@ -71,7 +71,7 @@ o[i]&=0xffff;
Aside from this modifications, all subsequent alterations to the TweetNaCl code% Aside from this modifications, all subsequent alterations to the TweetNaCl code%
---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})---% ---such as the type change of loop indexes (\TNaCle{int} instead of \TNaCle{i64})---%
were required for VST to parse the code properly. We believe that those were required for VST to step through the code properly. We believe that those
adjustments do not impact the trust of our proof. adjustments do not impact the trust of our proof.
We contacted the authors of TweetNaCl and expect that the changes described We contacted the authors of TweetNaCl and expect that the changes described
...@@ -89,12 +89,11 @@ the verification effort to Ed25519 would make directly use of the low-level ...@@ -89,12 +89,11 @@ 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 arithmetic. The ladder steps formula being different this would require a high
level verification similar to \tref{thm:montgomery-ladder-correct}. level verification similar to \tref{thm:montgomery-ladder-correct}.
The verification \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 require the adaptation of most of the low-level arithmetic (mainly the
multiplication, carry propagation and reduction). multiplication, carry propagation and reduction).
Once the correctness and bounds of the basic operations are established, Once the correctness and bounds of the basic operations are established,
reproving the full ladder would make use of our generic definition and lower reproving the full ladder would make use of our generic definition.
the workload.
\subheading{A complete proof.} \subheading{A complete proof.}
We provide a mechanized formal proof of the correctness of the X25519 We provide a mechanized formal proof of the correctness of the X25519
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment