Leakage models for cryptography.
As we saw in subsec:prelims-ct, high-assurance cryptography
implementations have long relied on the constant-time programming model;
thus, semantics intended for cryptographic programs naturally choose the
\(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  leakage model.
Like the constant-time programming model in the non-speculative world, the
\(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  leakage model is strong and hardware-agnostic, making it a
solid foundation for security guarantees.
The \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  leakage model is a popular choice among existing
formalizations:
As we highlight in tab:mechanics, over half of the formal
semantics for Spectre use the \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\)  leakage model (or an
equivalent) [1]}, [2]}, [3]}, [4]}, [5]}, [6]}, [7]}.
Guarnieri et al.  [8]}
leave the leakage model abstract, allowing the semantics to be used with
several different leakage models, including \(\llbracket \,\cdot \, \rrbracket ^{\text{}}_{\text{ct}}\) .
