Case App: on case $(H, \fplug{LE}{\elet{x:t}{f\;lv}{le}})\step(H, \fplug{LE}{\elet{x:t}{\subst{y}{lv}{le_1}}}{le})$ and $lp(f)=\lambda y:t_1.\;le_1:t_2$.

Appealing to Lemma <ref>, we have $ss=(t\;x=f(v);ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$.

Because $\lowtocd{lp}=p$, we know $le_1=\withframe\;le_2$ and $\lowtoc{le_2}=ss_2;e$ and $p(f)=\ecfuntwo{y}{t_1}{t_2}{ss_1}$ and $ss_1=(ss_2;\ereturn\;e)$.

Appealing to Lemma <ref>, we know $\ctolow{ss_1}=le_2$ hence $\ctolow{\{ss_1\}}=le_1$.

Pick $C'$ to be $(S;(\None, V, t\;x=\symhole;ss'), \{y\mapsto v\}, \{ss_1\})$.

It suffices to show that

$(H, \fplug{LE}{\elet{x:t}{\subst{v}{lv}{le_1}}{le}})\;R\;(S;(\None, V, t\;x=\symhole;ss'), \{y\mapsto v\}, \{ss_1\})$, which is true.

End of case.

Case Withframe:

on case $(H, \fplug{LE}{\withframe\;le})\step(H;\{\}, \fplug{LE}{\epop\;le})$.

Appealing to Lemma <ref>, we have $ss=\{ss_1\};ss_2$ and $le=V(\ctolow{ss_1})$ and $LE=\unravel(S, V(\ctolowE{(\symhole;ss_2)}))$.

Pack $C'$ to be $(S;(\{\}, V, \symhole;ss_2), V, ss_1)$.

It suffices to show that

$(H;\{\}, \fplug{LE}{\epop\;le})\;R\;(S;(\{\}, V, \symhole;ss_2), V, ss_1)$, which is true.

End of case.

Case Newbuf: on case $(H;h, \fplug{LE}{\elet{x}{\enewbuf{n}{(lv:t)}}{le}})\step_{\symwrite\;(b,0,[]),\dots,\symwrite\;(b,n-1,[])}(H;h[b\mapsto lv^n], \fplug{LE}{\subst{x}{(b,0,[])}{le}})$ and $b\not\in H;h$.

We have $(H;h, \fplug{LE}{\elet{x}{\enewbuf{n}{(lv:t)}}{le}})\;R\;(S, V, ss)$.

We are to exhibit $C'$ so that

$(H;h[b\mapsto lv^n], \subst{x}{(b,0,[])}{le})\;R\;C'$ and $(S, V, ss)\step^+C'$.

Appealing to Lemma <ref>, we have $ss=(\earray{t}{x}{n};\memset{x}{n}{v};ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$ and $S=S';(M, V', E)$.

Pick $C'$ to be $(S';(M[b\mapsto v^n], V', E), V[x\mapsto(b,0, [])], ss')$.

It suffices to show that $(H;h[b\mapsto lv^n], \fplug{LE}{\subst{x}{(b,0,[])}{le}})\;R\;(S';(M[b\mapsto v^n], V', E), V[x\mapsto(b,0,[])], ss')$, which is true.

End of case.

Case Newstruct: on case $(H;h,\fplug{LE}{\elet{x}{\enewstruct{(lv:t)}}{le}})\step_{\symwrite\;(b,0,[])}(H;h[b\mapsto lv], \subst{x}{(b,0,[])}{le})$ and $b\not\in H;h$.

We have $(H;h, \elet{x}{\enewstruct{(lv:t)}}{le})\;R\;(S, V, ss)$.

We are to exhibit $C'$ so that

$(H;h[b\mapsto lv], \fplug{LE}{\subst{x}{(b,0,[])}{le}})\;R\;C'$ and $(S, V, ss)\step^+C'$.

Appealing to Lemma <ref>, we have $ss=(\earray{t}{x}{1};\memset{x}{1}{v};ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$ and $S=S';(M, V', E)$.

Pick $C'$ to be $(S';(M[b\mapsto v], V', E), V[x\mapsto(b,0, [])], ss')$.

It suffices to show that $(H;h[b\mapsto lv], \fplug{LE}{\subst{x}{(b,0,[])}{le}})\;R\;(S';(M[b\mapsto v], V', E), V[x\mapsto(b,0,[])], ss')$, which is true.

End of case.

Case Readbuf: on case

$(H, \fplug{LE}{\elet{x:t}{\ereadbuf{(b,n,[])}{n'}}{le}})\step_{\symread\;(b,n+n',[])}(H, \fplug{LE}{\subst{x}{lv}{le}})$ and $H(b,n+n',[])=lv$.

Appealing to Lemma <ref>, we have $ss=(t\;x=(b,n,[])[n'];ss')$ and $le=V(\ctolow{ss'})$ and $LE=\unravel(S, \symhole)$.

Pick $C'$ to be $(S, V[x\mapsto v], ss')$ where $v=\lowtoce{lv}$.

We know $C\step^+_{\symread\;(b,n+n',[])}C'.$

It suffices to show that $(H, \fplug{LE}{\subst{x}{lv}{le}})\;R\;(S, V[x\mapsto v], ss')$, which is true because $\subst{x}{lv}{le}=V[x\mapsto v](\ctolow{ss'})$.

End of case.

Case Readstruct: on case

$(H, \fplug{LE}{\elet{x:t}{\ereadstruct{(b,n,\ls{fd})}}{le}})\step_{\symread\;(b,n,\ls{fd})}(H, \fplug{LE}{\subst{x}{lv}{le}})$ and $H(b,n,\ls{fd})=lv$.

Appealing to Lemma <ref>, we have $ss=(t\;x=\eread{(b,n,\ls{fd})};ss')$ and $le=V(\ctolow{ss'})$ and $LE=\unravel(S, \symhole)$.

Pick $C'$ to be $(S, V[x\mapsto v], ss')$ where $v=\lowtoce{lv}$.

We know $C\step^+_{\symread\;(b,n,\ls{fd})}C'.$

It suffices to show that $(H, \fplug{LE}{\subst{x}{lv}{le}})\;R\;(S, V[x\mapsto v], ss')$, which is true because $\subst{x}{lv}{le}=V[x\mapsto v](\ctolow{ss'})$.

End of case.

Case Writebuf: on case

$(H, \fplug{LE}{\elet{\_}{\ewritebuf{(b,n,[])}{n'}{lv}}{le}})\step_{\symwrite\;(b,n+n',[])}(H[(b,n+n',[])\mapsto lv], \fplug{LE}{le})$ and $(b,n+n',[])\in H$.

Appealing to Lemma <ref>, we have $ss=((b,n,[])[n']=v;ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$.

Pick $C'$ to be $(S', V, ss')$ where $\symset(S, (b,n,[]), v) = S'$.

We know $C\step^+_{\symwrite\;(b,n+n',[])}C'.$

It suffices to show that $(H[(b,n+n',[])\mapsto lv], \fplug{LE}{le})\;R\;(S', V, ss')$, which is true.

End of case.

Case Writestruct: on case

$(H, \fplug{LE}{\elet{\_}{\ewritestruct{(b,n,\ls{fd})}{lv}}{le}})\step_{\symwrite\;(b,n,\ls{fd})}(H[(b,n,\ls{fd})\mapsto lv], \fplug{LE}{le})$ and $(b,n,\ls{fd})\in H$.

Appealing to Lemma <ref>, we have $ss=(\ewrite{(b,n,\ls{fd})}{v};ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$.

Pick $C'$ to be $(S', V, ss')$ where $\symset(S, (b,n,\ls{fd}), v) = S'$.

We know $C\step^+_{\symwrite\;(b,n,\ls{fd})}C'.$

It suffices to show that $(H[(b,n,\ls{fd})\mapsto lv], \fplug{LE}{le})\;R\;(S', V, ss')$, which is true.

End of case.

Case Subbuf: on case $(H, \fplug{LE}{\esubbuf{(b,n,[])}{n'}})\step(H, \fplug{LE}{(b,n+n',[])})$.

Pick $C'$ to be $(S, V, ss)$.

Because $(H, \fplug{LE}{\esubbuf{(b,n,[])}{n'}})\;R\;C'$ with some $m$, it must be the case that $m\geq 1$ and $(H, \fplug{LE}{(b,n+n',[])})\;R\;C'$ with $m-1$.

End of case.

Case Structfield: on case $(H, \fplug{LE}{\estructfield{(b,n,\ls{fd})}{fd'}})\step(H, \fplug{LE}{(b,n,(\ls{fd}; fd'))})$.

Pick $C'$ to be $(S, V, ss)$.

Because $(H, \fplug{LE}{\estructfield{(b,n,\ls{fd})}{fd'}})\;R\;C'$ with some $m$, it must be the case that $m\geq 1$ and $(H, \fplug{LE}{(b,n,(\ls{fd};fd'))})\;R\;C'$ with $m-1$.

End of case.

Case IfTrue: on case $(H, \fplug{LE}{\eif{n}{le_1}{le_2}})\step_\brt (H, \fplug{LE}{le_1})$ and $n\not=0$.

Appealing to Lemma <ref>, we have $ss=\eif{e}{ss_1}{ss_2};ss'$ and $\eval{e}{(p,V)}=n$ and $le_i=V(\ctolow{ss_i})$ ($i=1,2$) and $LE=\unravel(S, V(\ctolowE{(\symhole;ss')}))$.

Pick $C'$ to be $(S, V, ss_1;ss')$.

We know $C\step^+_\brt C'.$

It suffices to show that $(H, \fplug{LE}{le_1})\;R\;(S, V, ss_1;ss')$, which is true.

End of case.

Case IfFalse: on case $(H, \fplug{LE}{\eif{n}{le_1}{le_2}})\step_\brf (H, \fplug{LE}{le_2})$ and $n=0$.

Similar to previous case.

End of case.

Case Proj: on case $(H, \fplug{LE}{\{\ls{fd=lv}\}.fd'})\step(H, \fplug{LE}{lv'})$ and $\{\ls{fd=lv}\}(fd')=lv'$.

Pick $C'$ to be $(S, V, ss)$.

Because $(H, \fplug{LE}{\{\ls{fd=lv}\}.fd'})\;R\;C'$ with some $m$, it must be the case that $m\geq 1$ and $(H, \fplug{LE}{lv'})\;R\;C'$ with $m-1$.

End of case.

Case Pop: on case $(H;h, \fplug{LE}{\epop\;lv})\step(H, \fplug{LE}{lv})$.

Apply Lemma <ref>.

In the first case, from $LE=\unravel(S', V'(\ctolowE{\symhole;ss'}))$ we know $LE=(\elet{\_}{\symhole}{le})$ and $le=\unravel(S',V'(ss'))$.

pick $C'$ to be $(S',V',ss')$ and $(H'', le'')$ to be $(H, le)$.

Obviously $(H, \fplug{LE}{lv})\step^*(H, le)$. It suffices to show that $(H,le)\;R\;(S',V',ss')$, which is true.

In the second case, pick $C'$ to be $(S',V',\fplug{E}{v})$ and $(H'', le'')$ to be $(H, \fplug{LE}{lv})$.

To suffices to show $(H, \fplug{LE}{lv})\;R\;(S', V', \fplug{E}{v})$, which follows from $LE=\unravel(S',V'(\ctolowE{E}))$.

For Condition 3(b), because and 's values are almost the same (except that locations have a field-path component), every value has an obvious corresponding value, so condition 3(b) is trivially true.

For all $p$ and $ss$, transition system $\sys_{\cstar}(p, ss)$ is deterministic, modulo renaming of block identifiers.

For all $lp$ and $le$, transition system $\sys_{\lamstar}(lp, le)$ is deterministic, modulo renaming of block identifiers.

For all program $lp$, closed expression $le$ and closing substitution $V$, if $\lowtocd{lp}=p$ and $\lowtoc{le}=ss$, then $([],V(le))\;R_{p,lp}\;([],V,ss)$.

Unfold $R$'s definition, it suffices to show:

$([], V(le))\step^*([], V(\ctolow{(\normal{\lowtoc{le}}{(p, \{\})})}))$.

If $H=\mem(S)$ and $le=\unravel(S, V(\ctolow{ss}))$ and $\normal{ss}{(p,V)}=ss'$, then $(H, le)\step^*(H, \unravel(S, V(\ctolow{ss'})))$.

If $(H, \fplug{LE}{\elet{x:t}{lv}{le}})\;R\;(S, V, ss)$, then either $ss=(t\;x=e;ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$, where $v\defeq\eval{e}{(p,V)}$ or $S=S';(\None, V', t\;x=\symhole;ss')$ and $ss=\ereturn{v}$ and $le=V'(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S', \symhole)$.

If $(H, \fplug{LE}{\elet{\_}{lv}{le}})\;R\;(S, V, ss)$, then either $ss=(e;ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$, where $v\defeq\eval{e}{(p,V)}$ or $S=S';(\None, V', \symhole;ss')$ and $ss=\ereturn{v}$ and $le=V'(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S', \symhole)$.

If $(H;h, \fplug{LE}{\elet{x}{\enewbuf{n}{(lv:t)}}{le}})\;R\;(S, V, ss)$, then $ss=(\earray{t}{x}{n};\memset{x}{n}{v};ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$ and $S=S';(M, V', E)$.

If $(H;h, \fplug{LE}{\elet{x}{\enewstruct{(lv:t)}}{le}})\;R\;(S, V, ss)$, then $ss=(\earray{t}{x}{1};\memset{x}{1}{v};ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$ and $S=S';(M, V', E)$.

$(H;h, \fplug{LE}{\elet{x:t}{\ereadbuf{(b,n,[])}{n'}}{le}})\;R\;(S, V, ss)$, then $ss=(t\;x=(b,n,[])[n'];ss')$ and $le=V(\ctolow{ss'})$ and $LE=\unravel(S, \symhole)$.

$(H;h, \fplug{LE}{\elet{x:t}{\ereadstruct{(b,n,\ls{fd})}}{le}})\;R\;(S, V, ss)$, then $ss=(t\;x=\eread{(b,n,\ls{fd})};ss')$ and $le=V(\ctolow{ss'})$ and $LE=\unravel(S, \symhole)$.

$(H;h, \fplug{LE}{\elet{\_}{\ewritebuf{(b,n,[])}{n'}{lv}}{le}})\;R\;(S, V, ss)$, then $ss=((b,n,[])[n']=v;ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$.

$(H;h, \fplug{LE}{\elet{\_}{\ewritestruct{(b,n,\ls{fd})}{lv}}{le}})\;R\;(S, V, ss)$, then $ss=(\ewrite{(b,n,\ls{fd})}{v};ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$.

If $(H, \fplug{LE}{\elet{x:t}{f\;lv}{le}})\;R\;(S, V, ss)$, then $ss=(t\;x=f(v);ss')$ and $le=V(\ctolow{ss'})$ and $lv=\ctolowe{v}$ and $LE=\unravel(S, \symhole)$.

If $(H, \fplug{LE}{\withframe\;le})\;R\;(S, V, ss)$, then $ss=\{ss_1\};ss_2$ and $le=V(\ctolow{ss_1})$ and $LE=\unravel(S, V(\ctolowE{(\symhole;ss_2)}))$.

If $(H, \fplug{LE}{\eif{n}{le_1}{le_2}})\;R\;(S, V, ss)$, then $ss=\eif{e}{ss_1}{ss_2};ss'$ and $\eval{e}{(p,V)}=n$ and $le_i=V(\ctolow{ss_i})$ ($i=1,2$) and $LE=\unravel(S, V(\ctolowE{(\symhole;ss')}))$.

If $(H;h, \fplug{LE}{\epop\;lv})\;R\;(S, V, ss)$, then either $ss=e$ and $\eval{e}{(p,V)}=v$ and $\ctolowe{v}=lv$ and $S=S';(M, V', \symhole;ss')$ and $LE=\unravel(S', V'(\ctolowE{\symhole;ss'}))$, or $ss=\ereturn{e}$ and $\eval{e}{(p,V)}=v$ and $\ctolowe{v}=lv$ and $S=S';(M,V',E)$ and $LE=\unravel(S',V'(\ctolowE{E}))$.

If $\lowtoc{le}=ss;e$, then $\ctolow{(ss;\ereturn\;e)}=le$.

§ FROM TO COMPCERT C AND BEYOND

To further back our claim that KreMLin offers a practical yet
trustworthy way to preserve security properties of programs down to
the executable code, we have to demonstrate that security guarantees
can be propagated from down to assembly.

Our idea here is to use the CompCert verified C compiler
<cit.>. CompCert formally proves the
preservation of functional correctness guarantees from C down to
assembly code (for x86, PowerPC and ARM platforms.)

§.§ Side channels and verified compilation

Regarding side-channel security guarantees, one has to be careful
because the compiler may very well introduce additional memory
accesses due to register allocation. Thus, although we prove the
preservation of the sequences of memory accesses from to , as
well as the preservation of branchings in the program counter model,
it may very well be the case that compiled code accesses many more
spilling locations in one secret-controlled branch (PW: but
there is no secret-controlled branch (TR: you are right in the source,
but experiments should be performed to show that the compiler does not
introduce any)) than in another, yielding potentially different cache
behaviors, which an attacker could exploit to deduce some secrets.

To mitigate this issue, there are several solutions. One by Barthe et
al. <cit.>, consists in performing a static analysis on
the Mach code (after most CompCert passes, but just before assembly
generation), with alias analysis to determine the sequence of memory
accesses and prove that they do not change across different
secret-controlled branches. This way, the security property is
guaranteed, actually turning CompCert into a certifying compiler to
this respect. That work has been extended to a full-scale LLVM static
analysis in <cit.>.

Another solution (not explored yet, due to lack of time) would be to
directly make all intermediate passes annotate the generated code with
hints about memory accesses they are adding, and use those annotations
to introduce a pass (just before assembly generation) adding unused
spilling memory accesses to guarantee that those locations are always
accessed across all secret-controlled branches. This way, we could
actually avoid performing a full-scale static analysis on the code, by
distinguishing between source-level memory accesses to stack-allocated
variables (which are exactly preserved) and additional spilling memory
accesses. In practice, this approach could avoid the risk of static
analysis failures.

We claim that the latter approach (although not modular, since it
would require pervasive modifications across all passes of CompCert)
is feasible because all additional memory accesses introduced by
CompCert are at constant offsets within the stack block of the
function; and we claim that those memory accesses are not leaked
through function calls, neither directly nor by pointer arithmetics
(if they were, then they would correspond to no valid operation in the
source program.)

However, generating Clight code (as we describe below) and then using
Barthe et al.'s instrumented CompCert <cit.> or Almeida
et al.'s instrumented LLVM <cit.> is already
practical enough and, at least at the metatheoretical level, already
gives enough guarantees about the preservation of side-channel
security properties.

§.§ Reminder: CompCert Clight

CompCert Clight <cit.> is a subset of C with no
side effects in expressions, and actual byte-level representation of
values. Syntax in Figure <ref>. Semantics
definitions in Figure <ref>. Evaluation of
expressions in Figure <ref>. Small-step semantics in
Figure <ref>.

The semantics of a Clight program is given by the return value of its
$\kw{main}$ function called with no arguments.[CompCert does
not support semantics preservation with system arguments.]  Thus,
given a Clight program $p$, the initial configuration of a CompCert
Clight transition from $p$ is $(\{ \}, [], [], [], \kw{int} ~ r =
\kw{main}())$, and a configuration is final with return value $i$ if,
and only if, it is of the form $(\{ \}, \_, \_V, \_, [])$ with $\_V(r)
= i$.

$p ::= $         program

$\ls d$                          series of declarations

$d ::= $         declaration

$\ecfun fxtt{\ls{ad},ss}$                    top-level function

with stack-allocated local variables $\ls{ad}$

${ad}$     top-level value

${ad} ::= $         array declaration

$\earray{t}{x}{n}{}$                   uninitialized global variable

$ss ::= $         statement lists

$s ::= $         statements

$\_x = e$     assign rvalue to a non-stack-allocated local variable

$\_x = {\eapply fe}$                      application

$\clread{\_x}{t}{e}$                   memory read from lvalue

$\clwrite tee$                   memory write rvalue to lvalue

$\clannot(\symread,t,e)$     annotation to produce read event

$\clannot(\symwrite,t,e)$     annotation to produce write event

$\eif{e}{ss}{ss}$     conditional

$\{\stmts\}$      block

e     return

$e ::= $         expressions

$n$        integer constant (rvalue)

$x$                               stack-allocated variable (lvalue)

$\_x$                               non-stack-allocated variable (rvalue)

$e_1+_te_2$                            pointer add (rvalue, $e_1$ is a rvalue pointer to a value of type $t$ and $e_2$ is a rvalue $\kw{int}$)

$e._tfd$     struct field projection (lvalue, $e$ lvalue)

$\claddr{e}$     address of a lvalue (rvalue, $e$ lvalue)

$\clderef{e}$     pointer dereference (lvalue, $e$ rvalue)

Clight Syntax

Just like C, there are two ways to evaluate Clight expressions: in
lvalue position or in rvalue position. Roughly speaking, in an
expression assignment $\clwrite t{e_l}{e_r}$, expression $e_l$ is said to be at
lvalue position and thus must evaluate into a memory location, whereas
$e_r$ is said to be at rvalue position and evaluates into a value
(integer or pointer to memory location). The operation $\claddr{e}$
takes an lvalue $e$ and transforms it into a rvalue, namely the
pointer to the memory location $e$ designates as an
lvalue. Conversely, $\clderef{e}$ takes an rvalue $e$, which must
evaluate to a pointer, and turns it into the corresponding memory
location as an lvalue.

Memory accesses in the trace
To account for memory accesses in the trace, we make each statement
perform at most one memory access in our generated Clight code. Then,
we prepend each such memory access statement with a built-in
call, a no-op annotation $\clannot(\mathit{ev},t,e)$ whose
semantics is merely to produce the corresponding memory access event
$\mathit{ev}(b, n)$ in the trace, where $e$ evaluates to the pointer
to offset $n$ within block $e$.

$v ::= $         values

$n$        integer constant

$(b, n)$                            memory location

$\clunkn{}$                            defined but unknown value

${vf} ::= $         value fragments

$n$        byte constant

$((b,n), n')$     $n'$-th byte of pointer value $(b,n)$

$\clunkn{}$                            defined but unknown value fragment

$V ::=$         stack-allocated variable assignments

$x\sympartial b$     map from variable to memory block identifier

$\_V ::=$         non-stack-allocated variable assignments

$\_x\sympartial v$     map from variable to value

$E ::=$         evaluation ctx (plug expr to get stmts)

$\symhole; ss$     discard returned value

$\_x=\symhole; ss$     receive returned value

$F ::=$         frames

$(V, \_V, E)$     stack frame

$S ::=$         stack

$\ls{F}$     list of frames

$M ::=$         memory

$(b, n) \sympartial vf$     map from block id and offset to value fragment

$C ::=$         configuration

$(S, V, \_V, M, ss)$

Clight Semantics Definitions

$\cllv{e}{(p, V, \_V)}=(b,n)$   and   $\clrv{e}{(p, V, \_V)}=v$

* [Right=Var]

V(x) = b

x(p,V, _V)=(b, 0)

* [Right=GVar]

x ∉V

p(x) = b

x(p,V, _V)=(b, 0)

* [Right=PtrFd]

e(p,V, _V) = (b, n)

e._tfd(p,V, _V)=(b, n + (t, fd))

* [Right=PtrDeref]

e(p,V,_V) = (b,n)

e(p,V,_V) = (b,n)

* [Right=RVar]

_V(_x) = v

* [Right=PtrAdd]

e_1(p,V,_V) = (b, n)

e_2(p,V,_V) = n'

e_1+e_2(p,V)=(b, n+n')

* [Right=AddrOf]

e(p,V,_V)= (b, n)

e(p,V,_V)= (b,n)

Clight Expression Evaluation

$p \vdash C\step_\olabel C'$

* [Right=Read]

e(p, V, _V) = (b, n)

(M, (b, n), sizeof(t)) = v

p ⊢(S, V, _V, M, _xte; ss) (S, V, _V[_x↦v], M, ss)

* [Right=Write]

e_1(p, V, _V) = (b, n)

e_2(p, V, _V) = v

(M, (b, n), sizeof(t), v) = S'

p ⊢(S, V, _V, M, te_1e_2; ss) (S', V, _V, M, ss)

* [Right=Annot]

e(p, V, _V) = (b, n)

p ⊢(S, V, _V, M, 𝑒𝑣, e; ss) _𝑒𝑣 (b,n)(S, V, _V, M, SS)

* [Right=Ret]

p ⊢(S;(V', _V',E), V, M,  e; ss) (S, V', _V', M, Ev)

* [Right=Call]

p(f)=_yt_1t_2ads; ss_1

(ads, , M) = (V', M')

p ⊢(S, V, _V, M, _x=f e; ss) (S;(V, _V, _x=;ss), V', {}[_y↦v], M', ss_1)

* [Right=AllocNil]

([], V, M) = (V, M)

* [Right=AllocCons]

(M,n ×sizeof(t)) = (b,M_1)

(ads, V[x ↦(b,0)], M_1) = (V', M')

((txn; ads), V, M) = (V', M')

* [Right=Expr]

e(p,V,_V) = v

p ⊢(S, V, _V, M, e; ss) (S, V, _V, M, ss)

* [Right=Empty]

p ⊢(S, V, _V, M, []) (S, V, _V, M,  )

* [Right=Block]

p ⊢(S, V, _V, M, {ss_1};ss_2) (S; V, _V, M, ss_1; ss_2)

* [Right=IfT]

e(p, V, _V) = v

v ≠ 0

v ≠

p ⊢(S, V, _V, M, ess_1ss_2;ss) _(S, V, ss_1;ss)

* [Right=IfF]

e(p, V, _V) = 0

p ⊢(S, V, _V, M, ess_1ss_2;ss) _(S, V, _V, M, ss_2;ss)

Clight Configuration Reduction

The CompCert memory model
The semantics of CompCert Clight statements depends on the CompCert
memory model <cit.>. Here we need three
operations: $\symget$, $\symset$ and $\clalloc$, whose description
follows.[In the current version of CompCert and its memory
model <cit.>, each memory location is
equipped with a permission to more faithfully model the fact
that the memory locations of a local variable cannot be read or
coincidentally reused in a Clight program after exiting the scope of
the variable. To this end, thanks to this permission model, the
CompCert memory model also defines a $\kw{free}$ operation which
invalidates memory accesses while preventing from reusing the memory
block for further allocations; although we do not describe it here,
CompCert Clight actually uses this operator to free all local
variables upon function exit. Thus, it is also necessary to amend
the semantics of in a similar way.]

$\symget(M, (b, n), n')$ reads $n'$ bytes from memory $M$ at offset
$n$ within block $b$, and decodes the obtained byte fragments into a
value. It fails if not all locations from $(b, n)$ to $(b, n'-1)$ are
defined. It returns $\clunkn$ if all locations are defined but the
decoding fails.

$\symset(M, (b, n), n', v)$ writes $n'$ bytes from memory $M$ at
offset $n$ within block $b$ corresponding to encoding value $v$ into
$n'$ value fragments. It fails if not all locations from $(b, n)$ to
$(b, n'-1)$ are defined.

$\clalloc{}(M, n)$ returns a pair $(b, M')$ where $b \not\in M$ is a
fresh block identifier and all locations from $(b,0)$ to $(b,n-1)$ in
$M'$ contain $\clunkn$.

§.§ Issues

Local structures

The main difference between and Clight is that allows structures
as values. Although converting a value into a Clight value is no
problem in terms of memory representation (since the layout of Clight
structures[which can be chosen when configuring CompCert with
a suitable platform] is already formalized in CompCert with basic
proofs such as the fact that two distinct fields of a structure
designate disjoint sets of memory locations), local structures cause
issues in terms of managing memory accesses (due to our desire for
noninterference in terms of memory accesses), as we describe in
Section <ref>.

Stack-allocated local variables

Another difference between and Clight is that, whereas allows
the user to stack-allocate local variables on the fly, Clight mandates
all local variables of a function to be hoisted to the beginning of
the function (in fact, the list of all stack-allocated variables of a
function is actually part of the function definition), and so they are
allocated all at once when entering the function.

Hoisting local variables is not supported in the verified part of

In practice, when compiling a piece of C code with CompCert,
an unverified elaboration pass performs this operation.[See
<cit.>, section “Architecture of the compiler”. By
reading the source code of the unverified elaborator in
, we figured out the hoisting strategy
adopted by CompCert 2.7.1, as we describe it here.] This unverified
phase of CompCert hoists all local variables of a function, without
trying to merge two local variables belonging to disjoint C code
blocks, contrary to GNU GCC
[If we were to follow the GNU GCC hoisting strategy, then we
would have to think about how to merge two variables of different
types. However, type annotations are present in CompCert until
Clight, and CompCert then erases those type annotations in a pass
from Clight to C$\sharp$minor, which is very similar to Clight
except that it no longer has any C-style types (structs, unions,
etc.) so that a stack-allocated variable only designates a memory
block of some constant size in bytes. So, in that case, I claim that
hoisting could and should be done at the level of C$\sharp$minor,
rather than in Clight or KreMLin. However, this would require
modifying CompCert Clight so that local variable allocation sites
would be attached to code blocks rather than functions.]  Regardless
of the hoisting strategy, verifying this pass may be an interesting
problem within CompCert itself.

Instead of trying to prove hoisting on Clight or any language of
CompCert, we could perform this phase at the level. We propose a
solution in Section <ref>.

Consider the following example, for a given conditional expression

\[
\eifthenelse
{\earray{\kint}{x}{1}{18}; }
{\{ \earray{\kword}{x}{1}{42}; \ewrite{x+0}{1729} \} }
\]

After hoisting, following the same strategy as the corresponding
unverified pass of CompCert, code will look like this:

\[
\earray{\kint}{x_1}{1}{};
\earray{\kword}{x_2}{1}{};
\]

\[
\eifthenelse
{\ewrite{x_1+0}{18}; }
{\{ \ewrite{x_2+0}{42}; \ewrite{x_2+0}{1729} \} }
\]

This example shows the following issue:
when producing the trace, the
memory blocks corresponding to the accessed memory location will
differ between the non-hoisted and the hoisted code. Indeed, in
the non-hoisted code, only one variable $x$ is allocated in the
stack, whereas in the hoisted code, two variables $x_1$ and $x_2$
corresponding to both branches will be allocated anyway, regardless
of the fact that only one branch is executed. Thus, in the code
before hoisting, allocating $x$ will create, say, block 1, whereas
after hoisting, two variables will be allocated, $x_1$ at block 1,
and $x_2$ at block 2. Thus, the statement $\ewrite{x+0}{1729}$ in
the code before hoisting will produce $\symread\;(1,0,[])$ on the
trace, whereas its corresponding translation after hoisting,
$\ewrite{x_2+0}{1729}$, will produce

Anyway, a similar problem of discrepancy of traces of memory accesses
will also exist in CompCert passes after Clight, this time because the
structure of the stack will change across intermediate languages of
CompCert (in particular, at some point, all stack-allocated variables
of one function call will be merged into one single stack block for
the entire stack frame.) Thus, so far, CompCert will very well
preserve functional correctness down to the assembly, but will require
more work to preserve security guarantees beyond Clight, unless
we instrument it as described before.

One quick solution to ensure that those event traces are exactly
preserved, is to replace the actual pointer $(b, n,
\mathit{fd})$ on $\symread$ and $\symwrite$ events with $(f, i, x, n,
\mathit{fd})$ where $f$ is the name of the function, $i$ is the
recursion depth of the function (which would be maintained as a global
variable, increased whenever entering the function, and decreased
whenever exiting) and $x$ is the local variable being accessed. (In
concurrent contexts, one could add a parameter $\theta$ recording the
identifier of the current thread within which $f$ is run, and so the
global variable maintaining recursion depth would become an array
indexed by thread identifiers.)

[Catalin: Isn't this much weakening the attacker model though?
And how does this new model apply to machine code?]

[Tahina: This abstract trace model is only for the purpose of proofs
of memory transformations, beginning with the to Clight
proof. This model also applies to C$\sharp$minor (exact
preservation, the only difference being the erasure of C-style type
information), and it can also be applied to Cminor (where all local
variables are merged into one single stack frame) when translating
from C$\sharp$minor. Then, from Cminor on, it becomes useless. In
fact, from Cminor on, the local variable region becomes contiguous
for a given function call, and (with the notable exception of in the
function inlining pass, which may very well merge several stack
frames of inlined callees into one single one. Anyway, function
inlining requires special treatment.) there are no pointer
transformations until the time spilling locations are introduced in
memory when generating assembly code.

Once again, the ultimate trace model that we want for our final
side-effect security correctness statement will definitely be the
one with concrete pointer values, and abstract pointer values are
only for the purpose of compiler verification.]

Finally, we adopted this solution as we describe in
Section <ref>, and we heavily use it to prove the
correctness of hoisting within in Section <ref>.

§.§ Summary: from to Clight

Given a program $p$ and an entrypoint $ss$, we are going to
transform it into a CompCert Clight program in such a way that both
functional correctness and noninterference are preserved.

This will not necessarily mean that traces are exactly preserved
between and Clight, due to the memory representation discrepancy
described before. Instead, by functional correctness, we mean that a
safe program is turned into a safe Clight program, and for such
safe programs, termination, I/O events and return value are preserved;
and by noninterference, we mean that if two executions with different
secrets produce identical (whole) traces in , then they will also
produce identical traces in CompCert Clight (although the trace may
have changed between and Clight.)

* In section <ref>, we transform a programs into a program with unambiguous variable names, and we take
advantage of such a syntactic property by enriching the
configuration of with more information regarding variable names,
thus yielding the 2 language.

* In section <ref>, we execute the obtained 2
program with a different, more abstract, trace model, as proposed
above. This is not a program transformation, but only a
reinterpretation of the same program with a different operational
semantics, which we call 3.

* In section <ref>, we transform the 3 program into
a 3 program where all local arrays are hoisted from block-scope to
function-scope. The abstract trace model critically helps in the
success of this proof where memory state representations need to

* In section <ref>, we transform the obtained
3 program into a 3 program where functions returning structures
are replaced with functions taking a pointer to the return location
as additional argument. Thus, we need to account for an additional
memory access, which we do through the 4 intermediate semantics,
another reinterpretation of the source 3 program producing new
events at functions returning structures. Then, our reinterpreted
4 program is translated back to 3 with those additional memory
accesses made explicit.

* In section <ref>, we reinterpret our obtained
3 program with a different event model where memory access events
of structure type are replaced by the sequences of memory access
events of all their non-structure fields. We call this new language

* In section <ref>, we transform our 5
program back into 3 by erasing all local structures that are not
local arrays, replacing them with their individual non-structure
fields. Thus, the more “elementary” memory accesses introduced in
the 3 to 5 reinterpretation are made concrete.

* We then reinterpret the obtained 3 program back into 2 as
described in <ref>, reverting to the traces
with concrete memory locations at events, thus accounting for all
memory accesses.

* Finally, in section <ref>, we compile the
obtained 2 program, now in the desired form, into CompCert Clight.

§.§ Normalized event traces in

As described above, traces where memory locations explicitly appear
are notoriously hard to reason about in terms of semantics
preservation for verified compilation. Thus, it becomes desirable to
find a common representation of traces that can be preserved between
different memory layouts across different intermediate languages.

In particular here, we would like to replace concrete pointers into
abstract pointers representing the local variable being modified in a
given nested function call.

§.§.§ Disambiguation of variable names

To this end, we first need to disambiguate the names of the local
variables of a function:

We say that a list of instructions has unambiguous local
variables if, and only if, it contains no two distinct array
declarations with the same variable name, and does not contain both
an array declaration and a non-array declaration with the same
variable name.

We say that a program has unambiguous local variables if, and
only if, for each of its functions, its body has unambiguous local

We say that a transition system $\sys(p, V, ss)$ has unambiguous
local variables if, and only if, $p$ has unambiguous local
variables, $ss$ has unambiguous local variables, and $V$ does not
define any variable with the same name as an array declared in $ss$.

There exists a transformation $T$ on lists of instructions (extended
to programs by morphism) such that, for any program $p$, and for
any list of instructions $ss$,

for any variable mapping $V'$
such that $\sys(T(p),V',T(ss))$ has unambiguous local variables,
there exists a variable mapping $V$
such that $\sys(p,V,ss)$ and $\sys(T(p),V',T(ss))$ have the same
execution traces.

The noninterference property can be proven to be stable by such

Let $p$ be a program and $ss$ be a list of instructions. Assume
that for any $V_1, V_2$ such that $\sys(p, V_1, ss)$ and $\sys(p,
V_2, ss)$ are both safe, then they have the same execution

Then, for any $V_1', V_2'$ such that $\sys(T(p), V_1', T(ss))$ and
$\sys(T(p), V_2', T(ss))$ are both safe, they have the same
execution traces.

By Lemma <ref>, there is some $V_1$ such that
$\sys(p, V_1, ss)$ and $\sys(T(p), V_1', T(ss))$ have the same
execution traces, thus in particular, $\sys(p, V_1, ss)$ is
safe. Same for some $V_2$. By hypothesis, $\sys(p, V_1, ss)$ and
$\sys(p, V_2, ss)$ have the same execution traces, thus the result
follows by transitivity of equality.

Thus, we can now restrict our study to programs whose functions
have no two distinct array declarations with the same variable names.

Let us first enrich the configuration $(S, V, ss)$ of small-step
semantics with additional information recording the current function
$f$ being executed (or maybe $\None$) and the set $A$ of the variable
names of local arrays currently declared in the scope. Thus, a stack frame $(\None, V, E)$ becomes $(\None, V, E, f, A)$ where $f$ is
the caller, a block frame $(M, V, E)$ becomes $(M, V, E, f, A)$ where
$f$ is the enclosing function of the block, and the configuration $(S,
V, ss)$ becomes $(S, V, ss, f, A)$ where $f$ is the current function
(with the frames of $S$ changed accordingly.) Let us then change some
rules accordingly as described in Fig. <ref>, leaving
other rules unchanged except with the corresponding $f$ and $A$
components preserved.

* [Right=$\text{ArrDecl}_2$]

S = S'; (M, V, E, f', A')

p ⊢(S, V, t x[n]=e; ss, f, A) (S';(M[b↦v^n], V, E, f', A'), V[x↦(b, 0, [])], ss, f, A∪{x})

* [Right=$\text{Ret}_2$]

p ⊢(S;(, V',E, f', A'), V,  e; ss, f, A) (S, V', Ev, f', A')

* [Right=$\text{Call}_2$]

p ⊢(S, V, t x=f e; ss, f', A') (S;(, V, t x=;ss, f', A'), {}[y↦v], ss_1, f, {})

2 Amended Configuration Reduction

Let us call 2 the obtained language where the initial state of the
transition system $\sys(p, V, ss)$ shall now be $([], V, ss, \None,

Then, it is easy to prove the following:

If $\sys(p, V, ss)$ has unambiguous local variables and is safe in
, then it has the same execution traces in as in 2 (and in
particular, it is also safe in 2.)

Thus, both functional correctness and noninterference are
preserved from to 2.

Lock-step bisimulation where the common parts of the configurations
(besides the 2-specific $f, A$ parts) are equal between and

Then, we can prove an invariant over the small-step execution of a 2

Let $p$ be a 2 program and $V$ a variable environment such that
$\sys(p,V,ss)$ has unambiguous local variables.

Let $n \in \mathbb N$. Then, for any 2 configuration $(S, V', ss',
f, A)$ obtained after $n$ 2 steps from $(\{\}, V, ss, \None, \{\})$,
the following invariants hold:

* for any variable or array declaration $x$ in $ss'$, it does not
appear in $A_1$

* any variable name in $A$ or in an array declaration of $ss'$ is
in an array declaration of $ss$ (if $f = \None$) or the body of $f$

* for each frame of $S$ of the form $(\_, \_, E, f'', A'')$, then
any variable name or array declaration in $E$ does not appear in
$A''$, and any variable name in $A''$ or in an array declaration of
$E$ is in an array declaration in $ss$ (if $f'' = \None$) or the
body of $f''$ (otherwise.)

*  if $S = S'; (M, \_, \_,
f', A')$ with $M \not= \None$, then $f' = f$, $A' \subseteq A$ and
for all block identifiers $b$ defined in $M$, there exists a unique
variable $x \in A$ such that $V'(x) = b$

*  for any two consecutive
frames $(M, \_, \_, f_1, A_1)$ just below $(\_, V_2, \_, f_2, A_2)$
with $M \not= \None$, then $f_1 = f_2$ and $A_1 \subseteq A_2$ and
$V_1(x) = V_2(x)$ for all variables $x \in A_1$, and for all block
identifiers $b$ defined in $M$, there exists a unique variable $x
\in A_2$ such that $V_2(x) = b$

*  for any two different
frames of $S$ of the form $(M_1, \_, \_, \_, \_)$ and $(M_2, \_, \_,
\_, \_)$ with $M_1 \not= \None$ and $M_2 \not= \None$, the sets of
block identifiers of $M_1$ and $M_2$ are disjoint

By induction on $n$ and case analysis on $\step$.

Then, we can prove a strong invariant between two executions of
the same 2 program with different secrets. This strong invariant
will serve as a preparation towards changing the event traces of 2.

Let $p$ be a 2 program, and $V_1, V_2$ be two variable environments
such that $\sys(p, V_1, ss)$ and $\sys(p, V_2, ss)$ have unambiguous
local variables, are both safe and produce the same traces in 2.

Let $n \in \mathbb N$. Then, for any two 2 configurations $(S_1,
V_1', ss_1, f_1, A_1)$ and $(S_2, V_2', ss_2, f_2, A_2)$ obtained
after $n$ 2 execution steps, the following invariants hold:

* $ss_1 = ss_2$

* $S_1, S_2$ have the same length

* $f_1 = f_2$

* $A_1 = A_2$

* $V_1(x) = V_2(x)$ for each $x \in A_1$

* for each $i$, if the $i$-th frames of $S_1, S_2$ are $(M_1,
V_1'', E_1, f_1'', A_1'')$ and $(M_2, V_2'', E_2, f_2'', A_2'')$,
then $E_1 = E_2$, $f_1'' = f_2''$ and $A_1'' = A_2''$ and $V_1''(x)
= V_2''(x)$ for any $x \in A_1''$. Moreover, $M_1 = \None$ if and
only if $M_2 = \None$, and if $M_1 \not= \None$, then $M_1$ and
$M_2$ have the same block domain.

Thus, the $n+1$-th step in both executions applies the same 2 rule.

By induction on $n$ and case analysis on $\step$, also using the
invariant of Lemma <ref>. In particular the
equality of codes is a consequence of the fact that there are no
function pointers in .[If we were to allow function
pointers in , then we would have to add function call/return
events into the trace beforehand, and assume that traces with
those events are equal before renaming = prove that they are equal
on the program as well. This might have consequences in the
proof of function inlining in the -to-translation.] Then,
both executions apply the same 2 rules since 2 small-step rules
are actually syntax-directed.

§.§.§ Normalized traces

Now, consider an execution of 2 from some initial state. In fact,
for any block identifier $b$ defined in $S$, it is easy to prove that
it actually corresponds to some variable defined in the scope. The
corresponding VarOfBlock algorithm is shown in
Figure <ref>.  FIXME: global
variables[Global variables (top-level values) are not
allocated anywhere in the memory of a program, so cannot
access them. can only access the local variables of the
entrypoint list of statements, which is not part of the program.]

Algorithm: VarOfBlock

* 2 configuration $(S, V, \_, \_, A)$ such that the invariants
of Lemma <ref> hold

* Memory block $b$ defined in $S$

Output: function, recursion depth and local variable
corresponding to the memory block

Let $S = S_1 ; (M, \_, \_, f, \_) ; S_2$ such that $b$ defined in
$M$. (Such a decomposition exists and is unique because of
Invariant <ref>. $f$ may be $\None$.)

Let $n$ be the number of frames in $S_1$ of the form $(\None, \_,
\_, f', \_)$ with $f' = f$.

Let $V'$ and $A'$ such that $S_2 = (\_, V', \_, \_, A) ; \_$, or $V'
= V$ and $A' = A$ if $S_2 = \{\}$.

Let $x$ such that $V'(x) = (b, 0)$ (exists and is unique because of
Invariants <ref>
and <ref>.)

Result: $(f, n, x)$

2: retrieving the local variable corresponding to a
memory block

Then, let 3 be the 2 language where the Read and
Write rules are changed according to
Figure <ref>, with event traces where the actual pointer
is replaced into an abstract pointer obtained using the
VarOfBlock algorithm above.

* [Right=$\text{Read}_3$]

C = (S, V, t x=*[e]; ss, f, A)

e(p, V) = (b, n, fd)

(S, (b, n, fd)) = v

ℓ= VarOfBlock(C, b)

p ⊢C _ (ℓ,n,fd) (S, V[x↦v], ss, f, A)

* [Right=$\text{Write}_3$]

C = (S, V, *e_1=e_2; ss, f, A)

e_1(p, V) = (b, n, fd)

e_2(p, V) = v

(S, (b, n, fd), v) = S'

ℓ= VarOfBlock(C, b)

p ⊢C _ (ℓ,n,fd) (S', V, ss, f, A)

3 Amended Configuration Reduction

If $\sys(p, V, ss)$ has no unambiguous variables, then $\sys(p, V,
ss)$, has the same behaviors in 2 with event traces with
$\symread, \symwrite$ removed, as in 3 with event traces with
$\symread, \symwrite$ removed.

Lock-step bisimulation with equal configurations. Steps
Read and Write need the invariant of
Lemma <ref> on 2 to prove that 3 does not
get stuck (ability to apply VarOfBlock.)

Let $C_1, C_2$ two 2 configurations such that invariants of
Lemma <ref> and
Lemma <ref> hold. Then, for any
block identifiers $b_1, b_2$ such that $\textsc{VarOfBlock}(C_1,
b_1)$ and $\textsc{VarOfBlock}(C_2, b_2)$ are both defined and
equal, then $b_1 = b_2$.

Assume $\textsc{VarOfBlock}(C_1, b_1) = \textsc{VarOfBlock}(C_2,
b_2) = (f, n, x)$. When applying $\textsc{VarOfBlock}$, consider
the frames $F_1, F_2$ holding the memory states defining $b_1,
b_2$. Consider the variable mapping $V'_2$ in the frame just above
$F_2$ (or in $C_2$ if such frame is missing.) Then, it is such that
$V'_2(x) = b_2$.

* If $F_1$ and $F_2$ are at the same level in their respective
stacks, then the variable mapping $V'_1$ in the frame directly
above $F_1$ (or in $C_1$ if such frame is missing) is such that
$V'_1(x) = b_1$, and also $V'_1(x) = V'_2(x)$ by the invariant, so
$b_1 = b_2$.

* Otherwise, without loss of generality (by symmetry), assume
that $F_2$ is strictly above $F_1$ (i.e. $F_2$ is strictly closer
to the top of its own stack than $F_1$ is in its own stack.) Thus,
in the stack of $C_1$, all frames in between $F_1$ and the frame
$F_1''$ corresponding to $F_2$ are of the form $(M', V', \_, f',
\_)$ with $f' = f$ and $M' \not= \None$ (otherwise the functions
and/or recursion depths would be different.) By
invariant <ref> of
Lemma <ref>, it is easy to prove that $V'(x) =
b_1$, and thus also for the variable mapping $V'_1$ in the frame
just above $F_1''$ (or in $C_1$ directly if there is no such
frame.) By invariants of
Lemma <ref>, we have $V'_1(x)
= V'_2(x)$, thus $b_1 = b_2$.

Assume that $\sys(p, V_1, ss)$ and $\sys(p, V_2, ss)$ have no
unambiguous variables. Then, they are both safe in 2 and produce
the same traces in 2, if and only if they are both safe in 3 and
produce the same traces in 3.

Use the invariants of Lemma <ref> and
Lemma <ref>. In fact, the
configurations and steps are the same in 2 as in 3, only the
traces differ between 2 and 3. Read and Write
steps match between 2 and 3 thanks to
Lemma <ref>.

The invariants of Lemma <ref> and
Lemma <ref> also hold in 3.

§.§ Local variable hoisting

On 3, hoisting can be performed, which will modify the structure of
the memory (namely the number of memory blocks allocated), which is
fine thanks to the fact that event traces carry abstract pointer
representations instead of concrete pointer values.

Memory allocator and dangling pointers
However, we have to cope with dangling pointers whose address should
not be reused. Consider the following code:

\[
\begin{array}{l}
\earray{\kint}{x}{1}{18}; \\
\earray{\kint *}{p}{1}{x}; \\
\{ \\
~ \earray{\kint}{y}{1}{42}; \\
~ \ewrite{p}{y}; \\
\} \\
\{ \\
~ \earray{\kint}{z}{1}{1729}; \\
~ \evardecl{\kint *}{q}{\eread{p}}; \\
~ f(q) \\
\} \\
\end{array}
\]

With a careless memory allocator which would reuse the space of $y$
for $z$, the above program would call $f$ not with a dangling pointer
to $y$, but instead with a valid pointer to $z$, which might not be
expected by the programmer. Then, if $f$ uses its argument to access
memory, what should the VarOfBlock algorithm compute? I claim
that such a 3 program generated from a safe program should never
try to access memory through dangling pointers.

As far as I understood, a program obtained from a well-typed program should be safe with any memory allocator, including
with a memory allocator which never reuses previously allocated block
identifiers, as in CompCert.[Formally, a (or )
configuration should be augmented with a state $\Sigma$ so that the
NewBuf rule (or the ArrDecl rule), instead
of picking a block identifier $b$ not in the domain of the memory,
call an allocator $\kw{alloc}$ with two parameters, the domain $D$
of the memory and the state $\Sigma$, and returning the fresh block
$b \not\in D$ and a new state $\Sigma'$ for future
allocations. Then, a CompCert-style allocator would, for instance,
use $\mathbb N$ as the type of block identifiers, as well as for the
type of $\Sigma$, so that if $\kw{alloc}(D, \Sigma) = (b, \Sigma')$,
then it is ensured that $b \not\in D$, $\Sigma \leq b$ and $b <
\Sigma'$. In that case, the domain of the memory being always within
$\Sigma$, could then be easily proven as an invariant of (or
).] In particular, a program safe with such a CompCert-style
allocator will actually never try to access memory through a dangling
pointer to a local variable no longer in scope.

Then, traces with concrete pointer values are preserved from to
2 with the allocator fixed in advance in all of , and
2; and functional correctness and noninterference are also
propagated down to 3 using the same memory allocator.

There should be a way to prove the following:

If a 3 program is safe with a CompCert-style memory allocator,
then it is safe with any memory allocator and the traces (with
abstract pointer representations) are preserved by change of memory

Lock-step simulation where the configurations have the same
structure but a (functional but not necessarily injective) renaming
of block identifiers from a CompCert-style allocator to any
allocator is maintained and augmented throughout the execution. In
particular, we have to prove that VarOfBlock is stable
under such renaming.

If so, then for the remainder of this paper, we can consider a
CompCert-style allocator.

For any list of statements $\mathit{ss}$ with unambiguous local
variables, the hoisting operation $\kw{hoist}(\mathit{ss}) =
(\mathit{ads}, \mathit{ss}')$ is so that $\mathit{ads}$ is the list
of all array declarations in $\mathit{ss}$ (regardless of their
enclosing code blocks) and $\mathit{ss}'$ is the list of statements
$\mathit{ss}$ with all array declarations replaced with $()$.

Then, hoisting the local variables in the body $ss$ of a function is
defined as replacing $ss$ with the code block $\{ \mathit{ads};
\mathit{ss}' \} $ where $\kw{hoist}(\mathit{ss}) = (\mathit{ads},
\mathit{ss}')$; and then, hoisting the local variables in a program
$p$, $\kw{hoist}(p)$, is defined as hoisting the local variables in
each of its functions.

Let $C_1, C_2$ be two 3 configurations. Block identifier $b_1$ is
said to correspond to block identifier $b_2$ from $C_1$ to
$C_2$ if, and only if, either $\textsc{VarOfBlock}(C_1, b_1)$ is
undefined, or $\textsc{VarOfBlock}(C_1, b_1)$ is defined and equal
to $\textsc{VarOfBlock}(C_2, b_2)$.

Then, value $v_1$ corresponds to $v_2$ from $C_1$ to $C_2$ if, and
only if, either they are equal integers, or they are pointers $(b_1,
n_1, fd_1)$, $(b_2, n_2, fd_2)$ such that $fd_1 = fd_2$, $n_1 = n_2$
and $b_1$ corresponds to $b_2$ from $C_1$ to $C_2$, or they are
structures with the same field identifiers and, for each field $f$,
the value of the field $f$ in $v_1$ corresponds to the value of the
field $f$ in $v_2$ from $C$ to $C'$.

If $\sys(p, V, ss)$ is safe in 3 with a CompCert-style allocator,
then $\sys(p, V, ss)$ and $\sys(\kw{hoist}(p), V, \kw{hoist}(ss))$
have the same execution traces (and in particular, the latter is
also safe) in 3 using the same CompCert-style allocator.

Forward downward simulation from 3 before to 3 after hoisting,
where one step before corresponds to one step after, except at
function entry where at least two steps are required in the compiled
program (function entry, followed by entering the enclosing block
that was added at function translation, then allocating all local
variables if any), and at function exit, where two steps are
required in the compiled program (exiting the added block before
exiting the function.)

Then, since 3 is deterministic, the forward downward simulation is
flipped into an upward simulation in the flavor of CompCert; thus
preservation of traces.

For the simulation diagram, we combine the invariants of
Lemma <ref> with the following invariant between
configurations $C = (S, V, ss, f, A)$ before hoisting and $C' = (S',
V', ss', f', A')$ after hoisting:

* for all variables $x$ defined in $V$, $V(x)$, if defined,
corresponds to $V'(x)$ from $C$ to $C'$

* $ss'$ is obtained from $ss$ by replacing all array
declarations with $()$

* $f' = f$

* $A \subseteq A'$

* the set of variables declared in $ss$ is included in $A'$

* if a block identifier $b$ corresponds to $b'$ from $C$ to
$C'$, then the value $\symget(S, b, n, fds)$, if defined, corresponds
to $\symget(S', b', n, fd)$ from $C$ to $C'$

Each frame of the form $(\None, V_1, E, f_1, A_1)$ in $S$ is
replaced with two frames in $S'$, namely $(\None, V_1', E, f_1,
A_1') ; (M', V_2', \symhole, f_2, A_2')$ where:

* for all variables $x$ defined in $V_1$, $V_1(x)$ corresponds to
$V'_1(x)$ from $C$ to $C'$

* all array declarations of $E$ are present in $A_1'$

* $E'$ is obtained from $E$ by replacing all array
declarations with $()$

* $f_1' = f_1$

* $A_1 \subseteq A_1'$

* $A_2'$ contains all variable names of arrays declared in
$f_2$, and is the block domain of $M'$

* $V_2'$ is defined for all variable names in $A_2'$ as a block
identifier valid in $M'$

* all memory locations of arrays declared in $f_2$ are valid in

Each frame of the form $(M, V_1, E, f_1, A_1)$ in $S$ with $M \not=
\None$ is replaced with one frame in $S'$, namely $(\{ \}, V_1', E',
f_1', A_1')$ where:

* all blocks of $M$ are defined in $A_1'$

* for all variables $x$ defined in $V_1$, $V_1(x)$, if defined,
corresponds to $V_1'(x)$ from $C$ to $C'$

* all array declarations of $E$ are present in $A_1'$

* $E'$ is obtained from $E$ by replacing all array declarations
with $()$

* $f_1' = f_1$

* $A_1 \subseteq A_1'$

The fact that we are using a CompCert-style memory allocator is
crucial here to ensure that, once a source block identifier $b$
starts corresponding to a target one, it remains so forever, in
particular after its block has been freed (i.e. after its
corresponding variable has fallen out of scope), since in the latter
case, it corresponds to any block identifier and nothing has to be
proven then (since accessing memory through it will fail in the
source, per the fact that the CompCert-style memory allocator will
never reuse $b$.)

§.§ Local structures

has structures as values, unlike CompCert C and Clight, which both
need all structures to be allocated in memory. With a naive -to-C
compilation phase, where structures are compiled as C structures
and passed by value to functions, we experienced more than 60%
slowdown with CompCert compared to GCC -O1, using the benchmark in Figure <ref>, extracted to C as Figure <ref>. This
is because, unlike GCC, CompCert cannot detect that a structure is
never taken its address, which is mostly the case for local structures
in code generated from . This is due to the fact that, even at the
level of the semantics of C structures in CompCert, a field access is
tantamount to reading in memory through a constant offset. In other
words, CompCert has no view of C structures other than as memory
regions. To solve this issue, we replace local structures with their
individual non-compound fields, dubbed as structure erasure. Our
benchmark after structure erasure is shown in Figure <ref>.

module StructErase
open FStar.Int32
open FStar.ST

type u =  left: Int32.t; right: Int32.t

let rec f (r: u) (n: Int32.t): Stack unit (fun _ -> true) (fun _ _ _ -> true)  =
if lt n 1l
then ()
let r' : u =  left = sub r.right 1l ; right = add r.left 1l  in
f r' (sub n 1l)

let test () =
let r : u =  left = 18l ; right = 42l  in
let z2 = mul 2l 2l in
let z4 = mul z2 z2 in
let z8 = mul z4 z4 in
let z16 = mul z8 z8 in
let z24 = mul z8 z16 in
let z = mul z24 2l in
f r z  (* without structure erasure, CompCert segfaults
if replaced with 2*z *)

benchmarking for structure erasure

typedef struct
int32_t left;
int32_t right;

void StructErase_f(StructErase_u r, int32_t n)
if (n < (int32_t )1)   else
StructErase_u r_ =
.left = r.right - (int32_t )1,
.right = r.left + (int32_t )1
StructErase_f(r_, n - (int32_t )1);

void StructErase_test()
StructErase_u r =
.left = (int32_t )18,
.right = (int32_t )42
int32_t z2 = (int32_t )4;
int32_t z4 = z2 * z2;
int32_t z8 = z4 * z4;
int32_t z16 = z8 * z8;
int32_t z24 = z8 * z16;
int32_t z = z24 * z2;
StructErase_f(r, z);

Extracted C code, before structure erasure

void StructErase_f(int32_t r_left, int32_t r_right, int32_t n)
if (n < (int32_t )1)   else
int32_t r__left = r_right - (int32_t )1
int32_t r__right = r_left + (int32_t )1;
StructErase_f(r__left, r__right, n - (int32_t )1);

void StructErase_test()
int32_t r_left = (int32_t )18;
int32_t r_right = (int32_t )42;
int32_t z2 = (int32_t )4;
int32_t z4 = z2 * z2;
int32_t z8 = z4 * z4;
int32_t z16 = z8 * z8;
int32_t z24 = z8 * z16;
int32_t z = z24 * z2;
StructErase_f(r_left, r_right, z);

Extracted C code, after structure erasure

In our noninterference proofs where we prove that memory accesses are
the same between two runs with different secrets, treating all local
structures as memory accesses would become a problem, especially
whenever a field of a local structure is read as an expression (in
addition to the performance decrease using CompCert.)  This is another
reason why, in this paper (although a departure from our current
KreMLin implementation), we propose an easier proof based on the fact
that local structures should not be considered as memory regions in
the generated C code.

In addition to buffers (stack-allocated arrays), uses local
structures in three ways: as local expressions, passed as an argument
to a function by value, and returned by a function. Here we claim that
it is always possible to not take them as memory accesses, except for
structures returned by a function: in the latter case, it is necessary
for the caller to allocate some space on its own stack and pass a
pointer to it to the callee, which will use this pointer to store its
result; then, the caller will read the result back from this memory
area. Thus, we claim that, at the level of CompCert Clight, the only
additional memory accesses due to local structures are structures
returned by value.

So we extend 3 with the ability for functions to have several
arguments, all of which shall be passed at each call site (there shall
be no partial applications.)

§.§.§ Structure return

To handle structure return, we also have to account for their memory
accesses by adding corresponding events in the trace. Instead of
directly adding the memory accesses and trying to prove both program
transformation and trace transformation at the same time, we will
first add new $\symread$ and $\symwrite$ events at function return,
without those events corresponding to actual memory accesses yet;
then, in a second pass, we will actually introduce the corresponding
new stack-allocated variables.

We assume given a function $\kw{FunResVar}$ such that for any list of
statements $ss$ and any variable $x$, $\kw{FunResVar}(ss, x)$ is a
local variable that does not appear in $ss$ and is distinct from
$\kw{FunResVar}(ss, x')$ for any $x' \not= x$.

Let $p$ be a program $p$ and $ss$ be an entrypoint list of statements,
so we define $\kw{FunResVar}(f, x) = \kw{FunResVar(ss', x)}$ if $f
(\_) \{ ss' \}$ is a function defined in $p$, and
$\kw{FunResVar}(\None, x) = \kw{FunResVar}(ss,x)$.

Then, we define 4 as the language 3 where the $\textsf{Ret}_2$
function return rule is replaced with two rules following
Figure <ref>, adding the fake $\symread$ and
$\symwrite$. We do not produce any such memory access event if the
result is discarded by the caller; thus, we also need to check in the
callee whether the caller actually needs the result. To prepare for
the second pass where this check will be done by testing whether the
return value pointer argument is null, we need to account for this
test in the event trace in 4 as well.

* [Right=$\text{Ret}_4\text{Some}$]

FunResVar(f', x) = x'

θ= ;  (x', 0, []); (x',0,[])

p ⊢(S;(, V', t   x = ; ss', f', A'), V,  e; ss, f, A) _θ(S, V', t   x = v ; ss', f', A')

* [Right=$\text{Ret}_4\text{None}$]

p ⊢(S;(, V', ; ss', f', A'), V,  e; ss, f, A) _(S, V', ss', f', A')

4 Amended Configuration Reduction

If $\sys(p, V, ss)$ is safe in 3 and has unambiguous local
variables, then it has the same behavior and trace as in 4 with
$\brt$, $\brf$, $\symread$ and $\symwrite$ events removed.

With all such events removed, 3 and 4 are actually the same

The 3 invariants of Lemma <ref>
and <ref> also hold on 4.

This is true because the invariants of
Lemma <ref> actually do not depend on the traces
produced; and it is obvious to prove that, if two executions have
the same traces in 4, then they have the same traces in 3
(because in 3, some events are just removed.)

If $\sys(p, V_1, ss)$ and $\sys(p, V_2, ss)$ are safe in 3, have
unambiguous local variables, and produce the same traces in 3, then
they also produce the same traces in 4.

Two such executions actually make the same 4 steps.

Then, we define the $\kw{StructRet}$ structure return transformation
from 4 to 3 in Figure <ref>, thus removing
all structure returns from 3 programs.

\[
\kw{StructRet}(\_, \kw{return}\; e, x) = \left\{
\begin{array}{ll}
\eif{x}{ *[x] = e}{()} ; \kw{return}\;() & \text{if} ~ x \not= \None \\
\kw{return}\; e & \text{otherwise}
\end{array}
\right.
\]

\[
\kw{StructRet}(f', t ~ x = f(e), \_) = \left\{
\begin{array}{ll}
t ~ x'[1]; f(x', e); t ~ x = *[x'] & \text{if} ~ t ~ \text{is a} ~ \kw{struct} \\
& \text{and} ~ x' = \kw{FunRetVar}(f', x) \\
t ~ x = f(e) & \text{otherwise}
\end{array}
\right.
\]

\[
\kw{StructRet}(\_, f(e), \_) = \left\{
\begin{array}{ll}
f(0, e) & \text{if the return type of } ~ f ~ \text{is a} ~ \kw{struct} \\
f(e) & \text{otherwise}
\end{array}
\right.
\]

\[
\kw{StructRet}(\ecfun{f}{x}{t}{t'}{ss}) = \left\{
\begin{array}{ll}
\ecfuntwoargs{f}{r}{t'*}{x}{t}{\kw{unit}}{\{ \kw{StructRet}(f, ss, r) \} } &
\text{if} ~ t' ~ \text{is a} ~ \kw{struct} \\
& (r ~ \text{fresh}) \\
\ecfun{f}{x}{t}{t'}{\{ \kw{StructRet}(f, ss, \None) \} } & \text{otherwise}
\end{array}
\right.
\]

4 to 3 structure return

Then, the transformation back to 3 exactly preserves the traces of
4 programs, so that we obtain both functional correctness and
noninterference at once:

If $\sys(p, V, ss)$ is safe in 4 and has unambiguous local
variables, then it has the same behavior and trace as
$\sys(\kw{StructRet}(p), V, \kw{StructRet}(ss, \None))$.

Forward downward simulation, where the compilation invariant also
involves block identifier renaming from
Definition <ref> due to the new local
arrays introduced by the transformed program.

Each 4 step is actually matched by the same 3 step, except for
function return and return from block: for the $\textsc{RetBlock}$
rule, the simulation diagram has to stutter as many times as the
level of block nesting in the source program before the actual
application of a $\textsc{Ret}_4$ rule. Then, when the
$\textsc{RetSome}_4$ rule applies, the trace events are produced by
the transformed program, the $\brt$ and the $\symwrite$ events from
within the callee, then the callee blocks are exited, and finally
the $\symread$ event is produced from within the caller.

Then, the diagram is turned into bisimulation since 3 is

After a further hoisting pass, we can now restrict our study to those
3 programs with unambiguous local variables, functions with multiple
arguments, function-scoped local arrays, and no functions returning

§.§.§ Events for accessing structure buffers

Now, we transform an access to one structure into the
sequence of accesses to all of its individual atomic (non-structure)

NOTE: we need to have some typing information added to the
$\symread$, $\symwrite$ events of and each of $n$: whenever we
read or write from a buffer, we need to mark the type of the data
read/written. This makes sense in the context of observing memory
accesses, since without this data, two programs accessing the same
memory location but reading data of different types, thus of
potentially different lengths, would still be considered as having the
same trace, which we would like to rule out.  So, in the remaining
parts of this document, we assume that $\symread$ and $\symwrite$
events carry the type of the data read or written.

Consider the following transformation for 3 $\symread$ (and
similarly for $\symwrite$) events:

\[
\begin{array}{ll}
\multicolumn{2}{l}{\llbracket \symread\;(f, i, x, j, \ls{fd}, t) \rrbracket} \\
= & \llbracket \symread\; (f, i, x, j, \ls{fd};fd_1, t_1) \rrbracket \\
; & \dots \\
; & \llbracket \symread\; (f, i, x, j, \ls{fd};fd_n, t_n) \rrbracket \\
\text{if} & t = \kw{struct} \{ fd_1: t_1, \dots, fd_n: t_n \} \\
\\
\multicolumn{2}{l}{\llbracket \symread\;(f, i, x, j, \ls{fd}, t) \rrbracket} \\
= & \symread\; (f, i, x, j, \ls{fd}, t) \\
\multicolumn{2}{l}{\text{otherwise}}
\end{array}
\]

Then, let 5 be the 3 language obtained by replacing each
$\symread$, $\symwrite$ event with its translation. Then, it is easy
to show the following:

Let $p$ be a 3 program. Then, $p$ has a trace $t$ in 5 if, and
only if, there exists a trace $t'$ such that $p$ has trace $t'$ in
3 and $\llbracket t' \rrbracket = t$.

Thus, this trace transformation preserves functional correctness; and,
although this trace transformation is not necessarily injective (since
it is not possible to disambiguate between an access to a 1-field
structure and an access to its unique field), noninterference is also

After such transformation, all $\symread$ and $\symwrite$ events now
are restricted to atomic (non-structure) types.

§.§.§ Local structures

Now, we are removing all local structures, in such a way that the only
remaining structures are those of local arrays, and all structures are
accessed only through their atomic fields. In particular, we are
replacing every local (non-array) variable $x$ of type struct with the
sequence of variable names $x\_\ls{fds}$ for all field name sequences
$\ls{fds}$ valid from $x$ such that $x.\ls{fds}$ is of
non-$\kw{struct}$ type. (We omit the details as to how to construct
names of the form $x\_\ls{fds}$ so that they do not clash with other
variables; at worst, we could also rename other variables to avoid
clashes as needed.)

Using our benchmark in Figure <ref>, with C
code after structure erasure in Figure <ref>,
on a 4-core Intel Core i7 1.7 GHz laptop with 8 Gb RAM, structure
erasure saves 20% time with CompCert 2.7.

If we assume that we know about the type of a expression, then it
can be first statically reduced to a normal form as in
Figure <ref>.

Γ⊢n ↓^Int n

(x : t) ∈Γ

Γ⊢x ↓^t x

Γ⊢e_1 ↓^t* e_1'

Γ⊢e_2 ↓^int e_2'

Γ⊢e_1 + e_2 ↓^t* e_1' + e_2'

Γ⊢e ↓^struct { fd : t; …} * e'

Γ⊢efd ↓^t* e'fd

Γ⊢e ↓^struct { fd : t ; …} x.fds

t   is a   struct

Γ⊢e.fd ↓^t x.fds.fd

Γ⊢e ↓^struct { fd : t ; …} x.fds

t   is not a   struct

Γ⊢e.fd ↓^t x_fds_fd

Γ⊢e ↓^struct { fd : t ; …} { f = e' ; …}

Γ⊢e.fd ↓^t e'

Γ⊢e_i ↓^t_i e'_i

Γ⊢{ fd_i = e_i } ↓^struct { fd_i : t_i }  { fd_i = e'_i }

Structure Erasure: Expressions

For any value $v$ of type $t$, if $\llbracket e \rrbracket_{(p,V)} =
v$ and $\Gamma \vdash e \downarrow^t e'$ and $V'$ is such that:

* for any $(x': t') \in \Gamma$,  $V(x')$ exists, is of type $t'$ and is equal to $V(x)$

* for any $(x': t') \in \Gamma$ that is a struct and for any $\ls{fds}$ such that $x.\ls{fds}$ is not a struct, then $V'(x\_\ls{fds}) = V(x)(\ls{fds})$

Then, $\llbracket e' \rrbracket_{(p,V')} = v$

By structural induction on $\downarrow$.

A expression $e$ is said to be of type $t$ without structures if, and only
if, one of the following is true:

* $e$ contains neither a structure field projection nor a structure expression

* $e$ is of the form $x.\ls{fds}$ where $x$ is a variable such
that $x.\ls{fds}$ is of $\kw{struct}$ type

* t is of the form $\{ \ls{fd_i : t_i} \}$ and $e$ is of the form $\{ \ls{fd_i = e_i} \}$ where for each $i$, $e_i$ is of type $t_i$ without structures

If $\Gamma \vdash e \downarrow^t e'$, then $e'$ is of type $t$
without structures.

By structural induction on $\downarrow$.

Then, once structure expressions are reduced within an expression
computing a non-structure value, we can show that evaluating such a
reduced expression no longer depends on any local structures:

If $\llbracket e \rrbracket_{(p,V)} = v$ for some value $v$, and $e$
is of type $t$ without structures, and $t$ is not a $\kw{struct}$
type, then, for any variable mapping $V'$ such that $V'(x) = V(x)$
for all variables $x$ of non-$\kw{struct}$ types, $\llbracket e
\rrbracket_{(p,V')} = v$.

By structural induction on $\llbracket e \rrbracket_{(p,V)}$.

Now, we take advantage of this transformation to transform 5
statements into 3 statements without structure assignments.  This
$\downarrow$ translation is detailed in
Figure <ref>

In particular, each function parameter of structure type passed by
value is replaced with its recursive list of all non-structure
fields.[Our solution, although semantics-preserving as we
show further down, yet causes ABI compliance issues. Indeed, in the
System V x86 ABI, structures passed by value must be replaced not
with their fields, but with their sequence of bytes, some of which
may correspond to padding related to no field of the original
structure. CompCert does support this feature but as an
unverified elaboration pass over source C code. So, we
should investigate whether we really need to expose functions taking
structures passed by value at the interface level.]

t   not a   struct

Γ⊢e ↓^t* e'

p,Γ⊢t   x = e ↓t   x = e'

Γ[x] ←t

t   not a   struct

Γ⊢e_1 ↓^t* e'_1

Γ⊢e_2 ↓^t e'_2

p,Γ⊢e_1e_2 ↓e'_1e'_2

t = struct { 𝑓𝑑_𝑖 : t_i }

Γ⊢e ↓^t* e'

(x, _) ∉Γ

(x', _) ∉Γ

p,Γ∪(x' : t*) ∪(x_𝑓𝑑_i : t_i) ⊢x_𝑓𝑑_i = x'𝑓𝑑_i ↓𝑠𝑠_i

p,Γ⊢t   x = e ↓t*   x' = e'; 𝑠𝑠_i

Γ[x] ←t

t = struct { 𝑓𝑑_𝑖 : t_i }

Γ⊢e_1 ↓^t* e'_1

Γ⊢e_2 ↓^t e'_2

(x', _) ∉Γ

p,Γ∪(x' : t*) ⊢x'𝑓𝑑_ie'_2.𝑓𝑑_i ↓𝑠𝑠_i

p,Γ⊢e_1e_2 ↓t*   x' = e'_1 ; 𝑠𝑠_i

t   not a   struct

Γ⊢e ↓^t e'

p,Γ⊢return   e ↓return   e'

* [Right=Block]

p,Γ⊢ss ↓ss'

p,Γ⊢{ ss } ↓{ ss' }

* [Right=Call]

p(f)= fun (_ : t_i) : t { _ }

t   not a   struct

p,Γ⊢(t_i, 𝑒𝑙) ↓𝑒𝑙'

p,Γ⊢t x=f (𝑒𝑙) ↓t x = f(𝑒𝑙')

Γ[x] ←t

p,Γ⊢([],[]) ↓[]

p,Γ⊢(t, e) ↓𝑒𝑙_1

p,Γ⊢(𝑡𝑙, 𝑒𝑙) ↓𝑒𝑙_2

p,Γ⊢(t; 𝑡𝑙, e; 𝑒𝑙) ↓𝑒𝑙_1; 𝑒𝑙_2

t   not a   struct

Γ⊢e ↓^t e'

p, Γ⊢(t, e) ↓[e']

t = struct { 𝑓𝑑_i : t_i }

Γ⊢e ↓^t e'

p,Γ⊢(t_i, e'.𝑓𝑑_i) ↓𝑒𝑙_i

p, Γ⊢(t, e) ↓𝑒𝑙_i

* [Right=If]

t   not a   struct

Γ⊢e ↓^t e'

p,Γ⊢ss_i ↓ss'_i

p,Γ⊢ess_1ss_2 ↓e'ss_1'ss_2'

t   not a   struct

(x : t) ↓(x : t)

t = struct { 𝑓𝑑_i : t_i }

(x_𝑓𝑑_i : t_i) ↓𝑣𝑡_i

(x : t) ↓𝑣𝑡_i

* [Right=Fun]

𝑣𝑡 ↓𝑣𝑡'

p, (𝑣𝑡 ∪x_i : t_i*) ⊢𝑠𝑠 ↓𝑠𝑠'

fun (𝑣𝑡) : t { t_i   x_i[_] = { }  ; 𝑠𝑠 }
↓fun (𝑣𝑡') : t { t_i   x_i[_] = { }  ; 𝑠𝑠' }

5 to 3 Structure Erasure: Statements

If $p \downarrow p'$ following Figure <ref>,
then $p'$ no longer has any variables of local structure type, and no
longer has any structure or field projection expressions.

By structural induction over $\downarrow$, also using
Lemma <ref>.

If $p$ is a 5 program (that is, syntactically, a program with
unambiguous local variables, no block-scoped local arrays other than
function-scoped, and no functions returning structures) such that
$p$ is safe in 5 and $p \downarrow p'$ following
Figure <ref>, then $p$ and $p'$ have the same
execution traces.

Forward downward simulation where one 5 step triggers one or
several 3 steps. Then, determinism of 3 turns this forward
downward simulation into bisimulation.

The compilation invariant is as follows: the code fragments are
translated using $\downarrow$, and variable maps $V$ in source 5
vs. their compiled 3 counterparts $V'$ follow the conditions of
Lemma <ref>, also using
Lemma <ref>. Memory states
$M$ are exactly preserved, as well as the structure of the stack.

Then, after a further $\alpha$-renaming pass, we obtain
a 3 program that no longer has any local (non-stack-allocated)
structures at all, and where all memory accesses are of non-structure
type. The shape of this program is now suitable for translation to a
CompCert Clight program in a straightforward way, which we describe
in the next subsection.

§.§ Generation of CompCert Clight code

Recall that going from 3 (with abstract pointer events) back to 2
(with concrete pointer events) is possible thanks to the fact that
Lemma <ref> and
Lemma <ref> are actually

Recall that a $n$ transition system is of the form $\sys(p, V,
\mathit{ss})$ where $p$ is a list of functions[and global
variables, although the semantics of says nothing about how to
actually initially allocate them in memory], $\mathit{ss}$ is a list
of statements with undeclared local variables, the values of which
shall be taken from the map $V$. $\mathit{ss}$ is actually taken as
the entrypoint of the program, and $V$ is deemed to store the initial
values of secrets, ensuring that $p$ and $\mathit{ss}$ are
syntactically secret-independent.

In CompCert Clight, it is not nominally possible to start with a set
of undeclared variables and a map to define them. So, when translating
the entrypoint into Clight, we have to introduce a
secret-independent way of representing $V$ and how they are
read in the entrypoint. Fortunately, CompCert introduces the notion of
built-in functions, which are special constructs whose
semantics can be customized and that are guaranteed to be preserved by
compilation down to the assembly.

Thus, we can populate the values of local non-stack-allocated
variables of a entrypoint by uniformly calling builtins in Clight,
and only the semantics of those builtins will depend on secrets, so
that the actually generated Clight code will be syntactically

Translating 2 expressions with no structures or structure field
projections into CompCert Clight is straightforward, as shown in
Figure <ref>. For any 2 expression $e$ of
type $t$, assuming that $A$ is a set of local variables to be
considered as local arrays, we define $\mathbb C^t_A(e)$ to be the
compiled Clight expression corresponding to $e$.

\[
\begin{array}{lcl}
\mathbb C^{\kw{int}}_A (n) & = & n \\
\mathbb C^{\kw{unit}}_A (()) & = & 0 \\
\mathbb C^t_A (x) & = & \&x \\
& \text{if} & x \in A \\
\mathbb C^t_A (x) & = & \_x \\
& \text{if} & x \not\in A \\
\mathbb C^{t*}_A (e_1 + e_2) & = & \mathbb C^{t*}_A (e_1) +_t \mathbb C^{\kw{int}}_A (e_2) \\
\mathbb C^{t*}_A (\eptrfd{e}{fd}) & = & \&(*\mathbb C^{t'*}_A (e) ._{t'}\mathit{fd}) \\
& \text{if} & t' = \kw{struct}\{ \mathit{fd} : t, \dots \}
\end{array}
\]

2 to Clight: Expressions

Let $V$ be a 2 local variable map, and $A$ be a set of local
variables to be considered as local arrays. Assume that, for all $x
\in A$, there exists a block identifier $b$ such that $V(x) = (b,
0)$, and define $V'(x)$ be such block identifier $b$. Then, define
$\_V'(\_x) = V(x)$ for all $x \not\in A$.

Then, for any expression $e$ with no structures or structure
projections, $\kw{rv}(\mathbb C^t_A (e), (p, V', \_V')) = \llbracket
e \rrbracket_{(p, V)}$.

By structural induction on $e$. TODO: global variables.

Translating 2 statements with no local array declarations, no read
or write of structure type and no functions returning structures into
Clight is straightforward as well, as shown in
Figure <ref>.

\[
\arraycolsep=1pt
\begin{array}{lcl}
\mathbb C_A (t ~ x = e) & = & t ~ x = C^t_A(e) \\
\mathbb C_A (t ~ x = f(\ls{e_i})) & = & t ~ x = f(\ls{C^{t_i}_A(e_i)}) \\
& & \text{if} ~ f ~ \text{is} ~ \kw{fun}(\ls{(\_ : t_i)}) : \_ \{ \_ \} \\
\mathbb C_A (t ~ x = \eread{e}) & = & \clannot(\symread,t,e) ; t ~ x = [*\mathbb C^{t*}_A (e) ] \\
\mathbb C_A (\ewrite{e_1}{e_2}) & = & \clannot(\symwrite,t,e) ; *\mathbb C^{t*}_A(e_1) = \mathbb C^{t}_A(e_2) \\
\mathbb C_A (\eifthenelse{e}{ss_1}{ss_2}) & = & \eifthenelse{\mathbb C^t_A (e) }{\mathbb C_A(ss_1)}{\mathbb C_A(ss_2)} \\
& & \text{for some} ~ t ~ \text{not} ~ \kw{struct} \\
\mathbb C_A ( \{ ss \} ) & = & \{ \mathbb C_A (ss) \} \\
\mathbb C_A ( \kw{return} ~ e ) & = & \kw{return} ~ \mathbb C^t_A(e) \\
\end{array}
\]

2 to Clight: Statements

Let $p$ be a 2 program, and $ss$ be a 2 entrypoint sequence of
statements. Assume that $p$ and $ss$ have unambiguous local variables,
no functions returning structures, no local arrays other than
function-scoped arrays, and no local structures other than local
arrays. Further assume that $p$ has no function called $\kw{main}$,
and no function with the same name as a built-in function. Then, we
can define the compiled CompCert Clight program $\mathbb C(p, ss)$ as
in Figure <ref>.

\[
\begin{array}{lcl}
\mathbb C(p, ss)(f) & = & \kw{fun} ~ (\ls{x : t}) : t' \{ \ls{t_i ~ x_i[n_i]} ; \mathbb C_{\ls{x_i}}(ss') \} \\
& \text{if} & p(f) = \kw{fun} ~ (\ls{x : t}) : t' \{ \ls{t_i ~ x_i[n_i]} ; ss' \} \\
\mathbb C(p, ss)(\kw{main}) & = & \kw{fun} () : \kw{int} \{ \\
& & ~ \ls{t_i ~ x_i[n_i]} ; \\
& & ~ \ls{\_y_i = \kw{get}\_y_i()} ; \\
& & ~ \mathbb C_{\ls{x_i}}(ss') \\
& & \} \\
& \text{if} & \mathit{ss} = \{ \ls{t_i ~ x_i[n_i]} ; ss' \} \\
& & \text{with free variables} ~ \ls{y_i}
\end{array}
\]

2 to Clight: Program and Entrypoint

If $\sys(p, V, ss)$ is safe in 2, then it has the same execution
trace as $\mathbb C(p, ss)$ in Clight, when the semantics of the
built-in functions $\kw{get}\_x$ are given by $V$.

Forward downward simulation where one 2 step corresponds to one or
several Clight steps. Then, since Clight is deterministic, the
forward downward simulation diagram is turned into a bisimulation.

The structure of the Clight stack is the same as in the 2 stack,
and the values of variables are the same, as well as the memory
block identifiers. The only change is in the Clight representation
of 2 structure values . A 2 memory state $M$ is said to
correspond to a Clight memory state $M'$ if, for any block
identifier $b$, for any array index $i$, and for any field sequence
$\mathit{fds}$ leading to a non-structure value, $M'(b, n +
\kw{offsetof}(\mathit{fds})) = M(b, n)(\mathit{fds})$.

Thus, since both 2 and Clight records all memory accesses in their
traces, this theorem entails both functional correctness and
preservation of noninterference.

§ PROOF OF THE SECRET INDEPENDENCE THEOREM