Other leakage channels.
There are a variety of specific microarchitectural mechanisms which could
result in leakages, beyond the ones we've been focusing on in this paper.
For instance, in the presence of multithreading, port contention in the
processor's execution units can reveal sensitive
information [1]}; and many processor instructions, e.g., floating-point or SIMD instructions, can reveal information about their
operands through timing side-channels [2]}.
Most existing semantics do not model these effects.
However, the commonly-used \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  and \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  leakage
models are strong enough to already capture leakages from most of these
sources:
for instance, port contention can only reveal sensitive data if the sensitive
data influenced which instructions are being executed—and the
\(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  leakage model would have already considered the sensitive
data leaked once it influenced control flow.
For variable-time instructions, most works' definitions of \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\) 
don't capture this leakage, but extending those definitions to cover it is
straightforward [3]}.
In both of these examples, the \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  leakage model would capture
all of the leaks, because it (even more conservatively) would already
consider the sensitive data leaked once it reached a register, long before it
could influence control-flow or be used in a variable-time instruction.
Although modeling any of these effects more precisely could increase the
precision with which an analysis detects potential vulnerabilities, the
tradeoff in analysis complexity is probably not worth it, and for mitigation
and verification tools, the \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  and \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{arch}}\)  leakage
models provide stronger and more generalizable guarantees.
