Leakage models for isolation.
Sections REF  and REF 
described the \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  leakage model more suited to speculative
isolation—e.g., JavaScript or WebAssembly runtimes which execute untrusted
code.
Like \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\) , this is a hardware-agnostic leakage model,
well-suited to providing solid security guarantees.
The \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  leakage model is, however, less-frequently considered
in formal models: Only two of the semantics in tab:mechanics
([1]}, [2]}) use the \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  leakage
model.
Spectre sandbox isolation frameworks such as Swivel [3]},
Venkman [4]}, and ELFbac [5]}
appear to use the \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  model as a guide, as do
SpecFuzz [6]} and certain modes of oo7 [7]}.
Unfortunately, many of these tools are not formalized, so their leakage
models are not explicit (and clear).
