lowlevel.tex 26.4 KB
Newer Older
 Peter Schwabe committed Jun 20, 2019 1 \section{Proving equivalence of X25519 in C and Coq}  Benoit Viguier committed Aug 12, 2019 2 \label{sec:C-Coq-RFC}  Benoit Viguier committed Aug 01, 2019 3   Benoit Viguier committed Aug 12, 2019 4 In this section we prove the following theorems:  Benoit Viguier committed Aug 01, 2019 5 \begin{theorem}  Benoit Viguier committed Aug 12, 2019 6 \label{thm:VST}  Benoit Viguier committed Aug 16, 2019 7 The implementation of X25519 in TweetNaCl (\TNaCle{crypto_scalarmult}) matches our  Benoit Viguier committed Aug 06, 2019 8 functional specification in Coq.  Benoit Viguier committed Aug 01, 2019 9 10 \end{theorem}  Benoit Viguier committed Aug 12, 2019 11 12 13 14 \begin{theorem} \label{thm:RFC} Our functional specification in Coq matches the specifications of RFC~7748~\cite{rfc7748}. \end{theorem}  Benoit Viguier committed Jun 21, 2019 15   Benoit Viguier committed Aug 12, 2019 16 We first describe the global structure of our proof (\ref{subsec:proof-structure}).  Benoit Viguier committed Aug 14, 2019 17 Then we introduce our specification, we specify the Hoare triple and prove it  Benoit Viguier committed Aug 12, 2019 18 19 correct with VST (\tref{thm:VST}). Then we discuss techniques used to prove equivalence of operations between  Benoit Viguier committed Aug 14, 2019 20 21 different number representations, proving the equivalence with the RFC (\tref{thm:RFC}).  Benoit Viguier committed Jul 10, 2019 22   Benoit Viguier committed Aug 13, 2019 23 24 25 26   Benoit Viguier committed Aug 12, 2019 27 28 29 30 31 32 33 34 35 36 37 \subsection{Structure of our proof} \label{subsec:proof-structure} In order to prove the correctness of X25519 in TweetNaCl code \TNaCle{crypto_scalarmult}, we use VST to prove that the code matches our functional Coq specification of \Coqe{Crypto_Scalarmult} (sometimes abbreviated as \Coqe{CSM}). Then, we prove that our specification of the scalar multiplication matches the mathematical definition of elliptic curves and Theorem 2.1 by Bernstein~\cite{Ber06} (\tref{thm:Elliptic-CSM}). \fref{tikz:ProofOverview} shows a graph of dependencies of the proofs considered. The mathematical proof of our specification is presented in \sref{sec:maths}.  Benoit Viguier committed Jul 12, 2019 38 \begin{figure}[h]  Benoit Viguier committed Jul 16, 2019 39  \centering  Benoit Viguier committed Jul 12, 2019 40  \include{tikz/proof}  Benoit Viguier committed Jul 16, 2019 41  \caption{Overview of the proof}  Benoit Viguier committed Aug 12, 2019 42  \label{tikz:ProofOverview}  Benoit Viguier committed Jul 12, 2019 43 \end{figure}  Benoit Viguier committed Jul 10, 2019 44   Benoit Viguier committed Aug 16, 2019 45 Verifying \TNaCle{crypto_scalarmult} also implies verifying all the functions  Benoit Viguier committed Aug 06, 2019 46 47 48 subsequently called: \TNaCle{unpack25519}; \TNaCle{A}; \TNaCle{Z}; \TNaCle{M}; \TNaCle{S}; \TNaCle{car25519}; \TNaCle{inv25519}; \TNaCle{set25519}; \TNaCle{sel25519}; \TNaCle{pack25519}.  Benoit Viguier committed Jul 10, 2019 49   Benoit Viguier committed Aug 06, 2019 50 We prove the implementation of X25519 is \textbf{sound}, \ie:  Benoit Viguier committed Jul 10, 2019 51 52 53 54 55 56 \begin{itemize} \item absence of access out-of-bounds of arrays (memory safety). \item absence of overflows/underflow on the arithmetic. \end{itemize} We also prove that TweetNaCl's code is \textbf{correct}: \begin{itemize}  Benoit Viguier committed Aug 12, 2019 57 \item X25519 is correctly implemented (we get what we expect) .  Benoit Viguier committed Jul 10, 2019 58 59 \item Operations on \texttt{gf} (\texttt{A}, \texttt{Z}, \texttt{M}, \texttt{S}) are equivalent to operations ($+,-,\times,x^2$) in \Zfield.  Benoit Viguier committed Jul 22, 2019 60 61 \item The Montgomery ladder computes a scalar multiplication between a natural number and a point.  Benoit Viguier committed Jul 10, 2019 62 63 \end{itemize}  Benoit Viguier committed Aug 01, 2019 64 In order to prove the soundness and correctness of \TNaCle{crypto_scalarmult},  Benoit Viguier committed Jul 10, 2019 65 we first create a skeleton of the Montgomery ladder with abstract operations which  Benoit Viguier committed Jul 22, 2019 66 67 can be instantiated over lists, integers, field elements... A high level specification (over a generic field $\K$) allows us to prove the  Benoit Viguier committed Jul 10, 2019 68 correctness of the ladder with respect to the curves theory.  Benoit Viguier committed Jul 22, 2019 69 70 71 72 This high-level specification does not rely on the parameters of Curve25519. By instantiating $\K$ with $\Zfield$, and the parameters of Curve25519 ($a = 486662, b = 1$), we define a mid-level specification. Additionally we also provide a low-level specification close to the \texttt{C} code  Benoit Viguier committed Jul 10, 2019 73 74 75 76 (over lists of $\Z$). We show this specification to be equivalent to the \textit{semantic version} of C (\texttt{CLight}) with VST. This low level specification gives us the soundness assurance. By showing that operations over instances ($\K = \Zfield$, $\Z$, list of $\Z$) are  Benoit Viguier committed Jul 22, 2019 77 equivalent, we bridge the gap between the low level and the high level specification  Benoit Viguier committed Jul 10, 2019 78 with Curve25519 parameters.  Benoit Viguier committed Aug 12, 2019 79 As such, we prove all specifications to equivalent (\fref{tikz:ProofStructure}).  Benoit Viguier committed Aug 01, 2019 80 This guarantees us the correctness of the implementation.  Benoit Viguier committed Jul 10, 2019 81 82  \begin{figure}[h]  Benoit Viguier committed Aug 12, 2019 83  \centering  Benoit Viguier committed Jul 10, 2019 84 85  \include{tikz/specifications} \caption{Structural construction of the proof}  Benoit Viguier committed Aug 12, 2019 86  \label{tikz:ProofStructure}  Benoit Viguier committed Jul 10, 2019 87 88 \end{figure}  Benoit Viguier committed Aug 13, 2019 89 90 91 92 93  \subsection{A Correct Specification}  Benoit Viguier committed Jul 03, 2019 94   Benoit Viguier committed Aug 12, 2019 95 TweetNaCl implements X25519 with numbers represented as arrays.  Benoit Viguier committed Aug 13, 2019 96 RFC~7748 defines X25519 over field elements. In order to simplify our proofs,  Benoit Viguier committed Aug 14, 2019 97 we define operations used in the ladder over generic types  Benoit Viguier committed Aug 16, 2019 98 \coqe{T} and \coqe{T'}. Those types are later instantiated as natural numbers,  Benoit Viguier committed Aug 13, 2019 99 100 101 102 103 104 105 integers, field elements, list of integers... The generic definition of the ladder (\coqe{montgomery_rec}) and its match with the definition of RFC~7748 are provided in Appendix~\ref{subsubsec:coq-ladder}. It has to be noted that the RFC uses an additional variable to optimize the number of \texttt{CSWAP}: \emph{Note that these formulas are slightly different from Montgomery's original paper. Implementations are free to use any correct formulas.''}~\cite{rfc7748}.  Benoit Viguier committed Aug 16, 2019 106 We later prove our ladder correct in that respect (\sref{sec:maths}).  Benoit Viguier committed Aug 12, 2019 107   Benoit Viguier committed Aug 14, 2019 108 \coqe{montgomery_rec} only computes the ladder steps.  Benoit Viguier committed Aug 16, 2019 109 110 While the inversion, the packing, the unpacking (setting bit 255 to \texttt{0}) and the clamping are not defined in a generic manner, we show their equivalence  Benoit Viguier committed Aug 14, 2019 111 between the different representations.  Benoit Viguier committed Aug 12, 2019 112   Benoit Viguier committed Aug 16, 2019 113 114 Appendix~\ref{subsubsec:ZCryptoScalarmult} shows the instantiation of our ladder over Integers (type \coqe{Z}). We call it \coqe{ZCrypto_Scalarmult}.  Benoit Viguier committed Aug 14, 2019 115 116 117 The modulo reduction is applied in \coqe{ZPack25519} translating every underlying operations as over \Zfield. As a result this specification can be interpreted as the formalization of X25519 in RFC~7748.  Benoit Viguier committed Aug 06, 2019 118   Benoit Viguier committed Aug 14, 2019 119 120 121 122 123 In appendix~\ref{subsubsec:CryptoScalarmult}, we show the the formalization of \TNaCle{crypto_scalarmult} over lists of integers. We define it as \Coqe{Crypto_Scalarmult} or \Coqe{CSM}. For the sake of space and simplicity we do not display the definitions of each underlying functions. The location of the definitions are listed in Appendix~\ref{appendix:proof-files}.  Benoit Viguier committed Aug 12, 2019 124 125 126 127  \subsection{With the Verifiable Software Toolchain} \label{subsec:with-VST}  Benoit Viguier committed Aug 14, 2019 128 We now turn our focus to the specification of the Hoare triple with our  Benoit Viguier committed Aug 16, 2019 129 specifications of \TNaCle{crypto_scalarmult} over lists of integers and proving  Benoit Viguier committed Aug 14, 2019 130 131 its correctness.  Benoit Viguier committed Aug 13, 2019 132 \subheading{Specifications.}  Benoit Viguier committed Aug 14, 2019 133 134 135 136 137 138 139 We show the soundness of TweetNaCl by proving the following specification matches a pure Coq function. % why "pure" ? % A pure function is a function where the return value is only determined by its % input values, without observable side effects (Side effect are e.g. printing) This defines the equivalence between the Clight representation and our Coq definition of the ladder (\coqe{CSM}).  Benoit Viguier committed Jul 03, 2019 140   Benoit Viguier committed Aug 12, 2019 141 \begin{lstlisting}[language=CoqVST]  Benoit Viguier committed Jul 03, 2019 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 Definition crypto_scalarmult_spec := DECLARE _crypto_scalarmult_curve25519_tweet WITH v_q: val, v_n: val, v_p: val, c121665:val, sh : share, q : list val, n : list Z, p : list Z (*------------------------------------------*) PRE [ _q OF (tptr tuchar), _n OF (tptr tuchar), _p OF (tptr tuchar) ] PROP (writable_share sh; Forall (fun x => 0 <= x < 2^8) p; Forall (fun x => 0 <= x < 2^8) n; Zlength q = 32; Zlength n = 32; Zlength p = 32) LOCAL(temp _q v_q; temp _n v_n; temp _p v_p; gvar __121665 c121665) SEP (sh [{ v_q }] <<(uch32)-- q; sh [{ v_n }] <<(uch32)-- mVI n; sh [{ v_p }] <<(uch32)-- mVI p; Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665) (*------------------------------------------*) POST [ tint ] PROP (Forall (fun x => 0 <= x < 2^8) (CSM n p); Zlength (CSM n p) = 32) LOCAL(temp ret_temp (Vint Int.zero)) SEP (sh [{ v_q }] <<(uch32)-- mVI (CSM n p); sh [{ v_n }] <<(uch32)-- mVI n; sh [{ v_p }] <<(uch32)-- mVI p; Ews [{ c121665 }] <<(lg16)-- mVI64 c_121665  Benoit Viguier committed Aug 12, 2019 172 \end{lstlisting}  Benoit Viguier committed Jul 03, 2019 173 174 175 176  In this specification we state as preconditions: \begin{itemize} \item[] \VSTe{PRE}: \VSTe{_p OF (tptr tuchar)}\\  Benoit Viguier committed Aug 06, 2019 177  The function \TNaCle{crypto_scalarmult} takes as input three pointers to  Benoit Viguier committed Jul 03, 2019 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196  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}, \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 to a list of integer values \VSTe{mVI p}. \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) p}\\ In order to consider all the possible inputs, we assumed each elements of the list \texttt{p} to be bounded by $0$ included and $2^8$ excluded. \item[] \VSTe{PROP}: \VSTe{Zlength p = 32}\\ We also assumed that the length of the list \texttt{p} is 32. This defines the complete representation of \TNaCle{u8[32]}. \end{itemize} As Post-condition we have: \begin{itemize} \item[] \VSTe{POST}: \VSTe{tint}\\  Benoit Viguier committed Aug 06, 2019 197  The function \TNaCle{crypto_scalarmult} returns an integer.  Benoit Viguier committed Jul 03, 2019 198 199 200 201 202 203 204 205 206 207 208  \item[] \VSTe{LOCAL}: \VSTe{temp ret_temp (Vint Int.zero)}\\ The returned integer has value $0$. \item[] \VSTe{SEP}: \VSTe{sh [{ v_q $\!\!\}\!\!]\!\!\!$ <<(uch32)-- mVI (CSM n p)}\\ In the memory share \texttt{sh}, the address \VSTe{v_q} points to a list of integer values \VSTe{mVI (CSM n p)} where \VSTe{CSM n p} is the result of the \VSTe{crypto_scalarmult} over \VSTe{n} and \VSTe{p}. \item[] \VSTe{PROP}: \VSTe{Forall (fun x => 0 <= x < 2^8) (CSM n p)}\\ \VSTe{PROP}: \VSTe{Zlength (CSM n p) = 32}\\ We show that the computation for \VSTe{CSM} fits in \TNaCle{u8[32]}. \end{itemize}  Benoit Viguier committed Aug 06, 2019 209 This specification shows that \TNaCle{crypto_scalarmult} in C computes the same  Benoit Viguier committed Jul 03, 2019 210 result as \VSTe{CSM} in Coq provided that inputs are within their respective  Benoit Viguier committed Aug 12, 2019 211 bounds: arrays of 32 bytes.  Benoit Viguier committed Aug 14, 2019 212 The location of the proof of this Hoare triple can be found in Appendix~\ref{appendix:proof-files}.  Benoit Viguier committed Aug 06, 2019 213   Benoit Viguier committed Aug 14, 2019 214 % We now bring the attention of the reader to details of verifications using the VST.  Benoit Viguier committed Aug 12, 2019 215   Benoit Viguier committed Aug 14, 2019 216 217 218 219 220 221 222 223 224 225 %% BLABLA about VST. Does not belong here. % The Verifiable Software Toolchain uses a strongest postcondition strategy. % The user must first write a formal specification of the function he wants to verify in Coq. % This should be as close as possible to the C implementation behavior. % This will simplify the proof and help with stepping through the CLight version of the software. % With the range of inputs defined, VST mechanically steps through each instruction % and ask the user to verify auxiliary goals such as array bound access, or absence of overflows/underflows. % We call this specification a low level specification. A user will then have an easier % time to prove that his low level specification matches a simpler higher level one.  Benoit Viguier committed Aug 12, 2019 226   Benoit Viguier committed Aug 14, 2019 227 228 229 230 231 232 233 234 % In order to further speed-up the verification process, it has to be know that to % prove the specification \TNaCle{crypto_scalarmult}, a user only need the specification of e.g. \TNaCle{M}. % This provide with multiple advantages: the verification by the Coq kernel can be done % in parallel and multiple users can work on proving different functions at the same time. % For the sake of completeness we proved all intermediate functions. \subheading{Memory aliasing.} In the VST, a simple specification of \texttt{M(o,a,b)} will assume three  Benoit Viguier committed Aug 16, 2019 235 distinct memory share. When called with three memory shares (\texttt{o, a, b}),  Benoit Viguier committed Aug 14, 2019 236 237 238 the three of them will be consumed. However assuming this naive specification when \texttt{M(o,a,a)} is called (squaring), the first two memory shares (\texttt{o, a}) are consumed and VST will expect a third memory share (\texttt{a}) which does not \textit{exist} anymore.  Benoit Viguier committed Aug 13, 2019 239 Examples of such cases are illustrated in \fref{tikz:MemSame}.  Benoit Viguier committed Aug 12, 2019 240 241 242 243 244 245 246 \begin{figure}[h] \centering \include{tikz/memory_same_sh} \caption{Aliasing and Separation Logic} \label{tikz:MemSame} \end{figure}  Benoit Viguier committed Aug 14, 2019 247 248 249 250 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. We chose the second approach: for functions with 3 arguments, named hereafter \texttt{o, a, b},  Benoit Viguier committed Aug 13, 2019 251 we define an additional parameter $k$ with values in $\{0,1,2,3\}$:  Benoit Viguier committed Aug 12, 2019 252 253 254 255 256 257 \begin{itemize} \item if $k=0$ then \texttt{o} and \texttt{a} are aliased. \item if $k=1$ then \texttt{o} and \texttt{b} are aliased. \item if $k=2$ then \texttt{a} and \texttt{b} are aliased. \item else there is no aliasing. \end{itemize}  Benoit Viguier committed Aug 14, 2019 258 259 260 In the proof of our specification, we do a case analysis over $k$ when needed. This solution does not cover all cases (e.g. all arguments are aliased) but it is enough for our needs.  Benoit Viguier committed Aug 12, 2019 261   Benoit Viguier committed Aug 13, 2019 262 \subheading{Verifying \texttt{for} loops.}  Benoit Viguier committed Aug 12, 2019 263 Final state of \texttt{for} loops are usually computed by simple recursive functions.  Benoit Viguier committed Aug 13, 2019 264 However we must define invariants which are true for each iteration step.  Benoit Viguier committed Aug 12, 2019 265 266  Assume we want to prove a decreasing loop where indexes go from 3 to 0.  Benoit Viguier committed Aug 13, 2019 267 Define a function $g : \N \rightarrow State \rightarrow State$ which takes as  Benoit Viguier committed Aug 16, 2019 268 269 input an integer for the index and a state, then returns a state. It simulates the body of the \texttt{for} loop.  Benoit Viguier committed Aug 13, 2019 270 Assume its recursive call: $f : \N \rightarrow State \rightarrow State$ which  Benoit Viguier committed Aug 16, 2019 271 iteratively applies $g$ with decreasing index:  Benoit Viguier committed Aug 12, 2019 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 \begin{equation*} f ( i , s ) = \begin{cases} s & \text{if } s = 0 \\ f( i - 1 , g ( i - 1 , s )) & \text{otherwise} \end{cases} \end{equation*} Then we have : \begin{align*} f(4,s) &= g(0,g(1,g(2,g(3,s)))) % \\ % f(3,s) &= g(0,g(1,g(2,s))) \end{align*} To prove the correctness of $f(4,s)$, we need to prove that intermediate steps $g(3,s)$; $g(2,g(3,s))$; $g(1,g(2,g(3,s)))$; $g(0,g(1,g(2,g(3,s))))$ are correct.  Benoit Viguier committed Aug 13, 2019 287 288 289 290 Due to the computation order of recursive function, our loop invariant for $i\in\{0;1;2;3;4\}$ cannot use $f(i)$. To solve this, we define an auxiliary function with an accumulator such that given $i\in\{0;1;2;3;4\}$, it will compute the first $i$ steps of the loop.  Benoit Viguier committed Aug 12, 2019 291   Benoit Viguier committed Aug 13, 2019 292 293 294 We then prove for the complete number of steps, the function with the accumulator and without returns the same result. We formalized this result in a generic way in Appendix~\ref{subsubsec:for}.  Benoit Viguier committed Aug 12, 2019 295 296  Using this formalization, we prove that the 255 steps of the Montgomery ladder  Benoit Viguier committed Aug 14, 2019 297 in C provide the same computations as in \coqe{CSM}.  Benoit Viguier committed Aug 12, 2019 298   Benoit Viguier committed Aug 17, 2019 299 300 301   Benoit Viguier committed Aug 12, 2019 302 303 \subsection{Number Representation and C Implementation}  Benoit Viguier committed Aug 13, 2019 304 As described in \sref{subsec:Number-TweetNaCl}, numbers in \TNaCle{gf} are represented  Benoit Viguier committed Jun 21, 2019 305 306 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,  Benoit Viguier committed Aug 16, 2019 307 we need to convert this number to a full integer.  Benoit Viguier committed Aug 14, 2019 308 309 310 311 312 \begin{dfn} Let \Coqe{ZofList} : $\Z \rightarrow \texttt{list} \Z \rightarrow \Z$, a parameterized map by $n$ between a list $l$ and its little endian representation with a radix $2^n$. \end{dfn}  Benoit Viguier committed Jun 21, 2019 313 314 315 316 317 318 319 320 321 322 323 324 We define it in Coq as: \begin{lstlisting}[language=Coq] Fixpoint ZofList {n:Z} (a:list Z) : Z := match a with | [] => 0 | h :: q => h + (pow 2 n) * ZofList q end. \end{lstlisting} We define a notation where $n$ is $16$. \begin{lstlisting}[language=Coq] Notation "Z16.lst A" := (ZofList 16 A). \end{lstlisting}  Benoit Viguier committed Aug 14, 2019 325 To facilitate working in \Zfield, we define the \coqe{:GF} notation.  Benoit Viguier committed Jun 21, 2019 326 327 328 \begin{lstlisting}[language=Coq] Notation "A :GF" := (A mod (2^255-19)). \end{lstlisting}  Benoit Viguier committed Aug 14, 2019 329 330 Later in \sref{sec:maths}, we formally define \F{\p}. Equivalence between operations under \coqe{:GF} and in \F{\p} are easily proven.  Benoit Viguier committed Jun 21, 2019 331 332  Using these two definitions, we proved intermediates lemmas such as the correctness of the  Benoit Viguier committed Aug 14, 2019 333 multiplication \Coqe{Low.MM} where \Coqe{Low.M} replicate the computations and steps done in C.  Benoit Viguier committed Jun 21, 2019 334 \begin{lemma}  Benoit Viguier committed Aug 14, 2019 335 336  \label{lemma:mult_correct} \Coqe{Low.M} implements correctly the multiplication over \Zfield.  Benoit Viguier committed Jun 21, 2019 337 338 \end{lemma} And seen in Coq as follows:  Benoit Viguier committed Aug 14, 2019 339 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 340 341 342 343 Lemma mult_GF_Zlength : forall (a:list Z) (b:list Z), Zlength a = 16 -> Zlength b = 16 ->  Benoit Viguier committed Aug 14, 2019 344  (Z16.lst (Low.M a b)) :GF =  Benoit Viguier committed Jun 21, 2019 345  (Z16.lst a * Z16.lst b) :GF.  Benoit Viguier committed Aug 14, 2019 346 347 348 349 \end{lstlisting} However for our purpose, simple functional correctness is not enough. We also need to define the bounds under which the operation is correct,  Benoit Viguier committed Aug 16, 2019 350 allowing us to chain them, guaranteeing us the absence of overflow.  Benoit Viguier committed Aug 14, 2019 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366  \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: \begin{lstlisting}[language=Coq] Lemma M_bound_Zlength : forall (a:list Z) (b:list Z), Zlength a = 16 -> Zlength b = 16 -> Forall (fun x => -2^26 < x < 2^26) a -> Forall (fun x => -2^26 < x < 2^26) b -> Forall (fun x => -38 <= x < 2^16 + 38) (Low.M a b). \end{lstlisting}  Benoit Viguier committed Jun 21, 2019 367   Benoit Viguier committed Aug 17, 2019 368 369 370   Benoit Viguier committed Aug 13, 2019 371 \subsection{Inversions, Reflections and Packing}  Benoit Viguier committed Jun 21, 2019 372   Benoit Viguier committed Aug 14, 2019 373 We now turn our attention to the inversion in \Zfield and techniques to  Benoit Viguier committed Aug 16, 2019 374 increase the verification speed of complex formulas.  Benoit Viguier committed Aug 14, 2019 375   Benoit Viguier committed Aug 13, 2019 376 \subheading{Inversions in \Zfield.}  Benoit Viguier committed Jul 10, 2019 377 We define a Coq version of the inversion mimicking  Benoit Viguier committed Aug 06, 2019 378 the behavior of \TNaCle{inv25519} (see below) over \Coqe{list Z}.  Benoit Viguier committed Jun 21, 2019 379 \begin{lstlisting}[language=Ctweetnacl]  Benoit Viguier committed Aug 14, 2019 380 sv inv25519(gf o,const gf i)  Benoit Viguier committed Jun 21, 2019 381 382 { gf c;  Benoit Viguier committed Aug 14, 2019 383 384 385  int a; set25519(c,i); for(a=253;a>=0;a--) {  Benoit Viguier committed Jun 21, 2019 386  S(c,c);  Benoit Viguier committed Aug 14, 2019 387  if(a!=2&&a!=4) M(c,c,i);  Benoit Viguier committed Jun 21, 2019 388  }  Benoit Viguier committed Aug 14, 2019 389  FOR(a,16) o[a]=c[a];  Benoit Viguier committed Jun 21, 2019 390 391 } \end{lstlisting}  Benoit Viguier committed Aug 14, 2019 392 393 We specify this with 2 functions: a recursive \Coqe{pow_fn_rev} to simulate the \texttt{for} loop and a simple \Coqe{step_pow} containing the body.  Benoit Viguier committed Jun 21, 2019 394 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Aug 14, 2019 395 396 Definition step_pow (a:Z) (c:list Z) (g:list Z) : list Z :=  Benoit Viguier committed Jun 21, 2019 397  let c := Sq c in  Benoit Viguier committed Aug 06, 2019 398  if a <>? 2 && a <>? 4  Benoit Viguier committed Jun 21, 2019 399 400 401  then M c g else c.  Benoit Viguier committed Aug 14, 2019 402 403 Function pow_fn_rev (a:Z) (b:Z) (c: list Z) (g: list Z)  Benoit Viguier committed Jun 21, 2019 404 405 406 407 408  {measure Z.to_nat a} : (list Z) := if a <=? 0 then c else let prev := pow_fn_rev (a - 1) b c g in  Benoit Viguier committed Aug 06, 2019 409  step_pow (b - a) prev g.  Benoit Viguier committed Jun 21, 2019 410 411 \end{lstlisting} This \Coqe{Function} requires a proof of termination. It is done by proving the  Benoit Viguier committed Aug 01, 2019 412 well-foundedness of the decreasing argument: \Coqe{measure Z.to_nat a}. Calling  Benoit Viguier committed Jun 21, 2019 413 414 415 416 417 \Coqe{pow_fn_rev} 254 times allows us to reproduce the same behavior as the \texttt{Clight} definition. \begin{lstlisting}[language=Coq] Definition Inv25519 (x:list Z) : list Z := pow_fn_rev 254 254 x x. \end{lstlisting}  Benoit Viguier committed Aug 01, 2019 418 Similarly we define the same function over $\Z$.  Benoit Viguier committed Jun 21, 2019 419 420 421 \begin{lstlisting}[language=Coq] Definition step_pow_Z (a:Z) (c:Z) (g:Z) : Z := let c := c * c in  Benoit Viguier committed Aug 06, 2019 422  if a <>? 2 && a <>? 4  Benoit Viguier committed Jun 21, 2019 423 424 425 426 427 428 429 430 431  then c * g else c. Function pow_fn_rev_Z (a:Z) (b:Z) (c:Z) (g: Z) {measure Z.to_nat a} : Z := if (a <=? 0) then c else let prev := pow_fn_rev_Z (a - 1) b c g in  Benoit Viguier committed Aug 06, 2019 432  step_pow_Z (b - a) prev g.  Benoit Viguier committed Jun 21, 2019 433 434 435 436  Definition Inv25519_Z (x:Z) : Z := pow_fn_rev_Z 254 254 x x. \end{lstlisting}  Benoit Viguier committed Aug 14, 2019 437 438 439 440 By using \lref{lemma:mult_correct}, we prove their equivalence in $\Zfield$. \begin{lemma} \label{lemma:Inv_equivalence} The function \coqe{Inv25519} over list of integers computes the same  Benoit Viguier committed Aug 16, 2019 441 result at \coqe{Inv25519_Z} over integers in \Zfield.  Benoit Viguier committed Aug 14, 2019 442 443 \end{lemma} This is formalized in Coq as follows:  Benoit Viguier committed Jun 21, 2019 444 445 446 447 448 449 \begin{lstlisting}[language=Coq] Lemma Inv25519_Z_GF : forall (g:list Z), length g = 16 -> (Z16.lst (Inv25519 g)) :GF = (Inv25519_Z (Z16.lst g)) :GF. \end{lstlisting}  Benoit Viguier committed Aug 17, 2019 450   Benoit Viguier committed Jul 22, 2019 451 In TweetNaCl, \TNaCle{inv25519} computes an inverse in $\Zfield$.  Benoit Viguier committed Aug 16, 2019 452 It uses Fermat's little theorem by doing an exponentiation to $2^{255}-21$.  Benoit Viguier committed Jun 21, 2019 453 This is done by applying a square-and-multiply algorithm. The binary representation  Benoit Viguier committed Aug 16, 2019 454 of $p-2$ implies to always do multiplications except for bits 2 and 4.  Benoit Viguier committed Jun 21, 2019 455 456 To prove the correctness of the result we can use multiple strategies such as: \begin{itemize}  Benoit Viguier committed Jul 22, 2019 457  \item Proving it is a special case of square-and-multiply algorithm applied to $2^{255}-21$.  Benoit Viguier committed Jun 21, 2019 458 459 460 461 462 463 464 465 466  \item Unrolling the for loop step-by-step and applying the equalities $x^a \times x^b = x^{(a+b)}$ and $(x^a)^2 = x^{(2 \times a)}$. We prove that the resulting exponent is $2^{255}-21$. \end{itemize} We use the second method for the benefits of simplicity. However it requires to apply the unrolling and exponentiation formulas 255 times. This can be automated in Coq with tacticals such as \Coqe{repeat}, but it generates a proof object which will take a long time to verify.  Benoit Viguier committed Aug 13, 2019 467   Benoit Viguier committed Aug 14, 2019 468 469 470 \subheading{Speeding up with Reflections.} This technique provides us with flexibility, \eg we don't need to know the number of times nor the order in which the lemmas needs to be applied (chapter 15 in \cite{CpdtJFR}).  Benoit Viguier committed Jun 21, 2019 471 472  The idea is to \textit{reflect} the goal into a decidable environment.  Benoit Viguier committed Aug 01, 2019 473 We show that for a property $P$, we can define a decidable Boolean property  Benoit Viguier committed Jun 21, 2019 474 475 476 477 478 479 480 $P_{bool}$ such that if $P_{bool}$ is \Coqe{true} then $P$ holds. $$reify\_P : P_{bool} = true \implies P$$ By applying $reify\_P$ on $P$ our goal become $P_{bool} = true$. We then compute the result of $P_{bool}$. If the decision goes well we are left with the tautology $true = true$. To prove that the \Coqe{Inv25519_Z} is computing $x^{2^{255}-21}$,  Benoit Viguier committed Aug 14, 2019 481 482 we define a Domain Specific Language (DSL). \begin{dfn}  Benoit Viguier committed Jun 21, 2019 483 484 485 Let \Coqe{expr_inv} denote an expression which is either a term; a multiplication of expressions; a squaring of an expression or a power of an expression. And Let \Coqe{formula_inv} denote an equality between two expressions.  Benoit Viguier committed Aug 14, 2019 486 \end{dfn}  Benoit Viguier committed Jun 21, 2019 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 \begin{lstlisting}[language=Coq] Inductive expr_inv := | R_inv : expr_inv | M_inv : expr_inv -> expr_inv -> expr_inv | S_inv : expr_inv -> expr_inv | P_inv : expr_inv -> positive -> expr_inv. Inductive formula_inv := | Eq_inv : expr_inv -> expr_inv -> formula_inv. \end{lstlisting} The denote functions are defined as follows: \begin{lstlisting}[language=Coq] Fixpoint e_inv_denote (m:expr_inv) : Z := match m with | R_inv => term_denote | M_inv x y => (e_inv_denote x) * (e_inv_denote y) | S_inv x => (e_inv_denote x) * (e_inv_denote x) | P_inv x p => pow (e_inv_denote x) (Z.pos p) end. Definition f_inv_denote (t : formula_inv) : Prop := match t with | Eq_inv x y => e_inv_denote x = e_inv_denote y end. \end{lstlisting} All denote functions also take as an argument the environment containing the variables.  Benoit Viguier committed Aug 14, 2019 517 518 We do not show it here for the sake of readability, given that an environment, \Coqe{term_denote} returns the appropriate variable.  Benoit Viguier committed Aug 16, 2019 519 With this Domain Specific Language we have the following equality:  Benoit Viguier committed Jun 21, 2019 520 521 522 523 524 525 526 527 \begin{lstlisting}[backgroundcolor=\color{white}] f_inv_denote (Eq_inv (M_inv R_inv (S_inv R_inv)) (P_inv R_inv 3)) = (x * x^2 = x^3) \end{lstlisting} On the right side, \Coqe{(x * x^2 = x^3)} depends on $x$. On the left side, \texttt{(Eq\_inv (M\_inv R\_inv (S\_inv R\_inv)) (P\_inv R\_inv 3))} does not depend on $x$.  Benoit Viguier committed Aug 01, 2019 528 This allows us to use computations in our decision procedure.  Benoit Viguier committed Jun 21, 2019 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545  We define \Coqe{step_inv} and \Coqe{pow_inv} to mirror the behavior of \Coqe{step_pow_Z} and respectively \Coqe{pow_fn_rev_Z} over our DSL and we prove their equality. \begin{lstlisting}[language=Coq] Lemma step_inv_step_pow_eq : forall (a:Z) (c:expr_inv) (g:expr_inv), e_inv_denote (step_inv a c g) = step_pow_Z a (e_inv_denote c) (e_inv_denote g). Lemma pow_inv_pow_fn_rev_eq : forall (a:Z) (b:Z) (c:expr_inv) (g:expr_inv), e_inv_denote (pow_inv a b c g) = pow_fn_rev_Z a b (e_inv_denote c) (e_inv_denote g). \end{lstlisting} We then derive the following lemma. \begin{lemma}  Benoit Viguier committed Aug 14, 2019 546 547 \label{lemma:reify} With an appropriate choice of variables, \Coqe{pow_inv} denotes \Coqe{Inv25519_Z}.  Benoit Viguier committed Jun 21, 2019 548 549 550 551 552 553 \end{lemma} In order to prove formulas in \Coqe{formula_inv}, we have the following a decidable procedure. We define \Coqe{pow_expr_inv}, a function which returns the power of an expression. We then compare the two values and decide over their equality.  Benoit Viguier committed Aug 06, 2019 554 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 555 556 557 Fixpoint pow_expr_inv (t:expr_inv) : Z := match t with (* power of a term is 1. *)  Benoit Viguier committed Aug 14, 2019 558 559  | R_inv => 1 (* x^a * x^b = x^{a+b}. *)  Benoit Viguier committed Jun 21, 2019 560 561  | M_inv x y => (pow_expr_inv x) + (pow_expr_inv y)  Benoit Viguier committed Aug 14, 2019 562  (* (x^a)^2 = x^{2a}. *)  Benoit Viguier committed Jun 21, 2019 563 564  | S_inv x => 2 * (pow_expr_inv x)  Benoit Viguier committed Aug 14, 2019 565  (* (x^b)^a = x^{a*b}. *)  Benoit Viguier committed Jun 21, 2019 566 567 568 569 570 571 572 573 574 575 576  | P_inv x p => (Z.pos p) * (pow_expr_inv x) end. Definition decide_e_inv (l1 l2:expr_inv) : bool := (pow_expr_inv l1) ==? (pow_expr_inv l2). Definition decide_f_inv (f:formula_inv) : bool := match f with | Eq_inv x y => decide_e_inv x y end.  Benoit Viguier committed Aug 06, 2019 577 \end{lstlisting}  Benoit Viguier committed Aug 17, 2019 578   Benoit Viguier committed Jun 21, 2019 579 580 We prove our decision procedure correct. \begin{lemma}  Benoit Viguier committed Aug 14, 2019 581 \label{lemma:decide}  Benoit Viguier committed Jun 21, 2019 582 583 584 585 For all formulas $f$, if the decision over $f$ returns \Coqe{true}, then the denoted equality by $f$ is true. \end{lemma} Which is formalized as:  Benoit Viguier committed Aug 06, 2019 586 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 587 588 589 Lemma decide_formula_inv_impl : forall (f:formula_inv), decide_f_inv f = true ->  Benoit Viguier committed Aug 14, 2019 590  f_inv_denote f.  Benoit Viguier committed Aug 06, 2019 591 \end{lstlisting}  Benoit Viguier committed Aug 17, 2019 592   Benoit Viguier committed Aug 14, 2019 593 594 By reification to over DSL (\lref{lemma:reify}) and by applying our decision (\lref{lemma:decide}), we prove the following corollary.  Benoit Viguier committed Aug 13, 2019 595 \begin{lemma}  Benoit Viguier committed Aug 14, 2019 596 \label{lemma:inv_comput_inv}  Benoit Viguier committed Jun 21, 2019 597 \Coqe{Inv25519_Z} computes an inverse in \Zfield.  Benoit Viguier committed Aug 13, 2019 598 \end{lemma}  Benoit Viguier committed Aug 14, 2019 599 Which is formalized as:  Benoit Viguier committed Aug 06, 2019 600 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 601 602 603 Theorem Inv25519_Z_correct : forall (x:Z), Inv25519_Z x = pow x (2^255-21).  Benoit Viguier committed Aug 06, 2019 604 \end{lstlisting}  Benoit Viguier committed Jun 21, 2019 605   Benoit Viguier committed Aug 16, 2019 606 607 % From \Coqe{Inv25519_Z_GF} (\lref{lemma:Inv_equivalence}) and \Coqe{Inv25519_Z_correct} (Corollary~\ref{lemma:inv_comput_inv}), From \lref{lemma:Inv_equivalence} and Corollary~\ref{lemma:inv_comput_inv},  Benoit Viguier committed Aug 14, 2019 608 we conclude the functional correctness of the inversion over \Zfield.  Benoit Viguier committed Jun 21, 2019 609 \begin{corollary}  Benoit Viguier committed Aug 13, 2019 610 \label{cor:inv_comput_field}  Benoit Viguier committed Jun 21, 2019 611 612 \Coqe{Inv25519} computes an inverse in \Zfield. \end{corollary}  Benoit Viguier committed Aug 14, 2019 613 Which is formalized as:  Benoit Viguier committed Aug 06, 2019 614 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 615 616 617 618 619 Corollary Inv25519_Zpow_GF : forall (g:list Z), length g = 16 -> Z16.lst (Inv25519 g) :GF = (pow (Z16.lst g) (2^255-21)) :GF.  Benoit Viguier committed Aug 06, 2019 620 \end{lstlisting}  Benoit Viguier committed Jun 21, 2019 621   Benoit Viguier committed Aug 13, 2019 622 \subheading{Another applications of reflections: packing}  Benoit Viguier committed Aug 14, 2019 623 This reflection technique can also be used where proofs requires some computing  Benoit Viguier committed Aug 16, 2019 624 over a small and finite domain of variables to test e.g. for all $i$ such that $0 \le i < 16$.  Benoit Viguier committed Jun 21, 2019 625 626 627 628 629 630 631 Using reflection we prove that we can split the for loop in \TNaCle{pack25519} into two parts. \begin{lstlisting}[language=Ctweetnacl] for(i=1;i<15;i++) { m[i]=t[i]-0xffff-((m[i-1]>>16)&1); m[i-1]&=0xffff; } \end{lstlisting}  Benoit Viguier committed Aug 16, 2019 632 The first loop is computing the subtraction while the second is applying the carries.  Benoit Viguier committed Jun 21, 2019 633 634 635 636 \begin{lstlisting}[language=Ctweetnacl] for(i=1;i<15;i++) { m[i]=t[i]-0xffff }  Benoit Viguier committed Aug 16, 2019 637   Benoit Viguier committed Jun 21, 2019 638 639 640 641 642 for(i=1;i<15;i++) { m[i]=m[i]-((m[i-1]>>16)&1); m[i-1]&=0xffff; } \end{lstlisting}  Benoit Viguier committed Aug 17, 2019 643   Benoit Viguier committed Aug 01, 2019 644 This loop separation allows simpler proofs. The first loop is seen as the subtraction of a number in \Zfield.  Benoit Viguier committed Jul 10, 2019 645 We then prove that with the iteration of the second loop, the number represented in $\Zfield$ stays the same.  Benoit Viguier committed Aug 16, 2019 646 This leads to the proof that \TNaCle{pack25519} is effectively reducing modulo $\p$ and returning a number in base $2^8$.  Benoit Viguier committed Aug 06, 2019 647 \begin{lstlisting}[language=Coq]  Benoit Viguier committed Jun 21, 2019 648 Lemma Pack25519_mod_25519 :  Benoit Viguier committed Aug 16, 2019 649 650 651 652 653  forall (l:list Z), Zlength l = 16 -> Forall (fun x => -2^62 < x < 2^62) l -> ZofList 8 (Pack25519 l) = (Z16.lst l) mod (2^255-19).  Benoit Viguier committed Aug 06, 2019 654 \end{lstlisting}  Benoit Viguier committed Jul 10, 2019 655   Benoit Viguier committed Aug 14, 2019 656 657 658 659 By proving that each functions \coqe{Low.M}; \coqe{Low.A}; \coqe{Low.Sq}; \coqe{Low.Zub}; \coqe{Unpack25519}; \coqe{clamp}; \coqe{Pack25519}; \coqe{car25519} are behaving over \coqe{list Z} as their equivalent over \coqe{Z} in \coqe{:GF} (in \Zfield), we prove the correctness of \tref{thm:RFC}. This is formalized as follows in Coq:  Benoit Viguier committed Aug 12, 2019 660 661 662 663 664 665 666 667 668 669 \begin{lstlisting}[language=Coq] Theorem Crypto_Scalarmult_Eq : forall (n p:list Z), Zlength n = 32 -> Zlength p = 32 -> Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) n -> Forall (fun x : Z, 0 <= x /\ x < 2 ^ 8) p -> ZofList 8 (Crypto_Scalarmult n p) = ZCrypto_Scalarmult (ZofList 8 n) (ZofList 8 p). \end{lstlisting}