The domain of Attacks
Software
Hardware
Attack Model
CAPEC-233: Privilege Escalation
CWE-ID: – 1262
Illegal Physical Memory Protection (PMP) unit access after mismatch
Threat Model – Privilege Escalation
| Soc Vul. # | Name of Core | Security Requirement | Threat model description | Effect | SW attack model |
|---|---|---|---|---|---|
| 6 | CVA6 RISC-V CPU | If there is any address mismatch during address translation for the physical memory locations, access should only be given in the highest privilege mode (M mode) | Privilege Escalation: Illegal access is given to lower privilege modes | Illegal memory page access from user privilege level | Software in the guest OS can access memory page without having the proper privilege permission. Possible attacks: Access control, Illegal interrupt, information leakage etc |
Description
In a system-on-chip (SoC), the software will commonly access the peripherals through a memory-mapped register interface. Thus, the software can access only certain registers with respect to their privilege level hardcoded in the design. However, through the accessible register interface, malicious software could tamper with the hardware data. The physical memory protection (PMP) unit takes care of the address translation for the physical memory locations inside the processor. If there is any mismatch during this process, no physical memory access is given to the lower privilege levels. However, this vulnerability can enable an attacker to gain the memory access even with lower privilege levels ( S mode and U mode).
Security Property
| property pmp; @(posedge clk_i) disable iff (!rst_ni) (ariane.ex_stage_i.lsu_i.i_mmu.i_pmp_if.priv_lvl_i == riscv::PRIV_LVL_S) |-> (ariane.ex_stage_i.lsu_i.i_mmu.i_pmp_if.allow_o !=1); endproperty ap_vulnerability126: assert property (pmp); |
Procedure
- Invoke Cadence JG inside the cva6_master folder
- Run the prove_t1.tcl script to check the assertion.
- Violation in the assertion will generate CEX.
Impact of Vulnerability
Loss of confidentiality and integrity of the SoC
Severity
TBA (Metrics to evaluate the vulnerability impact)
tools used
Cadence JasperGold
Results (counter-example)
Fig.1 shows that the property (ref. Table.2) violates the RISC-V design, indicating the illegal physical memory location access (privilege violation) in the generated CEX (shown in Fig.2).
