2_preliminaries.tex 13.5 KB
 Peter Schwabe committed Jun 20, 2019 1 \section{Preliminaries}  Benoit Viguier committed Aug 12, 2019 2 \label{sec:preliminaries}  Benoit Viguier committed Jul 10, 2019 3   Peter Schwabe committed Jul 30, 2019 4 5 6 7 In this section, we first give a brief summary of the mathematical background on elliptic curves. We then describe X25519 and its implementation in TweetNaCl. Finally, we provide a brief description of the formal tools we use in our proofs.  Benoit Viguier committed Sep 02, 2019 8   Peter Schwabe committed Jul 30, 2019 9 \subsection{Arithmetic on Montgomery curves}  Benoit Viguier committed Aug 12, 2019 10 \label{subsec:arithmetic-montgomery}  Peter Schwabe committed Jul 30, 2019 11   Benoit Viguier committed Aug 12, 2019 12 \begin{dfn}  Benoit Viguier committed Sep 02, 2019 13  Given a field \K, let $a,b \in \K$ such that $a^2 \neq 4$ and $b \neq 0$,  Peter Schwabe committed Sep 28, 2019 14 15  $M_{a,b}$ is the Montgomery curve defined over $\K$ with equation $$M_{a,b}: by^2 = x^3 + ax^2 + x.$$  Benoit Viguier committed Aug 12, 2019 16 \end{dfn}  Benoit Viguier committed Aug 01, 2019 17   Benoit Viguier committed Aug 12, 2019 18 \begin{dfn}  Peter Schwabe committed Sep 28, 2019 19 20 21 22  For any algebraic extension $\L \supseteq \K$, we call $M_{a,b}(\L)$ the set of $\L$-rational points defined as $$M_{a,b}(\L) = \{\Oinf\} \cup \{(x,y) \in \L \times \L~|~by^2 = x^3 + ax^2 + x\}.$$ Here, the additional element $\Oinf$ denotes the point at infinity.  Benoit Viguier committed Aug 12, 2019 23 24 \end{dfn} Details of the formalization can be found in \sref{subsec:ECC-Montgomery}.  Benoit Viguier committed Aug 01, 2019 25   Benoit Viguier committed Sep 27, 2019 26   Peter Schwabe committed Sep 28, 2019 27 For $M_{a,b}$ over a finite field $\F{p}$, the parameter $b$ is known as the twisting factor''.  Benoit Viguier committed Sep 27, 2019 28 For $b'\in \F{p}\backslash\{0\}$ and $b' \neq b$, the curves $M_{a,b}$ and $M_{a,b'}$  Benoit Viguier committed Sep 02, 2019 29 30 are isomorphic via $(x,y) \mapsto (x, \sqrt{b'/b} \cdot y)$.  Benoit Viguier committed Aug 12, 2019 31 \begin{dfn}  Peter Schwabe committed Sep 28, 2019 32 33  When $b'/b$ is not a square in \F{p}, $M_{a,b'}$ is a \emph{quadratic twist} of $M_{a,b}$, i.e., a curve that is isomorphic over $\F{p^2}$~\cite{cryptoeprint:2017:212}.  Benoit Viguier committed Aug 12, 2019 34 \end{dfn}  Benoit Viguier committed Aug 01, 2019 35   Peter Schwabe committed Sep 28, 2019 36 Points in $M_{a,b}(\K)$ can be equipped with a structure of an abelian group  Benoit Viguier committed Sep 27, 2019 37 with the addition operation $+$ and with neutral element the point at infinity $\Oinf$.  Peter Schwabe committed Sep 28, 2019 38 39 For a point $P \in M_{a,b}(\K)$ and a positive integer $n$ we obtain the scalar product $$n\cdot P = \underbrace{P + \cdots + P}_{n\text{ times}}.$$  Benoit Viguier committed Aug 01, 2019 40   Benoit Viguier committed Sep 27, 2019 41 In order to efficiently compute the scalar multiplication we use an algorithm  Benoit Viguier committed Sep 02, 2019 42 similar to square-and-multiply: the Montgomery ladder where the basic operations  Peter Schwabe committed Sep 28, 2019 43 are differential addition and doubling~\cite{MontgomerySpeeding}.  Benoit Viguier committed Sep 02, 2019 44   Benoit Viguier committed Sep 30, 2019 45 We consider \xcoord-only operations. Throughout the computation,  Peter Schwabe committed Sep 28, 2019 46 47 48 these $x$-coordinates are kept in projective representation $(X : Z)$, with $x = X/Z$; the point at infinity is represented as $(1:0)$. See \sref{subsec:ECC-projective} for more details.  Benoit Viguier committed Sep 27, 2019 49 We define two operations:  Benoit Viguier committed Aug 01, 2019 50 \begin{align*}  Peter Schwabe committed Sep 28, 2019 51  \texttt{xADD} &: (x_{Q-P}, (X_P:Z_P), (X_Q:Z_Q)) \mapsto \\  Benoit Viguier committed Sep 27, 2019 52 53 &(X_{P + Q}:Z_{P + Q})\\ \texttt{xDBL} &: (X_P:Z_P) \mapsto (X_{2 \cdot P}:Z_{2 \cdot P})  Benoit Viguier committed Aug 01, 2019 54 \end{align*}  Benoit Viguier committed Sep 02, 2019 55 56 In the Montgomery ladder, % notice that the arguments of \texttt{xADD} and \texttt{xDBL}  Benoit Viguier committed Aug 07, 2019 57 are swapped depending of the value of the $k^{th}$ bit. We use a conditional  Benoit Viguier committed Aug 12, 2019 58 59 swap \texttt{CSWAP} to change the arguments of the above function while keeping the same body of the loop.  Peter Schwabe committed Sep 28, 2019 60 61 Given a pair $(P_0, P_1)$ and a bit $b$, \texttt{CSWAP} returns the pair $(P_b, P_{1-b})$.  Benoit Viguier committed Aug 06, 2019 62 63  By using the differential addition and doubling operations we define the Montgomery ladder  Benoit Viguier committed Sep 27, 2019 64 computing a \xcoord-only scalar multiplication (see \aref{alg:montgomery-ladder}).  Benoit Viguier committed Aug 01, 2019 65 66 \begin{algorithm} \caption{Montgomery ladder for scalar mult.}  Benoit Viguier committed Aug 12, 2019 67 \label{alg:montgomery-ladder}  Benoit Viguier committed Aug 01, 2019 68 \begin{algorithmic}  Peter Schwabe committed Sep 28, 2019 69 70 71 72 73 74 75 76 77 78 79  \REQUIRE{\xcoord $x_P$ of a point $P$, scalar $n$ with $n < 2^m$} \ENSURE{\xcoord $x_Q$ of $Q = n \cdot P$} \STATE $Q = (X_Q:Z_Q) \leftarrow (1:0)$ \STATE $R = (X_R:Z_R) \leftarrow (x_P:1)$ \FOR{$k$ := $m$ down to $1$} \STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$ \STATE $Q \leftarrow \texttt{xDBL}(Q)$ \STATE $R \leftarrow \texttt{xADD}(x_P,Q,R)$ \STATE $(Q,R) \leftarrow \texttt{CSWAP}((Q,R), k^{\text{th}}\text{ bit of }n)$ \ENDFOR \RETURN $X_Q/Z_Q$  Benoit Viguier committed Aug 01, 2019 80 81 \end{algorithmic} \end{algorithm}  Benoit Viguier committed Jul 10, 2019 82   Benoit Viguier committed Sep 02, 2019 83 84   Peter Schwabe committed Jun 20, 2019 85 \subsection{The X25519 key exchange}  Benoit Viguier committed Aug 12, 2019 86 \label{subsec:X25519-key-exchange}  Benoit Viguier committed Jul 10, 2019 87   Peter Schwabe committed Sep 28, 2019 88 89 From now on let $\F{p}$ be the field with $p=2^{255}-19$ elements. We consider the elliptic curve $E$ over $\F{p}$ defined by the  Benoit Viguier committed Sep 30, 2019 90 equation $y^2 = x^3 + 486662 x^2 + x$.  Peter Schwabe committed Sep 28, 2019 91 For every $x \in \F{p}$ there exist a point $P$ in $E(\F{p^2})$  Benoit Viguier committed Sep 27, 2019 92 such that $x$ is the \xcoord of $P$.  Peter Schwabe committed Jun 20, 2019 93   Peter Schwabe committed Sep 28, 2019 94 The core of the X25519 key-exchange protocol is a scalar-multiplication  Benoit Viguier committed Sep 30, 2019 95 function, which we will also refer to as X25519.  Peter Schwabe committed Sep 28, 2019 96 This function receives as input two arrays of $32$ bytes each.  Benoit Viguier committed Sep 30, 2019 97 98 One of them is interpreted as the little-endian encoding of a non-negative integer $n$ (see \ref{subsec:integer-bytes}).  Peter Schwabe committed Sep 28, 2019 99 100 101 102 103 104 105 106 107 The other is interpreted as the little-endian encoding of the \xcoord $x_P \in \F{p}$ of a point in $E(\F{p^2})$, using the standard mapping of integers modulo $p$ to elements in $\F{p}$. The X25519 function first computes a scalar $n'$ by setting bit 255 of $n$ to \texttt{0}; setting bit 254 to \texttt{1} and setting the lower 3 bits to \texttt{0}. This operation is often called clamping'' of the scalar $n$. Note that $n' \in 2^{254} + 8\{0,1,\ldots,2^{251}-1\}$. X25519 then computes the \xcoord of $n'\cdot P$.  Benoit Viguier committed Jun 21, 2019 108   Benoit Viguier committed Sep 27, 2019 109 110 111 112 RFC~7748~\cite{rfc7748} standardized the X25519 Diffie–Hellman key-exchange algorithm. Given the base point $B$ where $X_B=9$, each party generate a secret random number $s_a$ (respectively $s_b$), and computes $X_{P_a}$ (respectively $X_{P_b}$), the \xcoord of $P_A = s_a \cdot B$ (respectively $P_B = s_b \cdot B$).  Benoit Viguier committed Sep 30, 2019 113 The parties exchange $X_{P_a}$ and $X_{P_b}$ and compute their shared secret with  Peter Schwabe committed Sep 28, 2019 114 X25519 on $s_a$ and $X_{P_b}$ (respectively $s_b$ and $X_{P_a}$).  Benoit Viguier committed Sep 02, 2019 115   Peter Schwabe committed Jul 30, 2019 116 \subsection{TweetNaCl specifics}  Benoit Viguier committed Aug 12, 2019 117 \label{subsec:Number-TweetNaCl}  Benoit Viguier committed Aug 06, 2019 118   Peter Schwabe committed Sep 28, 2019 119 As its name suggests, TweetNaCl aims for code compactness (\emph{a crypto library in 100 tweets''}).  Benoit Viguier committed Sep 27, 2019 120 As a result it uses a few defines and typedefs to gain precious bytes while  Benoit Viguier committed Aug 01, 2019 121 still remaining readable.  Benoit Viguier committed Jul 22, 2019 122 123 124 125 \begin{lstlisting}[language=Ctweetnacl] #define FOR(i,n) for (i = 0;i < n;++i) #define sv static void typedef unsigned char u8;  Peter Schwabe committed Jul 30, 2019 126 typedef long long i64;  Benoit Viguier committed Jul 22, 2019 127 \end{lstlisting}  Benoit Viguier committed Aug 06, 2019 128   Benoit Viguier committed Sep 02, 2019 129 130 TweetNaCl functions take pointers as arguments. By convention the first one points to the output array. It is then followed by the input arguments.  Benoit Viguier committed Aug 06, 2019 131 132 133  Due to some limitations of VST, indexes used in \TNaCle{for} loops have to be of type \TNaCle{int} instead of \TNaCle{i64}. We change the code to allow our  Benoit Viguier committed Sep 02, 2019 134 135 proofs to carry through. We believe this does not affect the correctness of the original code. A complete diff of our modifications to TweetNaCl can be found in  Benoit Viguier committed Aug 06, 2019 136 137 Appendix~\ref{verified-C-and-diff}.  Benoit Viguier committed Sep 02, 2019 138   Peter Schwabe committed Jul 30, 2019 139 \subsection{X25519 in TweetNaCl}  Benoit Viguier committed Aug 12, 2019 140 \label{subsec:X25519-TweetNaCl}  Peter Schwabe committed Jul 30, 2019 141   Benoit Viguier committed Aug 01, 2019 142 We now describe the implementation of X25519 in TweetNaCl.  Benoit Viguier committed Jul 22, 2019 143 144  \subheading{Arithmetic in \Ffield.}  Peter Schwabe committed Jul 30, 2019 145 In X25519, all computations are performed in $\F{p}$.  Benoit Viguier committed Aug 01, 2019 146 147 Throughout the computation, elements of that field are represented in radix $2^{16}$,  Peter Schwabe committed Sep 28, 2019 148 i.e., an element $A$ is represented as $(a_0,\dots,a_{15})$,  Peter Schwabe committed Jul 30, 2019 149 150 151 with $A = \sum_{i=0}^{15}a_i2^{16i}$. The individual limbs'' $a_i$ are represented as 64-bit \TNaCle{long long} variables:  Benoit Viguier committed Jun 21, 2019 152 153 154 155 \begin{lstlisting}[language=Ctweetnacl] typedef i64 gf[16]; \end{lstlisting}  Benoit Viguier committed Sep 27, 2019 156 157 Conversion from the input byte array to this representation in radix $2^{16}$ is done as follows:  Benoit Viguier committed Aug 01, 2019 158 159 160 161 162 163 164 165 \begin{lstlisting}[language=Ctweetnacl] sv unpack25519(gf o, const u8 *n) { int i; FOR(i,16) o[i]=n[2*i]+((i64)n[2*i+1]<<8); o[15]&=0x7fff; } \end{lstlisting}  Peter Schwabe committed Jul 30, 2019 166 167  The radix-$2^{16}$ representation in limbs of $64$ bits is  Benoit Viguier committed Sep 20, 2019 168 highly redundant; for any element $A \in \Ffield$ there are  Peter Schwabe committed Jul 30, 2019 169 multiple ways to represent $A$ as $(a_0,\dots,a_{15})$.  Benoit Viguier committed Sep 02, 2019 170 This is used to avoid carry handling in the implementations of addition  Benoit Viguier committed Sep 20, 2019 171 (\TNaCle{A}) and subtraction (\TNaCle{Z}) in $\Ffield$:  Benoit Viguier committed Jul 12, 2019 172 173 174 175 176 177 178 179 180 181 \begin{lstlisting}[language=Ctweetnacl] sv A(gf o,const gf a,const gf b) { int i; FOR(i,16) o[i]=a[i]+b[i]; } sv Z(gf o,const gf a,const gf b) { int i; FOR(i,16) o[i]=a[i]-b[i]; }  Peter Schwabe committed Jul 30, 2019 182 183 184 185 186 \end{lstlisting} Also multiplication (\TNaCle{M}) is heavily exploiting the redundancy of the representation to delay carry handling. \begin{lstlisting}[language=Ctweetnacl]  Benoit Viguier committed Jul 12, 2019 187 188 189 190 191 192 193 194 195 196 sv M(gf o,const gf a,const gf b) { i64 i,j,t[31]; FOR(i,31) t[i]=0; FOR(i,16) FOR(j,16) t[i+j]+=a[i]*b[j]; FOR(i,15) t[i]+=38*t[i+16]; FOR(i,16) o[i]=t[i]; car25519(o); car25519(o); } \end{lstlisting}  Benoit Viguier committed Jun 21, 2019 197   Peter Schwabe committed Jul 30, 2019 198 199 200 After the actual multiplication, the limbs of the result \texttt{o} are too large to be used again as input, which is why the two calls to \TNaCle{car25519} at the end of \TNaCle{M} propagate the carries through the limbs:  Benoit Viguier committed Jul 12, 2019 201 202 203 204 205 206 207 \begin{lstlisting}[language=Ctweetnacl] sv car25519(gf o) { int i; FOR(i,16) { o[(i+1)%16]+=(i<15?1:38)*(o[i]>>16); o[i]&=0xffff;  Benoit Viguier committed Jun 21, 2019 208  }  Benoit Viguier committed Jul 12, 2019 209 210 } \end{lstlisting}  Benoit Viguier committed Aug 06, 2019 211   Benoit Viguier committed Aug 05, 2019 212 In order to simplify the verification of this function,  Benoit Viguier committed Sep 02, 2019 213 we treat the last iteration of the loop $i = 15$ as a separate step.  Benoit Viguier committed Jul 12, 2019 214   Benoit Viguier committed Sep 30, 2019 215 216 217 Inverses in $\Ffield$ are computed with \TNaCle{inv25519}. This function uses exponentiation by $2^{255}-21$, computed with the square-and-multiply algorithm.  Peter Schwabe committed Sep 28, 2019 218 Fermat's little theorem gives the correctness.  Benoit Viguier committed Jul 12, 2019 219 Notice that in this case the inverse of $0$ is defined as $0$.  Benoit Viguier committed Sep 27, 2019 220 221 222 223 224 225 226 227 228 229 230 231 232 \begin{lstlisting}[language=Ctweetnacl] sv inv25519(gf o,const gf i) { gf c; int a; set25519(c,i); for(a=253;a>=0;a--) { S(c,c); if(a!=2&&a!=4) M(c,c,i); } FOR(a,16) o[a]=c[a]; } \end{lstlisting}  Benoit Viguier committed Jul 12, 2019 233   Benoit Viguier committed Aug 12, 2019 234 235 \TNaCle{sel25519} implements a constant-time conditional swap (\texttt{CSWAP}) by applying a mask between two fields elements.  Benoit Viguier committed Aug 07, 2019 236 237 238 239 240 241 242 243 244 245 246 247 \begin{lstlisting}[language=Ctweetnacl] sv sel25519(gf p,gf q,i64 b) { int i; i64 t,c=~(b-1); FOR(i,16) { t= c&(p[i]^q[i]); p[i]^=t; q[i]^=t; } } \end{lstlisting}  Peter Schwabe committed Jul 30, 2019 248   Benoit Viguier committed Sep 27, 2019 249 Finally, we need the \TNaCle{pack25519} function,  Peter Schwabe committed Jul 30, 2019 250 which converts from the internal redundant radix-$2^{16}$  Peter Schwabe committed Sep 28, 2019 251 252 representation to a unique byte array representing an integer in $\{0,\dots,p-1\}$ in little-endian format.  Benoit Viguier committed Jul 12, 2019 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 \begin{lstlisting}[language=Ctweetnacl] sv pack25519(u8 *o,const gf n) { int i,j; i64 b; gf t,m={0}; set25519(t,n); car25519(t); car25519(t); car25519(t); FOR(j,2) { m[0]=t[0]- 0xffed; for(i=1;i<15;i++) { m[i]=t[i]-0xffff-((m[i-1]>>16)&1); m[i-1]&=0xffff;  Benoit Viguier committed Jun 21, 2019 268  }  Benoit Viguier committed Jul 12, 2019 269 270 271 272  m[15]=t[15]-0x7fff-((m[14]>>16)&1); m[14]&=0xffff; b=1-((m[15]>>16)&1); sel25519(t,m,b);  Benoit Viguier committed Jun 21, 2019 273  }  Benoit Viguier committed Jul 12, 2019 274 275 276  FOR(i,16) { o[2*i]=t[i]&0xff; o[2*i+1]=t[i]>>8;  Benoit Viguier committed Jun 21, 2019 277  }  Benoit Viguier committed Jul 12, 2019 278 279 } \end{lstlisting}  Peter Schwabe committed Jul 30, 2019 280 As we can see, this function is considerably more complex than the  Benoit Viguier committed Aug 01, 2019 281 unpacking function. The reason is that it needs to convert  Peter Schwabe committed Sep 28, 2019 282 283 to a \emph{unique} representation, i.e., also fully reduce modulo $p$ and remove the redundancy of the radix-$2^{16}$ representation.  Peter Schwabe committed Jul 30, 2019 284   Benoit Viguier committed Jul 22, 2019 285 \subheading{The Montgomery ladder.}  Benoit Viguier committed Sep 30, 2019 286 With these low-level arithmetic and helper functions defined,  Peter Schwabe committed Sep 28, 2019 287 288 289 290 we can now turn our attention to the core of the X25519 computation: the \TNaCle{crypto_scalarmult} API function of TweetNaCl, which is implemented through the Montgomery ladder.  Benoit Viguier committed Jul 12, 2019 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 \begin{lstlisting}[language=Ctweetnacl] int crypto_scalarmult(u8 *q, const u8 *n, const u8 *p) { u8 z[32]; i64 r; int i; gf x,a,b,c,d,e,f; FOR(i,31) z[i]=n[i]; z[31]=(n[31]&127)|64; z[0]&=248; unpack25519(x,p); FOR(i,16) { b[i]=x[i]; d[i]=a[i]=c[i]=0; } a[0]=d[0]=1; for(i=254;i>=0;--i) { r=(z[i>>3]>>(i&7))&1; sel25519(a,b,r); sel25519(c,d,r); A(e,a,c); Z(a,a,c); A(c,b,d); Z(b,b,d); S(d,e); S(f,a); M(a,c,a); M(c,b,e); A(e,a,c); Z(a,a,c); S(b,a); Z(c,d,f); M(a,c,_121665); A(a,a,d); M(c,c,a); M(a,d,f); M(d,b,x); S(b,e); sel25519(a,b,r); sel25519(c,d,r);  Benoit Viguier committed Jun 21, 2019 333  }  Benoit Viguier committed Jul 12, 2019 334 335 336 337 338 339  inv25519(c,c); M(a,a,c); pack25519(q,a); return 0; } \end{lstlisting}  Peter Schwabe committed Sep 28, 2019 340 341 %XXX: I really want line numbers here to link lines in this code to % the pseudocode description  Benoit Viguier committed Sep 02, 2019 342 343   Peter Schwabe committed Sep 28, 2019 344 \subsection{Coq, separation logic, and VST}  Benoit Viguier committed Aug 12, 2019 345 \label{subsec:Coq-VST}  Benoit Viguier committed Jul 10, 2019 346   Benoit Viguier committed Sep 27, 2019 347 348 Coq~\cite{coq-faq} is an interactive theorem prover based on type theory. It provides an expressive formal language to write mathematical definitions,  Peter Schwabe committed Sep 28, 2019 349 350 351 352 algorithms, and theorems together with their proofs. It has been used in the proof of the four-color theorem~\cite{gonthier2008formal} and it is also the system underlying the CompCert formally verified C compiler~\cite{Leroy-backend}. Unlike systems like F*~\cite{DBLP:journals/corr/BhargavanDFHPRR17},  Benoit Viguier committed Aug 01, 2019 353 354 Coq does not rely on an SMT solver in its trusted code base. It uses its type system to verify the applications of hypotheses,  Peter Schwabe committed Jul 30, 2019 355 lemmas, and theorems~\cite{Howard1995-HOWTFN}.  Benoit Viguier committed Jul 16, 2019 356   Benoit Viguier committed Jul 22, 2019 357 358 Hoare logic is a formal system which allows reasoning about programs. It uses triples such as  Benoit Viguier committed Jul 16, 2019 359 360 $$\{{\color{doc@lstnumbers}\textbf{Pre}}\}\texttt{~Prog~}\{{\color{doc@lstdirective}\textbf{Post}}\}$$ where ${\color{doc@lstnumbers}\textbf{Pre}}$ and ${\color{doc@lstdirective}\textbf{Post}}$  Benoit Viguier committed Sep 02, 2019 361 are assertions and \texttt{Prog} is a fragment of code.  Benoit Viguier committed Aug 01, 2019 362 363 It is read as when the precondition ${\color{doc@lstnumbers}\textbf{Pre}}$ is met,  Peter Schwabe committed Jul 30, 2019 364 365 executing \texttt{Prog} will yield postcondition ${\color{doc@lstdirective}\textbf{Post}}$''. We use compositional rules to prove the truth value of a Hoare triple.  Benoit Viguier committed Jul 16, 2019 366 367 368 369 370 371 372 For example, here is the rule for sequential composition: \begin{prooftree} \AxiomC{$\{P\}C_1\{Q\}$} \AxiomC{$\{Q\}C_2\{R\}$} \LeftLabel{Hoare-Seq} \BinaryInfC{$\{P\}C_1;C_2\{R\}$} \end{prooftree}  Benoit Viguier committed Jul 22, 2019 373 374 Separation logic is an extension of Hoare logic which allows reasoning about pointers and memory manipulation. This logic enforces strict conditions on the  Benoit Viguier committed Aug 05, 2019 375 memory shared such as being disjoint.  Benoit Viguier committed Aug 12, 2019 376 We discuss this limitation further in \sref{subsec:with-VST}.  Peter Schwabe committed Sep 28, 2019 377   Benoit Viguier committed Aug 05, 2019 378 The Verified Software Toolchain (VST)~\cite{cao2018vst-floyd} is a framework  Benoit Viguier committed Sep 27, 2019 379 380 which uses Separation logic proven correct with respect to CompCert semantics to prove the functional correctness of C programs.  Benoit Viguier committed Aug 21, 2019 381 The first step consists of translating the source code into Clight,  Benoit Viguier committed Aug 05, 2019 382 an intermediate representation used by CompCert.  Peter Schwabe committed Sep 28, 2019 383 For such purpose one uses the parser of CompCert called \texttt{clightgen}.  Benoit Viguier committed Sep 27, 2019 384 385 In a second step one defines the Hoare triple representing the specification of the piece of software one wants to prove. Then using VST, one uses a strongest  Benoit Viguier committed Aug 05, 2019 386 387 postcondition approach to prove the correctness of the triple. This approach can be seen as a forward symbolic execution of the program.