Semantics for assembly or IRs.
The majority of formal semantics in tab:mechanics operate on
abstract assembly-like languages, with commands that map to simple
architectural instructions.
Semantics at this level implement control flow directly in terms
of jumps to program points—usually indices into memory or an
array of program instructions—and treat memory as largely unstructured.
Since these low-level semantics closely correspond to the behavior of real
hardware, they capture speculative behaviors in a straightforward manner,
and provide a foundational model for higher-level reasoning.
Similarly, many concrete
analysis tools for constant-time or Spectre operate directly on
binaries or
compiler intermediate representations (IRs) [1]}, [2]}, [3]}, [4]}, [5]}.
These tools operate at this lowest level
so that their analysis will be valid for the program unaltered—compiler optimizations for higher-level languages can end up transforming programs in
insecure ways [6]}, [2]}, [3]}.
As a result however, these tools necessarily
lose access to higher-level information such as control flow structure
or how variables are mapped in memory.
