Skip to content

Commit

Permalink
added command line support for Smepmp. command line switch: --enable-…
Browse files Browse the repository at this point in the history
…smepmp. Sail function: haveSmepmp

Added support of Smepmp

Co-authored-by: William McSpaddden <bill@riscv.org>
Co-authored-by: Hamza Khan <hamza.khan@10xengineers.ai>
  • Loading branch information
3 people committed Mar 3, 2025
1 parent 8387b14 commit cf51e2e
Show file tree
Hide file tree
Showing 9 changed files with 141 additions and 17 deletions.
1 change: 1 addition & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -126,6 +126,7 @@ Supported RISC-V ISA features
- Sv32, Sv39, Sv48 and Sv57 page-based virtual-memory systems
- Physical Memory Protection (PMP)
- Smcntrpmf extension for cycle and instret privilege mode filtering, v1.0
- Smepmp extension for pmp enhancements for memory access and execution prevention on Machine mode, v1.0

#### The following features are not currently supported:
- The Hypervisor Extension.
Expand Down
5 changes: 5 additions & 0 deletions c_emulator/riscv_platform.c
Original file line number Diff line number Diff line change
Expand Up @@ -92,6 +92,11 @@ uint64_t sys_vector_elen_exp(unit u)
return rv_vector_elen_exp;
}

bool sys_enable_smepmp(unit u)
{
return rv_enable_smepmp;
}

bool sys_enable_writable_misa(unit u)
{
return rv_enable_writable_misa;
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform.h
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ uint64_t sys_pmp_grain(unit);
bool sys_vext_vl_use_ceil(unit);
uint64_t sys_vector_vlen_exp(unit);
uint64_t sys_vector_elen_exp(unit);
bool sys_enable_smepmp(unit);

bool plat_enable_dirty_update(unit);
bool plat_enable_misaligned_access(unit);
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.c
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,7 @@ bool rv_enable_bext = false;
bool rv_enable_zicbom = false;
bool rv_enable_zicboz = false;
bool rv_enable_sstc = false;
bool rv_enable_smepmp = false;

bool rv_enable_dirty_update = false;
bool rv_enable_misaligned = false;
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.h
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ extern bool rv_enable_misaligned;
extern bool rv_mtval_has_illegal_inst_bits;
extern bool rv_enable_writable_fiom;
extern uint64_t rv_writable_hpm_counters;
extern bool rv_enable_smepmp;

extern uint64_t rv_ram_base;
extern uint64_t rv_ram_size;
Expand Down
6 changes: 6 additions & 0 deletions c_emulator/riscv_sim.c
Original file line number Diff line number Diff line change
Expand Up @@ -54,6 +54,7 @@ enum {
OPT_ENABLE_ZICBOZ,
OPT_ENABLE_SSTC,
OPT_CACHE_BLOCK_SIZE,
OPT_ENABLE_SMEPMP,
};

static bool do_show_times = false;
Expand Down Expand Up @@ -147,6 +148,7 @@ static struct option options[] = {
{"enable-bitmanip", no_argument, 0, 'B' },
{"enable-writable-fiom", no_argument, 0, OPT_ENABLE_WRITABLE_FIOM},
{"enable-svinval", no_argument, 0, OPT_ENABLE_SVINVAL },
{"enable-smepmp", no_argument, 0, OPT_ENABLE_SMEPMP },
{"enable-zcb", no_argument, 0, OPT_ENABLE_ZCB },
{"enable-zicbom", no_argument, 0, OPT_ENABLE_ZICBOM },
{"enable-zicboz", no_argument, 0, OPT_ENABLE_ZICBOZ },
Expand Down Expand Up @@ -305,6 +307,10 @@ static int process_args(int argc, char **argv)
}
rv_pmp_grain = pmp_grain;
break;
case OPT_ENABLE_SMEPMP:
fprintf(stderr, "enabling Smepmp extension.\n");
rv_enable_smepmp = true;
break;
case 'C':
fprintf(stderr, "disabling RVC compressed instructions.\n");
rv_enable_rvc = false;
Expand Down
47 changes: 45 additions & 2 deletions model/riscv_pmp_control.sail
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,14 @@ function pmpAddrRange(cfg: Pmpcfg_ent, pmpaddr: xlenbits, prev_pmpaddr: xlenbits
}
}
}
// helper function to check if the access type is execute
val isExecute: AccessType(ext_access_type) -> bool
function isExecute(acc: AccessType(ext_access_type)) -> bool =
match acc {
Execute(_) => true,
_ => false,
}


/* permission checks */

Expand All @@ -47,6 +55,34 @@ function pmpCheckRWX(ent, acc) =
Execute() => ent[X] == 0b1,
}

