Added support of Smepmp

README.md

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

c_emulator/riscv_platform.c

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

c_emulator/riscv_platform.h

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

c_emulator/riscv_platform_impl.c

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

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

@@ -54,6 +54,7 @@ enum {
   OPT_ENABLE_ZICBOZ,
   OPT_ENABLE_SSTC,
   OPT_CACHE_BLOCK_SIZE,
+  OPT_ENABLE_SMEPMP,
 };
 
 static bool do_show_times = false;
@@ -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       },
@@ -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;

model/riscv_pmp_control.sail

@@ -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 */
 
@@ -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 */
 
@@ -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
   }
@@ -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 = {
@@ -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.

model/riscv_pmp_regs.sail

@@ -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
@@ -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])
+}

model/riscv_sys_regs.sail

@@ -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
 
@@ -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 = {