diff --git a/c_emulator/riscv_platform.c b/c_emulator/riscv_platform.c index ae67bac42..dc8146094 100644 --- a/c_emulator/riscv_platform.c +++ b/c_emulator/riscv_platform.c @@ -87,6 +87,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; diff --git a/c_emulator/riscv_platform.h b/c_emulator/riscv_platform.h index fe81c901b..7c84a1555 100644 --- a/c_emulator/riscv_platform.h +++ b/c_emulator/riscv_platform.h @@ -18,6 +18,7 @@ uint64_t sys_pmp_grain(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); diff --git a/c_emulator/riscv_platform_impl.c b/c_emulator/riscv_platform_impl.c index 2713715cc..0b6efc4e0 100644 --- a/c_emulator/riscv_platform_impl.c +++ b/c_emulator/riscv_platform_impl.c @@ -19,6 +19,7 @@ bool rv_enable_vext = true; bool rv_enable_bext = false; bool rv_enable_zicbom = false; bool rv_enable_zicboz = false; +bool rv_enable_smepmp = false; bool rv_enable_dirty_update = false; bool rv_enable_misaligned = false; diff --git a/c_emulator/riscv_platform_impl.h b/c_emulator/riscv_platform_impl.h index 8bda5e624..515ef697b 100644 --- a/c_emulator/riscv_platform_impl.h +++ b/c_emulator/riscv_platform_impl.h @@ -29,6 +29,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; diff --git a/c_emulator/riscv_sim.c b/c_emulator/riscv_sim.c index 78838462a..c68b5e965 100644 --- a/c_emulator/riscv_sim.c +++ b/c_emulator/riscv_sim.c @@ -59,6 +59,7 @@ enum { OPT_ENABLE_ZICBOM, OPT_ENABLE_ZICBOZ, OPT_CACHE_BLOCK_SIZE, + OPT_ENABLE_SMEPMP, }; static bool do_dump_dts = false; @@ -155,6 +156,7 @@ static struct option options[] = { {"enable-zfinx", no_argument, 0, 'x' }, {"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 }, @@ -334,6 +336,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; diff --git a/model/riscv_csr_begin.sail b/model/riscv_csr_begin.sail index 053776435..a22d8cbdc 100644 --- a/model/riscv_csr_begin.sail +++ b/model/riscv_csr_begin.sail @@ -158,6 +158,8 @@ mapping clause csr_name_map = 0x342 <-> "mcause" mapping clause csr_name_map = 0x343 <-> "mtval" mapping clause csr_name_map = 0x344 <-> "mip" /* machine protection and translation */ +mapping clause csr_name_map = 0x747 <-> "mseccfg" +mapping clause csr_name_map = 0x757 <-> "mseccfgh" mapping clause csr_name_map = 0x3A0 <-> "pmpcfg0" mapping clause csr_name_map = 0x3A1 <-> "pmpcfg1" mapping clause csr_name_map = 0x3A2 <-> "pmpcfg2" diff --git a/model/riscv_insts_zicsr.sail b/model/riscv_insts_zicsr.sail index 5e4d47b9e..c70f9696f 100644 --- a/model/riscv_insts_zicsr.sail +++ b/model/riscv_insts_zicsr.sail @@ -51,6 +51,9 @@ function clause read_CSR(0x342) = mcause.bits function clause read_CSR(0x343) = mtval function clause read_CSR(0x344) = mip.bits +function clause read_CSR(0x747) = mseccfg.bits +function clause read_CSR(0x757 if xlen == 32) = mseccfgh + // pmpcfgN function clause read_CSR(0x3A @ idx : bits(4) if idx[0] == bitzero | xlen == 32) = pmpReadCfgReg(unsigned(idx)) // pmpaddrN. Unfortunately the PMP index does not nicely align with the CSR index bits. @@ -133,6 +136,8 @@ function clause write_CSR(0x3D @ idx : bits(4), value) = { let idx = unsigned(0b function clause write_CSR(0x3E @ idx : bits(4), value) = { let idx = unsigned(0b11 @ idx); pmpWriteAddrReg(idx, value); pmpReadAddrReg(idx) } /* machine mode counters */ +function clause write_CSR(0x747, value) = { mseccfg = mseccfgWrite(mseccfg, value); mseccfg.bits } +function clause write_CSR((0x757, value) if xlen == 32) = { mseccfgh } function clause write_CSR(0xB00, value) = { mcycle[(xlen - 1) .. 0] = value; value } function clause write_CSR(0xB02, value) = { minstret[(xlen - 1) .. 0] = value; minstret_increment = false; value } function clause write_CSR((0xB80, value) if xlen == 32) = { mcycle[63 .. 32] = value; value } diff --git a/model/riscv_pmp_control.sail b/model/riscv_pmp_control.sail index 433fd6606..b6408e491 100644 --- a/model/riscv_pmp_control.sail +++ b/model/riscv_pmp_control.sail @@ -48,14 +48,43 @@ function pmpCheckRWX(ent, acc) = { } } -// this needs to be called with the effective current privilege. +/* 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) = { - match priv { - Machine => if pmpLocked(ent) - then pmpCheckRWX(ent, acc) - else true, - _ => pmpCheckRWX(ent, acc) + if sys_has_mseccfg() & 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 + }, + (_, _, _, _) => + if (priv == Machine) == pmpLockBit(ent) + then pmpCheckRWX(ent, acc) + else false + } + } + else{ + match priv { + Machine => + if pmpLockBit(ent) + then pmpCheckRWX(ent, acc) + else true, + _ => pmpCheckRWX(ent, acc) + } } } @@ -123,7 +152,18 @@ function pmpCheck forall 'n, 'n > 0. (addr: xlenbits, width: int('n), acc: Acces PMP_Continue => (), } }; - if priv == Machine then None() else Some(accessToFault(acc)) + if priv == Machine + then { + if sys_has_mseccfg() & mseccfg[MMWP] == 0b1 /* Make Read, Write and execute denied by default, if condition meets for M mode */ + then Some(accessToFault(acc)) + else if sys_has_mseccfg() & mseccfg[MML] == 0b1 /* Make execute denied, if condition meets for M mode */ + then match acc { + Execute(_) => Some(accessToFault(acc)), + _ => None() + } + else None() + } + else Some(accessToFault(acc)) } function init_pmp() -> unit = { @@ -132,6 +172,9 @@ function init_pmp() -> unit = { "sys_pmp_count() must be 0, 16, or 64" ); + mseccfg = [mseccfg with MML = 0b0, MMWP = 0b0, RLB = 0b0]; + mseccfgh = zero_extend(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. diff --git a/model/riscv_pmp_regs.sail b/model/riscv_pmp_regs.sail index 3764f3533..6561dd7dc 100644 --- a/model/riscv_pmp_regs.sail +++ b/model/riscv_pmp_regs.sail @@ -43,6 +43,15 @@ bitfield Pmpcfg_ent : bits(8) = { register pmpcfg_n : vector(64, Pmpcfg_ent) register pmpaddr_n : vector(64, xlenbits) +bitfield Mseccfg_ent : xlenbits = { + RLB : 2, /* Rule Locking Bypass */ + MMWP : 1, /* Machine Mode Whitelist Policy */ + MML : 0 /* Machine Mode Lockdown */ +} + +register mseccfg : Mseccfg_ent +register mseccfgh : bits(32) + /* Packing and unpacking pmpcfg regs for xlen-width accesses */ function pmpReadCfgReg(n : range(0, 15)) -> xlenbits = { @@ -89,32 +98,48 @@ function pmpReadAddrReg(n : range(0, 63)) -> xlenbits = { } /* Helpers to handle locked entries */ -function pmpLocked(cfg: Pmpcfg_ent) -> bool = - cfg[L] == 0b1 +function pmpLockBit(cfg: Pmpcfg_ent) -> bool = cfg[L] == 0b1 -function pmpTORLocked(cfg: Pmpcfg_ent) -> bool = - (cfg[L] == 0b1) & (pmpAddrMatchType_of_bits(cfg[A]) == TOR) +function pmpLocked(cfg: Pmpcfg_ent) -> bool = (cfg[L] == 0b1) & (mseccfg[RLB] == 0b0) -function pmpWriteCfg(n: range(0, 63), cfg: Pmpcfg_ent, v: bits(8)) -> Pmpcfg_ent = - if pmpLocked(cfg) then cfg - else { - // Bits 5 and 6 are zero. - let cfg = Mk_Pmpcfg_ent(v & 0x9f); +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 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 { + /* Constructing legal Pmpcfg_ent by making bit 5 and 6 zero */ + let legal_v : Pmpcfg_ent = Mk_Pmpcfg_ent(v & 0x9f); // "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 @@ -146,3 +171,27 @@ function pmpWriteAddrReg(n : range(0, 63), v : xlenbits) -> unit = { v, ); } + +function checkPmpNcfgL(n : range(0, 63)) -> bool = { + if n == 0 + then pmpcfg_n[0][L] == 0b1 + else checkPmpNcfgL(n - 1) | (pmpcfg_n[n][L] == 0b1) +} + +function mseccfgWrite(reg: Mseccfg_ent, v: xlenbits) -> 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]) { /* to set RLB, need to check PMPCFG_L */ + (0b0, 0b1) => + if (checkPmpNcfgL(63)) + then reg + else update_RLB(reg, legal_v[RLB]), + (_, _) => update_RLB(reg, 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 +} diff --git a/model/riscv_sys_control.sail b/model/riscv_sys_control.sail index 6379f5676..d318456bc 100644 --- a/model/riscv_sys_control.sail +++ b/model/riscv_sys_control.sail @@ -46,6 +46,8 @@ function clause is_CSR_defined(0x342) = true // mcause function clause is_CSR_defined(0x343) = true // mtval function clause is_CSR_defined(0x344) = true // mip +function clause is_CSR_defined(0x747) = sys_has_mseccfg() // mseccfg +function clause is_CSR_defined(0x757) = sys_has_mseccfg() & (xlen == 32) // mseccfgh // pmpcfgN function clause is_CSR_defined(0x3A) @ idx : bits(4) = sys_pmp_count() > unsigned(idx) & (idx[0] == bitzero | xlen == 32) diff --git a/model/riscv_sys_regs.sail b/model/riscv_sys_regs.sail index e7ca84887..a6cadf2cf 100644 --- a/model/riscv_sys_regs.sail +++ b/model/riscv_sys_regs.sail @@ -105,6 +105,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