/* this needs to be called with the effective current privilege */
val pmpCheckPerms: (Pmpcfg_ent, AccessType(ext_access_type), Privilege) -> bool
function pmpCheckPerms(ent, acc, priv) = {
if mseccfg[MML] == 0b1
then {
match (ent[L], ent[R], ent[W], ent[X]) {
(0b1, 0b0, 0b1, _) =>
match acc {
Execute(_) => true,
Read(_) => priv == Machine & ent[X] == 0b1,
_ => false
},
(0b0, 0b0, 0b1, _) =>
match acc {
Read(_) => true,
Write(_) => priv == Machine | ent[X] == 0b1,
_ => false
},
(0b1, 0b1, 0b1, 0b1) =>
match acc {
Read(_) => true,
_ => false
},
(L, _, _, _) => ((priv == Machine) == (L == 0b1)) & pmpCheckRWX(ent, acc)
}
}
else (priv == Machine & not(pmpLocked(ent))) | pmpCheckRWX(ent, acc)
}

/* matching logic */

Expand Down Expand Up @@ -84,7 +120,7 @@ function pmpMatchEntry(addr: physaddr, width: xlenbits, acc: AccessType(ext_acce
match pmpMatchAddr(addr, width, rng) {
PMP_NoMatch => PMP_Continue,
PMP_PartialMatch => PMP_Fail,
PMP_Match => if pmpCheckRWX(ent, acc) | (priv == Machine & not(pmpLocked(ent)))
PMP_Match => if pmpCheckPerms(ent, acc, priv)
then PMP_Success
else PMP_Fail
}
Expand Down Expand Up @@ -112,7 +148,12 @@ function pmpCheck forall 'n, 'n > 0. (addr: physaddr, width: int('n), acc: Acces
PMP_Continue => (),
}
};
if priv == Machine then None() else Some(accessToFault(acc))
/* Make Read, Write and execute denied by default, if mseccfg[MMWP] == 0b1 for M mode
* Make execute denied, if mseccfg[MML] == 0b1 for M mode
*/
if priv == Machine & mseccfg[MMWP] == 0b0 & (mseccfg[MML] == 0b0 | not(isExecute(acc)))
then None()
else Some(accessToFault(acc))
}

function reset_pmp() -> unit = {
Expand All @@ -121,6 +162,8 @@ function reset_pmp() -> unit = {
"sys_pmp_count() must be 0, 16, or 64"
);

mseccfg = [mseccfg with MML = 0b0, MMWP = 0b0, RLB = 0b0];

foreach (i from 0 to 63) {
// On reset the PMP register's A and L bits are set to 0 unless the plaform
// mandates a different value.
Expand Down
50 changes: 35 additions & 15 deletions model/riscv_pmp_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -89,32 +89,46 @@ function pmpReadAddrReg(n : range(0, 63)) -> xlenbits = {
}

/* Helpers to handle locked entries */
function pmpLocked(cfg: Pmpcfg_ent) -> bool =
cfg[L] == 0b1
function pmpLocked(cfg: Pmpcfg_ent) -> bool = (cfg[L] == 0b1) & (mseccfg[RLB] == 0b0)

function pmpTORLocked(cfg: Pmpcfg_ent) -> bool =
(cfg[L] == 0b1) & (pmpAddrMatchType_of_bits(cfg[A]) == TOR)
function pmpTORLocked(cfg: Pmpcfg_ent) -> bool = pmpLocked(cfg) & (pmpAddrMatchType_of_bits(cfg[A]) == TOR)

function pmpWriteCfg(n: range(0, 63), cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent =
if pmpLocked(cfg) then cfg
function pmpWriteCfg(n: range(0, 63), cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = {
/* If locked then configuration is unchanged */
if pmpLocked(cfg)
then cfg
/* To prevent adding a rule with execution privileges if MML is enabled unless RLB is set */
else {
// Bits 5 and 6 are zero.
let cfg = Mk_Pmpcfg_ent(v & 0x9f);

/* Constructing legal Pmpcfg_ent by making bit 5 and 6 zero */
let legal_v : Pmpcfg_ent = Mk_Pmpcfg_ent([v with 6 .. 5 = zeros()]);
// "The R, W, and X fields form a collective WARL field for which the combinations with R=0 and W=1 are reserved."
// In this implementation if R=0 and W=1 then R, W and X are all set to 0.
// This is the least risky option from a security perspective.
let cfg = if cfg[W] == 0b1 & cfg[R] == 0b0 then [cfg with X = 0b0, W = 0b0, R = 0b0] else cfg;
let legal_v : Pmpcfg_ent = match (mseccfg[MML], legal_v[R], legal_v[W]) {
(0b0, 0b0, 0b1) => [legal_v with W = 0b0],
(_, _, _) => legal_v
};

let legal_v : Pmpcfg_ent = if (mseccfg[MML] == 0b1 & mseccfg[RLB] == 0b0 & legal_v[L] == 0b1)
then {
match (legal_v[R], legal_v[W], legal_v[X]) {
(0b0, 0b0, 0b1) => cfg,
(0b0, 0b1, 0b0) => cfg,
(0b0, 0b1, 0b1) => cfg,
(0b1, 0b0, 0b1) => cfg,
(_, _, _) => legal_v
}
} else legal_v;

// "When G >= 1, the NA4 mode is not selectable."
// In this implementation we set it to OFF if NA4 is selected.
// This is the least risky option from a security perspective.
let cfg = if sys_pmp_grain() >= 1 & pmpAddrMatchType_of_bits(cfg[A]) == NA4
then [cfg with A = pmpAddrMatchType_to_bits(OFF)]
else cfg;

cfg
let legal_v = if (sys_pmp_grain() >= 1 & pmpAddrMatchType_of_bits(legal_v[A]) == NA4)
then [legal_v with A = pmpAddrMatchType_to_bits(OFF)]
else legal_v;
legal_v
}
}

function pmpWriteCfgReg(n : range(0, 15), v : xlenbits) -> unit = {
if xlen == 32
Expand Down Expand Up @@ -254,3 +268,9 @@ function clause write_CSR(0x3B @ idx : bits(4), value) = { let idx = unsigned(0b
function clause write_CSR(0x3C @ idx : bits(4), value) = { let idx = unsigned(0b01 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
function clause write_CSR(0x3D @ idx : bits(4), value) = { let idx = unsigned(0b10 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }
function clause write_CSR(0x3E @ idx : bits(4), value) = { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) }

function checkPmpNcfgL(n : range(0, 63)) -> bits(1) = {
if n == 0
then pmpcfg_n[0][L]
else checkPmpNcfgL(n - 1) | (pmpcfg_n[n][L])
}
46 changes: 46 additions & 0 deletions model/riscv_sys_regs.sail
Original file line number Diff line number Diff line change
Expand Up @@ -107,6 +107,11 @@ val sys_pmp_grain = pure "sys_pmp_grain" : unit -> range(0, 63)
/* Which HPM counters are supported (as a bit mask). Bits [2 .. 0] are ignored. */
val sys_writable_hpm_counters = pure "sys_writable_hpm_counters" : unit -> bits(32)

/* Enable Smepmp */
val sys_enable_smepmp = pure "sys_enable_smepmp" : unit -> bool
/* TODO: for extension smmpm and zkr to enable */
function sys_has_mseccfg() -> bool = sys_enable_smepmp()

/* whether misa.v was enabled at boot */
val sys_enable_vext = pure "sys_enable_vext" : unit -> bool

Expand Down Expand Up @@ -409,6 +414,47 @@ function is_fiom_active() -> bool = {
}
}

bitfield Mseccfg_ent : bits(64) = {
RLB : 2, /* Rule Locking Bypass */
MMWP : 1, /* Machine Mode Whitelist Policy */
MML : 0 /* Machine Mode Lockdown */
}

register mseccfg : Mseccfg_ent

val checkPmpNcfgL : range(0, 63) -> bits(1)

function mseccfgWrite(reg: Mseccfg_ent, v: bits(64)) -> Mseccfg_ent = {
let legal_v : Mseccfg_ent = Mk_Mseccfg_ent(zero_extend(v[2 .. 0]));
let reg : Mseccfg_ent = match (reg[RLB], legal_v[RLB], checkPmpNcfgL(63)) {
// to set RLB, need to check PMPCFG_L
(0b0, 0b1, 0b1) => reg,
(_, _, _) => [reg with RLB = legal_v[RLB]],
};
let reg : Mseccfg_ent = match (reg[MML], reg[MMWP]) {
// Implements stickiness of MML bit, if once set remains set
(0b0, 0b0) => [reg with MMWP = legal_v[MMWP], MML = legal_v[MML]],
(0b0, 0b1) => [reg with MML = legal_v[MML]],
(0b1, 0b0) => [reg with MMWP = legal_v[MMWP]],
(0b1, 0b1) => reg
};
reg
}

mapping clause csr_name_map = 0x747 <-> "mseccfg"
mapping clause csr_name_map = 0x757 <-> "mseccfgh"

function clause is_CSR_defined(0x747) = sys_has_mseccfg()
function clause is_CSR_defined(0x757) = sys_has_mseccfg() & xlen == 32

function clause read_CSR(0x747) = mseccfg.bits[xlen - 1 .. 0]
function clause read_CSR(0x757 if xlen == 32) = mseccfg.bits[63 .. 32]

// Keep a consistent writing style, as it may be necessary to integrate the ifs process into the writeCSR function body in the future
function clause write_CSR((0x747, value) if xlen == 64) = { mseccfg = mseccfgWrite(mseccfg, value); mseccfg.bits }
function clause write_CSR((0x747, value) if xlen == 32) = { mseccfg = mseccfgWrite(mseccfg, mseccfg.bits[63 .. 32] @ value); mseccfg.bits[xlen - 1 .. 0] }
function clause write_CSR((0x757, value) if xlen == 32) = { mseccfg = mseccfgWrite(mseccfg, value @ mseccfg.bits[31 .. 0]); mseccfg.bits[63 .. 32] }

/* interrupt processing state */

bitfield Minterrupts : xlenbits = {
Expand Down

0 comments on commit cf51e2e

Please sign in to comment.