>> Hello, I'm Catalin Marinas,
Fellow Engineer at Linux Kernel Lead at ARM Limited.
While my day job is mostly
Linux Kernel development and maintenance,
I have an interest in formal methods and
use them occasionally to help with my tasks.
This may be modeling the spin lock implementations,
some tricky concurrent algorithm,
or just after hardware interaction.
This doc however, is not about Linux,
but something both hardware and software people have
been concerned with for the past three years.
Cache speculation side-channels from a formal angle.
From the Wikipedia definition,
a side-channel attack is an attack that gets information from
the actual hardware implementation rather
than relying on a weakenising the algorithm itself.
For example, in the cache side-channels case,
the attacker can probe the contents of the cache
by timing the access to certain memory locations.
With cache speculation side-channels,
the attacker uses the imprint left in the cache
by instructions executed speculatively in the victim.
The aim is to create a significantly simpler abstract model of
CPU speculative execution and
define its confidentiality and integrity properties.
We then want to check whether
the security properties are upheld by
the CPU specification for any reasonable code sequence.
Such model allows us to explore
related vulnerabilities and workarounds at
an abstract level and in a unified way.
As we'll see, the model can explain
the current Spectre and Meltdown vulnerabilities.
Let's start with the Spectre variant 1 example
taken from our speculation side-channels whitepaper.
This is a code sequence of
64-bit ARM assembly running in a high privilege mode,
for example, an operating system kernel.
The input provided by a low privilege user has heard in the X0
register and represents an untrusted offsetting to a kernel array.
If such offset is off the bonds,
the algorithm skips the kernel array access
with a conditional branch instruction.
If the decision on the branch
inside the CPU if delayed, for example,
because the extra upper-bound hasn't been loaded yet,
the CPU may speculatively continue
the execution of the upper instructions in this sequence.
With X0 or the bonds,
the first LDRB instruction will access
potentially secret information belonging to the kernel.
Subsequent arithmetic operations on this value and the load from
a user address at an offset derived from
this secret data will leave a trace in the cache.
While the register state under speculation is discarded,
the attacker can still probably cast
data by timing the memory access.
Let's now dive into
the abstract CPU model and define the system state.
Rather than using 64-bit values and
the arithmetics for which the model checker won't scale,
we go for sets of model values,
we define symbols for low and high addresses,
data values, and the set of names for the CPU registers.
Since we don't have actual numbers and arithmetics,
we need to define a set of operations on these values.
An operation is a function that
takes two values and gives back a new one.
Optables here is the set of
all such functions over the values we defined.
The system state consists of a privilege mode,
registers mapping names to values we defined,
memory mapping addresses to values,
and the cached stateable addresses.
We don't need to model the caches and
associative array for our security properties,
we are only interested in whether
a memory location is cached or not.
Not that we don't include the program counter,
although it can be part of the regs set of model values.
With the system variables defined,
we need a set of actions to transition between states.
We will use tuples of
instruction mnemonics and arguments
for modeling the program execution.
We have a Havoc subset of instructions that
set the register state to a specific value.
The move instructions copy a value from a register to another.
The memory accesses are only permitted if
the current privilege mode allows
loads and stores to specific memory locations.
For example, the AccessOK operator will not
allow a low privilege mode to read or write high addresses.
The OP subset contains all possible instructions that take values
from two source registers and combine them
into a new value stored in a destination register.
To switch the system state between
low and high privilege modes, for example,
our system call and the corresponding return,
we introduce a set of two instructions, HCALL and LRET.
The set of all valid instructions sees the union of these subsets.
The execute instruction dispatcher is responsible for
interpreting the commands and
changing the system's date accordingly.
The program execution is modeled as
a succession of steps starting from an initial state.
To reduce the number of initial states for the model checker,
we chose registers initialized to zero and cache is empty.
The next step chooses an instruction
non-deterministically from the valid set
and invokes the dispatcher,
which is responsible for changing the system state.
Since we pick instructions non-deterministically,
there isn't a need to
model a program counter for the instruction flow.
As you can see in the example at the bottom of the slide,
the register's state starts with
an initial zero values and
transitions according to the instructions being executed.
In the final step,
we have an operation that takes the values d1 and they tron into
registers and computes a new value
h2 that is stored in the destination register.
So far the behavior of our system only
modeled the algorithmic state that is visible to the programmer.
Under speculation, the CPU may
execute additional instructions starting from
a programmer visible state either
discarding the resulting registered values
or committing the status value,
depending on how, for example,
a previously delayed condition check was resolved.
In our model, we only consider
the discarding of the speculative register state.
Since the programmer's view of the registers
remains unchanged during speculation,
we model it as another instance of
the previously defined SimpleCPU
but with a separate register state.
The new slightly more complex system consists of
two simple CPUs that share the memory and the cache,
but with separate register backs.
Know that not all instructions are available on the speculation,
especially those that can modify memory,
a such state is programmer visible.
From now on I will refer to
executed instructions as those steps visible to the programmer
affecting the algorithmic state and speculated instructions
as those where the speculative register state
will eventually be discarded.
You can see the example figure where states 0 and
1 of the executing CPU registers
are kept in sync with a speculating one.
If the executed instructions are
delayed but the speculation continuous,
the instructions only affect
the speculative register path and are eventually discarded.
Actually plus specification of
our new system behavior with two instances of a simple CPU.
The SpecCPU instance has its own regs variable.
We also need two instruction dispatchers,
one for the executing CPU,
which keeps the speculative registers in sync,
and another for the speculating CPU,
which leaves the programmer visible state unchanged.
As I mentioned earlier,
only a subset of instructions are available under speculation.
We limited it here to memory loads and operations on values,
but other instructions like the Havoc set could be included.
The next step is defined as
a non-deterministic choice of either
executed or speculated instructions.
Since this doc is about security properties,
before stating them, we need to define
the roles and projections of the system state.
We consider the victim to be a high-privileged mode,
for example, an operating system kernel.
It has its own state consisting of registers and high memory.
Such high memory may or may not contain secret information.
The high mode can accept input and provide output,
for example, system poll arguments
and results returned to the caller.
In our model, these consist of all the low memory
and the registers or when entering or exiting the high mode.
The attacker is a low-privilege mode, for example,
a user application with a low state
consisting of registers and low memory.
Without timing side-channel, the attacker can only observe
the content of the low memory and some registers.
With cache side-channels, however,
the attacker can probe whether the memory location is cached using
the difference in the execution time
or the corresponding memory access.
We have not explicitly included time
as a state in this model, however,
we define the attacker observable state as a function mapping
low addresses to both the values in memory and the cached state.
Because of the AccessOK operator defined earlier,
the model does not permit the attacker to
directly observe any high memory locations.
Confidentiality is a non-interference property stating that
the attacker cannot observe anything
other than what the victim allows in its output.
In other words, the attacker's observation is
a deterministic function of
only the initial state victim's output and its own actions.
We modeled this as a property over
two LowState-identical behaviors that
must have the same low observation functions.
We assume that the individual commands
or instructions are deterministic.
This means that for a given state and instruction,
always leads to the same next state in all behaviors.
We'll define integrity since it
compliments the confidentiality property,
although this is not included in the TLAplus model.
This property holds when the victim's execution is not
affected by the attacker beyond the input provided.
This can be modeled similarly with a hybrid property over
two behaviors that start from the same initial high state,
have the same input,
and must always lead to the same high state and output.
TLAplus does not directly support hybrid properties.
However, we can create a new specification
encompassing two behaviors: the start from
the same LowState and low observation and
perform a similar execution or speculation next step.
I highlighted the requirement that following an executing step,
the registers are the same in both behaviors.
What we actually want here is that
the low observations are the same for
an executing step under the assumption that
the algorithm itself does not
leak information through side channels.
Using regs equality may be a bit more restrictive,
but I don't think TLAplus supports LowObs prime notation.
For the confidentiality property,
the new hyperspec must imply
that the observation functions are identical.
Now that we defined our specification and its properties,
we can run it through TLC,
the TLAplus model checker probably
expected the confidentiality property does not hold.
This figure represents the reported trace
of the two behaviors of our specification.
For space reasons, the trace has been
simplified and the low mode execution removed.
As you can see, we have two behaviors starting from
the same LowState and low observation,
but with
potentially different high-stake holding secret information.
The r1 register contains an untrusted value,
d1, provided by the attacker.
The victim sets the r3 register to a higher address,
h1 that is not expected to contain any secret.
Subsequently, the algorithm decides that the d1
is out of bound and changes the executed instructions flow.
However, the CPU continues to
use this untrusted value under speculation.
An operation combining the safe address,
h1, with the untrusted value, d1,
yields a new address, h2,
which contains secret information
and therefore is different in the two behaviors.
The load from h2 sets
the speculative register r1
to two different values in the two behaviors.
These are used to compute
two different low addresses and the speculative loads from
those addresses leave two different imprints
in the low address cache,
the confidentiality property is not violated
since the low observation function is
different in the two behaviors.
This trace resembles at an abstract level,
a Spectre Variant 1 exploit.
What do the speculative execution vulnerabilities
map onto our abstract model?
We just seen a Spectre Variant 1 example on the previous slide
with a confidentiality property violated by the speculating CPU.
The softer workarounds usually try to make
speculative instructions flow not depend on untrusted data.
For example, behind the conditional branch,
the register holding such data would be zero if deemed unsafe.
Spectre Variant 2 is
an integrity violation in the speculating CPU.
If we consider a program counter as part
of the register set on certain CPU implementation,
its values can be driven
from the attacker by training the branch predictor.
Know that this is only for the speculating CPU.
This would make it much easier to employ a Spectre v1 attack.
The workarounds limit the influence
one mode has over the branch prediction in another mode,
either by explicit flushing or by tagging
the branch predictor entries with additional context information.
Meltdown or Variant 3 doesn't even need the victim to run,
a speculative load in the low mode
is not checked against the high access permissions.
While the value loaded cannot be used directly,
it can be made through a set of operations to leave a trace
in the cache state that's probed with executed instructions.
The workaround on the affected CPUs is to enforce
such permission check by other means
like kernel page-table isolation.
Spectre Variant 4 is in some ways similar to Variant 1,
only that the secret high memory location
is one written by the victim
with an non-private value and considered algorithmically safe.
Under speculation, a load instruction from
this address is allowed to read data prior to the store,
therefore revealing potentially secret information.
The model can be adopted for this vulnerability by
using separate memory state in the speculating CPU instance.
The workaround is either a hardware knob
disabling this behavior with some performance penalty,
or explicit software use of specific barriers.
Only the disclosure of
the speculations by channel vulnerabilities,
the ARM architecture introduce
new barriers to help with the software workarounds.
In this model, we haven't
included data value prediction in the speculating CPU,
but that's equivalent to allowing
the Havoc instruction set on the speculation.
CSDB prevents those instructions.
SSBB does not allow
a speculative load from reading values prior to store.
We just mentioned it in the Spectre example on the previous slide.
SB disallows the set of
instructions on the speculation
that may have an observable side effect.
There are several papers on
noninterference and observational determinism,
but not enough space to be written here.
I'll mention the ARM whitepaper on speculative execution.
This is not the both for more models,
but rather a description of the Spectre and Meltdown
variants as they apply to the ARM processors.
Of course, this model wouldn't have been possible
without the Specifying Systems book.
Source of inspiration on modeling the security properties
in this presentation was Subramanyan's paper on secure enclaves.
This paper does not cover speculative execution,
but it does cover slide channels.
Guarnieri's SPECTECTOR paper proposes
a slightly different approach to modeling speculation,
but is focused mostly on analyzing
specific code gadgets for vulnerabilities.
If you are interested in the TLAplus model presented here,
please follow the link.
Thank you for watching and I hope to see you at
the TLAplus community event in October, 2020.