Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Added support of Smepmp #601

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Added support of Smepmp #601

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 5 additions & 0 deletions c_emulator/riscv_platform.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions c_emulator/riscv_platform_impl.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
6 changes: 6 additions & 0 deletions c_emulator/riscv_sim.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,7 @@ enum {
OPT_ENABLE_ZICBOM,
OPT_ENABLE_ZICBOZ,
OPT_CACHE_BLOCK_SIZE,
OPT_ENABLE_SMEPMP,
};

static bool do_dump_dts = false;
Expand Down Expand Up @@ -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 },
Expand Down Expand Up @@ -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;
Expand Down
2 changes: 2 additions & 0 deletions model/riscv_csr_begin.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
5 changes: 5 additions & 0 deletions model/riscv_insts_zicsr.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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 }
Expand Down
57 changes: 50 additions & 7 deletions model/riscv_pmp_control.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 */
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

// style comments are nicer IMO. I don't see why we would change them back?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is the part that was changed by @HamzaKh01, I didn't check this as I was too focused on the code implementation part, we can change it back if needed, but there are many one line comments like /* ... */ in Sail, we might need to declare it better in the codestyle after some discussion?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah there is an experimental auto-formatter in the Sail compiler but I don't know what state it got to and I'd guess it doesn't change this sort of thing.

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

Expand Down Expand Up @@ -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 = {
Expand All @@ -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.
Expand Down
79 changes: 64 additions & 15 deletions model/riscv_pmp_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Normally we don't treat this as a separate register, we just make bitfield Mseccfg : bits(64) and then read/write the appropriate bits of it.

We have an implementation of mseccfg like that internally; I'll make a PR for it.


/* Packing and unpacking pmpcfg regs for xlen-width accesses */

function pmpReadCfgReg(n : range(0, 15)) -> xlenbits = {
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
}
2 changes: 2 additions & 0 deletions model/riscv_sys_control.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
5 changes: 5 additions & 0 deletions model/riscv_sys_regs.sail
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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()
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You can implement mseccfg even if you don't have any of the extensions that use it (and that isn't a weird edge case). So ideally this would be

// Callback to C
val sys_have_mseccfg : "sys_have_mseccfg" unit -> bool

function have_mseccfg() -> bool = sys_have_mseccfg() | sys_enable_smepmp() | sys_enable_zkr() ...

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You mean we need to add an extra command line parameter to act as an extra switch to control the presence of mseccfg to make sure that even if we don't implement extensions that use this register, we can still implement this register, right ?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yeah exactly. I don't think we need to actually bother hooking it up to a CLI arguments at the moment - we can wait until Alasdair's new config system exists and then it will be a whole lot less tedious. But we can just have a function that returns true as a placeholder so we don't forget.


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

Expand Down
Loading