UPEC
References:
- Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. By Mohammad Rahmani Fadiheh, et. al. 2018 arXiv, 2019 DATE
UPEC: Unique Program Execution Checking.
Orc Attack
- Leverage the RAW(Read after write) hazard: load latency is longer when RAW happens.
- Assumptions: (simplified for easy understanding)
- each cache line is selected based on lower 8 bits;
- a total of $2^8=256$ cache lines.
- Attack:
- guess a possible address
#test_value; - write a value at the
#test_value - load a secret to a register
lw x4, 0(x1), wherex1is#protected_addr; ==> this will throw an exception,x4will not have the secret value (not architectual visible). - perform a load with secret as address:
lw x5, 0(x4); ==> this will not be architecturally visible (x5 not updated), but the instruction already in the pipeline and will issue a cache transaction. - If
#test_valueand0(x4)in the same cache line, then a RAW hazard will happen, and- the instruction sequence will have higher latency due to the RAW hazard. ==> this timing latecy will be used to detect whether the possible hazard exists.
- their lower 8 bits are the same. ==> the secret will be leaked by 8 bits.
- guess a possible address
Design
Unique Program Execution Checking.
Security Property Definition
Two sets of state variables
- State variables associated with the content of its memory;
- State variables associated with all other parts of the hardware, the logic parts.
- Microarchitectural State Variable: belonging to the logic part of the computing system’s microarchitecture.
- Registers, buffers, flip-flops.
- Architectural State Variable: subset of microarchitectural state variables that define the state of program execution at the ISA level (excluding the program state that is represented in the program’s memory).
- Microarchitectural State Variable: belonging to the logic part of the computing system’s microarchitecture.
Secret Data
- Secret Data $D$, at Protected Location $A$.
Unique Program Execution
- Unique Program Execution. A program executes uniquely w.r.t. a secret $D$ if and only if the sequence of valuations to the set of architectural state variables is independent of the values of $D$, in every clock cycle of program execution.
- In other words, unique program execution means that different values of $D$ does not lead to different values of the program’s architectural state variables, nor lead to different time points when these values are assigned.
Confidentiality
- Confidentiality/Observalibity. A set of secret data $D$ in a protected location $A$ is confidential if and only if any user-level program executes uniquely w.r.t. $D$. Otherwise, $D$ is observable.
Property Checking
The requirement of unique program execution is formalized as a “property” expressed in a property language which is understood by a (commercially available) tool for property checking.
Challenge: current tools for property checking are build for functional design verification. In order to make property checking applicable to UPEC, we present a tailor-made computational model and formulate a specific property to be proven on this model.
UPEC Model
Automatically derived model: This model (in Figure 3) can be derived automatically from the RTL description of the design and only requires the user to provide the protected region.
Two identical instrances: $SoC_1$ and $SoC_2$ are two identical instances of the logic part of the SoC under verification.
Two almost same set of memory: $Memory_1$ and $Memory_2$ hold the same set of values except for the memory location of a defined secret data.
UPEC Property
For a system to be secure w.r.t. convert channel attacks, the computational model derived from the design’s RTL description has to fulfill the following property expressed in the CTL property language [c36]:
No Covert Channel Property: $\boldsymbol{AG}$(secret_data_protected $\wedge$ micro_soc_state_1 = micro_soc_state_2 $\rightarrow \boldsymbol{AG}$ soc_state_1 = soc_state_2)
where $\boldsymbol{AG}$: the following condition must be fulfilled at all times and for all possible runs of the system (“A for All paths, G for Globally”). Note: CTL symbols
where micro_soc_state is a a vector of all microarchitecture state variables.
where soc_state is some vector of state variables which includes, as a subset, all architectural state variables.
where secret_data_protected is a constraint specifing that a protection mechanism in the hardware is enabled for the secret data memory location.
The property fails, if and only if, there exists a state, soc_state, such that the transition to the next state, soc_state’, depends on the secret data.
UPEC outputs
Counterexamples of unique program execution.
$L-alert$, Leakage alert.
$P-alert$, Propagation alert.
Evaluation
(2019 DATE) Rocket/OneSpin 360 DV-Verify
Rocketchip, a single-core SoC with in-order pipelined processors and separate data and instruction level-1 cache.
OneSpin 360 DV-Verify, a commercial property checker.
- Original Rocketchip
- Variant a, with Meltdown;
- Modified the design: a cache line refill is not canceled in case of an invalid access.
- Attack: the illegal access itself is not successful but raises an exception, the cache content is modified and can be analysed by an attacker.
- Highlight: this covert channel is based on an in-order pipeline, instead of an out-of-order as previous reports.
- Variant b, with Orc attack.
- Conditionally bypass one buffer.
Results:
- UPEC captured all vulnerabilities.
- found an ISA incompliance in the Physical Memory Protection (PMP) unit of the original design.
More
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?