Next, to precisely specify the attacker model, the developer
must define which
leakage observations—information
produced during an execution step—are visible to an attacker. For example,
we may decide that rules with memory accesses leak the addresses being accessed.
The set of leakage observations in a semantics' rules is its
leakage model.
We again borrow notation from [1]},
which defines the leakage models \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  and \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\) .
The \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  model exposes leakage observations relevant to constant-time security:
The sequence of control flow (the execution trace) and the sequence
of addresses accessed in memory (the memory trace).Like [1]}, we omit variable-latency
instructions from our formal model for simplicity.
The \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  model exposes
the values loaded from memory in addition to the addresses.Equivalently, it exposes the trace of register values [1]}.
Since the leakage observations in \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  are a strict superset of
those in \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\) , we say that \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  is stronger
than \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\) , meaning that it models a more powerful attacker.
In fact, with \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\) , effectively all computation is leaked to the
attacker.
Thus, \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  is most useful for software isolation: A sandbox
verifier, for example, will want to prove that a guest sandbox cannot
retrieve any data at all from outside its sandbox boundary.
