From 6e99c543c80411687234e91a2822230dd94d8e85 Mon Sep 17 00:00:00 2001 From: Nathaniel Wesley Filardo Date: Thu, 12 Nov 2020 00:29:18 +0000 Subject: [PATCH] Introduce load-capability generation traps Co-authored-by: Jessica Clarke --- src/cheri_insts.sail | 55 ++++++++++++++++++++++++++++---------- src/cheri_pte.sail | 50 +++++++++++++++++++++++++++++----- src/cheri_riscv_types.sail | 12 +++++++-- src/cheri_sys_regs.sail | 14 ++++++++++ 4 files changed, 109 insertions(+), 22 deletions(-) diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index e62bc256..b39c16bb 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -1376,11 +1376,25 @@ function handle_load_cap_via_cap(cd, auth_idx, auth_val, vaddrBits) = { let c = mem_read_cap(addr, aq, rl, false); match c { MemValue(v) => { - let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR - then {v with tag = false} /* strip the tag */ - else {v with tag = v.tag & auth_val.permit_load_cap}; - C(cd) = cr; - RETIRE_SUCCESS + match ptw_info.ptw_lc { + PTW_LC_OK => { + C(cd) = { v with tag = v.tag & auth_val.permit_load_cap }; + RETIRE_SUCCESS + }, + PTW_LC_CLEAR => { + C(cd) = { v with tag = false }; + RETIRE_SUCCESS + }, + PTW_LC_TRAP => { + if v.tag then { + handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT)); + RETIRE_FAIL + } else { + C(cd) = v; + RETIRE_SUCCESS + } + } + } }, MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL } } @@ -1607,15 +1621,28 @@ if not(auth_val.tag) then { let c = mem_read_cap(addr, aq, rl, false); match c { MemValue(v) => { - let cr = if ptw_info.ptw_lc == PTW_LC_CLEAR - then {v with tag = false} /* strip the tag */ - else { - /* the Sail model currently reserves virtual addresses */ - load_reservation(addr); - {v with tag = v.tag & auth_val.permit_load_cap} - }; - C(cd) = cr; - RETIRE_SUCCESS + match ptw_info.ptw_lc { + PTW_LC_OK => { + load_reservation(addr); + C(cd) = { v with tag = v.tag & auth_val.permit_load_cap }; + RETIRE_SUCCESS + }, + PTW_LC_CLEAR => { + load_reservation(addr); + C(cd) = { v with tag = false }; + RETIRE_SUCCESS + }, + PTW_LC_TRAP => { + if v.tag then { + handle_mem_exception(vaddrBits, E_Extension(EXC_LOAD_CAP_PAGE_FAULT)); + RETIRE_FAIL + } else { + load_reservation(addr); + C(cd) = v; + RETIRE_SUCCESS + } + } + } }, MemException(e) => {handle_mem_exception(vaddrBits, e); RETIRE_FAIL } } diff --git a/src/cheri_pte.sail b/src/cheri_pte.sail index bff236a5..36d29231 100644 --- a/src/cheri_pte.sail +++ b/src/cheri_pte.sail @@ -31,8 +31,21 @@ bitfield PTE_Bits : pteAttribs = { * state cached and then observe a CW=1 CD=1 PTE, no PTE write is necessary. * On the other hand, if CW=0 is observed, the store operation must trap. * + * The intended semantics for capability loads are as follows. + * + * CR CR_Mod CR_Gen Action + * + * 0 0 0 Capability loads strip tags + * 0 1 0 Capability loads trap (on set tag) + * 0 X 1 [Reserved] + * + * 1 0 0 Capability loads succeed: no traps or tag clearing + * 1 0 1 [Reserved] + * 1 1 G Capability loads trap if G mismatches sccsr.[su]gclg, + * where the compared bit is keyed off of this PTE's U. + * * SV32: There are no extension bits available, so we hard-code the result to - * CW=1 CR=1 CD=1. + * CW=1 CR=1 CD=1 CR_Mod=0 CR_Gen=0 */ type extPte = bits(10) @@ -40,13 +53,17 @@ bitfield Ext_PTE_Bits : extPte = { CapWrite : 9, /* Permit capability stores */ CapRead : 8, /* Permit capability loads */ CapDirty : 7, /* Capability Dirty flag */ + CapRead_Mod : 6, /* Modify capability load prohibition; see above table */ + CapRead_Gen : 5, /* When load-cap gens. are in use, the "local" gen. bit */ } /* * CapWrite = 1, * CapRead = 1, * CapDirty = 1, - * bits 0 .. 6 = 0 + * CapRead_Mod = 0, + * CapRead_Gen = 0, + * bits 0 .. 4 = 0 */ let default_sv32_ext_pte : extPte = 0b1110000000 @@ -57,7 +74,10 @@ function isPTEPtr(p : pteAttribs, ext : extPte) -> bool = { function isInvalidPTE(p : pteAttribs, ext : extPte) -> bool = { let a = Mk_PTE_Bits(p); - a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) + let e = Mk_Ext_PTE_Bits(ext); + a.V() == 0b0 | (a.W() == 0b1 & a.R() == 0b0) | + (e.CapRead() == 0b0 & e.CapRead_Gen() == 0b1) | + (e.CapRead() == 0b1 & e.CapRead_Gen() == 0b1 & e.CapRead_Mod() == 0b0) } union PTE_Check = { @@ -73,6 +93,25 @@ function checkPTEPermission_SC(e, ext_ptw) = { else PTE_Check_Failure(ext_ptw, EPTWF_CAP_ERR) } +/* + * Assuming we're allowed to load from this page, modulate our cap response + */ +val checkPTEPermission_LC : (PTE_Bits, Ext_PTE_Bits, ext_ptw) -> PTE_Check effect { escape, rreg } +function checkPTEPermission_LC(p, e, ext_ptw) = + match (e.CapRead(), e.CapRead_Mod(), e.CapRead_Gen()) { + (0b0, 0b0, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_CLEAR)), /* Clear tag for "unmodified" no-LC case */ + (0b0, 0b1, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_TRAP)), /* Trap on tag load for "modified" no-LC case */ + (0b0, _ , 0b1) => internal_error("Bad PTE not caught by isInvalidPTE"), + (0b1, 0b0, 0b0) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, PTW_LC_OK)), /* Unmodified LC case: go ahead */ + (0b1, 0b0, 0b1) => internal_error("Bad PTE not caught by isInvalidPTE"), + (0b1, 0b1, lclg) => { + /* Compare local CLG against the pte.U-selected, not mode-selected, global CLG bit */ + let gclg : bits(1) = if p.U() == 0b1 then sccsr.ugclg() else sccsr.sgclg(); + let ptwl = if lclg == gclg then PTW_LC_OK else PTW_LC_TRAP; + PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptwl)) + } + } + function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, mxr : bool, do_sum : bool, p : PTE_Bits, ext : extPte, ext_ptw : ext_ptw) -> PTE_Check = { /* * Although in many cases MXR doesn't make sense for capabilities, we honour @@ -123,7 +162,6 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, }; /* Load side */ - let ptw_lc = if e.CapRead() == 0b1 then PTW_LC_OK else PTW_LC_CLEAR; let res : PTE_Check = match res { PTE_Check_Failure(_, _) => res, PTE_Check_Success(ext_ptw) => match ac { @@ -132,8 +170,8 @@ function checkPTEPermission(ac : AccessType(ext_access_type), priv : Privilege, Write(_) => res, ReadWrite(Data, _) => res, - Read(Cap) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc)), - ReadWrite(Cap, _) => PTE_Check_Success(ext_ptw_lc_join(ext_ptw, ptw_lc)) + Read(Cap) => checkPTEPermission_LC(p, e, ext_ptw), + ReadWrite(Cap, _) => checkPTEPermission_LC(p, e, ext_ptw) } }; diff --git a/src/cheri_riscv_types.sail b/src/cheri_riscv_types.sail index ad230fea..29258d92 100644 --- a/src/cheri_riscv_types.sail +++ b/src/cheri_riscv_types.sail @@ -10,7 +10,10 @@ enum ext_ptw_lc = { PTW_LC_OK, /* PTE settings require clearing tags */ - PTW_LC_CLEAR + PTW_LC_CLEAR, + + /* PTE settings require us to trap */ + PTW_LC_TRAP } struct ext_ptw = { @@ -21,7 +24,12 @@ function ext_ptw_lc_join(e : ext_ptw, l : ext_ptw_lc) -> ext_ptw = { e with ptw_lc = match l { PTW_LC_OK => e.ptw_lc, - PTW_LC_CLEAR => l + PTW_LC_CLEAR => match e.ptw_lc { + PTW_LC_OK => PTW_LC_CLEAR, + PTW_LC_CLEAR => PTW_LC_CLEAR, + PTW_LC_TRAP => PTW_LC_TRAP + }, + PTW_LC_TRAP => PTW_LC_TRAP } } diff --git a/src/cheri_sys_regs.sail b/src/cheri_sys_regs.sail index ac4dfffe..6dbac57f 100644 --- a/src/cheri_sys_regs.sail +++ b/src/cheri_sys_regs.sail @@ -3,6 +3,8 @@ /* Capability control csr */ bitfield ccsr : xlenbits = { + ugclg : 3, /* Global Cap Load Gen bit for User pages */ + sgclg : 2, /* Global Cap Load Gen bit for System (not User) pages */ d : 1, /* dirty */ e : 0 /* enable */ } @@ -16,6 +18,18 @@ function legalize_ccsr(p : Privilege, c : ccsr, v : xlenbits) -> ccsr = { // write only the defined bits, leaving the other bits untouched let v = Mk_ccsr(v); + let c : ccsr = match p { + User => { + // No bits defined for uccsr + c + }, + _ => { + let c = update_ugclg(c, v.ugclg()); + let c = update_sgclg(c, v.sgclg()); + c + } + }; + /* For now these bits are not really supported so hardwired to true */ let c = update_d(c, 0b1); let c = update_e(c, 0b1);