added command line support for Smepmp. command line switch: --enable-…

…smepmp. Sail function: haveSmepmp

Added support of Smepmp

Co-authored-by: William McSpaddden <[email protected]>
Co-authored-by: Hamza Khan <[email protected]>

c_emulator/riscv_platform.c

@@ -92,6 +92,11 @@ uint64_t sys_vector_elen_exp(unit)
   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;

c_emulator/riscv_platform.h

@@ -19,6 +19,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);

c_emulator/riscv_platform_impl.c

@@ -20,6 +20,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;

c_emulator/riscv_platform_impl.h

@@ -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;

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;
@@ -156,6 +157,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       },
@@ -336,6 +338,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;

doc/Status.md

@@ -19,6 +19,8 @@ The Sail specification currently captures the following ISA features:
 
 - Physical Memory Protection (PMP)
 
+- PMP Enhancements for memory accesses and execution prevention on Machine mode (Smepmp)
+
 For the RVWMO memory consistency model, this Sail ISA semantics is integrated with the RVWMO operational model in [the
 RMEM tool](https://github.com/rems-project/rmem).
 

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"

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 }

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.

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
+}

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)
 

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