Welcome > Logics > Fm in Arch > UPEC

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), where x1 is #protected_addr; ==> this will throw an exception, x4 will 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_value and 0(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.

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).

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.

If you could revise
the fundmental principles of
computer system design
to improve security...

... what would you change?