CTSRD-CHERI / cheri-specification

CHERI ISA Specification
Other
20 stars 6 forks source link

CHERI global enable/disable #69

Open tariqkurd-repo opened 1 year ago

tariqkurd-repo commented 1 year ago

Other RISC-V extensions which add state to the machine (F and V) each have two bits allocated in mstatus/sstatus for lazy context save/restore, and also to restrict access to the new state.

To be added in a regular way, CHERI should have the same, as it exends the register file and adds new SCRs/CSRs and instructions (F and V both add all three categories). Therefore I propose allocating bits [24:23] of mstatus/status to be CS[1:0] with the same spec as FS, VS, XS.

0 = Off     -> CHERI fully disabled - as if it wasn't implemented
1 = Initial -> CHERI enabled - so all checks are permenantly enabled
2 = Clean   -> CHERI enabled - so all checks are permenantly enabled
3 = Dirty   -> CHERI enabled - so all checks are permenantly enabled

As an additional note the Smstateen extension says:

Each bit of a stateen CSR controls less-privileged access to an extension’s state, 
for an extension that was not deemed "worthy" of a full XS field in sstatus like 
the FS and VS fields for the F and V extensions.

Therefore I'm saying that CHERI is worthy of a field in Xstatus.

A useful side-effect of doing this is that it should help with the instruction definitions for inclusion into RISC-V to show that CHERI is an incremental addition and not a replacement for parts of the architecture. As a specific example to extend conditional branches to take a CHERI exception if taken and the target is out-of-bounds then I've taken the standard SAIL function add added some example extra code. I believe that we will be required to have the additional code gated like this to prove that there are no side-effects and so that CHERI can be 100% backwards compatible in this way. This approach is fundamental to my CHERI is not a separate universe argument. If the new code is fully disabled then then there's no doubt about backwards compatibility.

Here's some example SAIL code extended to include CHERI checking (I'm not saying we need to rewrite SAIL in this way, this is just to show how CHERI extends the existing RISC-V machine):

function clause execute (BTYPE(imm, rs2, rs1, op)) = {
  let rs1_val = X(rs1);
  let rs2_val = X(rs2);
  let taken : bool = match op {
    RISCV_BEQ  => rs1_val == rs2_val,
    RISCV_BNE  => rs1_val != rs2_val,
    RISCV_BLT  => rs1_val <_s rs2_val,
    RISCV_BGE  => rs1_val >=_s rs2_val,
    RISCV_BLTU => rs1_val <_u rs2_val,
    RISCV_BGEU => rs1_val >=_u rs2_val
  };
  let t : xlenbits = PC + EXTS(imm);
  if taken then {

  // Start of CHERI addition
  if mstatus.CS!=Off {
    if not(inCapBounds(PCC, t, minimum_instruction_bytes())) then {
       <take exception>
       RETIRE_FAIL
     }
   }
   // End of CHERI addition

    // Extensions get the first checks on the prospective target address.
    match ext_control_check_pc(t) {
      Ext_ControlAddr_Error(e) => {
        ext_handle_control_check_error(e);
        RETIRE_FAIL
      },
      Ext_ControlAddr_OK(target) => {
        if bit_to_bool(target[1]) & not(haveRVC()) then {
          handle_mem_exception(target, E_Fetch_Addr_Align());
          RETIRE_FAIL;
        } else {
          set_next_pc(target);
          RETIRE_SUCCESS
        }
      }
    }
  } else RETIRE_SUCCESS
}
jrtc27 commented 1 year ago

The two bit approach doesn’t make sense given CHERI capabilities extend the integer register file. Note that we used to have a dirty bit in xccsr but it was in practice hardwired to 1 and so got removed; we do not want to be adding back some notion of dirty.

What you want is a lone bit that enables the instructions and SCR access.

tariqkurd-repo commented 1 year ago

That's fair comment, unlike F and V which may/may not be used CHERI is expected to always be used, at least for the highest level of software (or you chose the wrong core). maybe we could get 1-bit in mstatus for this.

jrtc27 commented 1 year ago

It's not just about expectation, it's about that if you are using it the 01 and 10 states make little sense, no exception handler is going to conditionally save CHERI or non-CHERI state (more code, and more register pressure to determine the dirty status in the first place) so it's a useless reporting mechanism that just complicates the specification and implementations

jonwoodruff commented 1 year ago

Just to try and document some discussion from our last meeting:

We expect behaviour with an almighty DDC/PCC to be indistinguishable to non-cap-aware programs from a non-capability processor. If this is not the case, we should fix the architecture, as we would like to sandbox non-capability-aware programs using capabilities. This property may need to be proven against the Sail architecture, which should be more desirable than adding an enable bit to the architecture to ensure that it is obvious.

If this is the case, then the "enable" bit is not necessary, but just the privilege-level enable bits for context switching.

There is then a separate question about whether these privilege level enable bits gate access to all capability instructions, or only those that could create a change in capability state...

tariqkurd-repo commented 1 year ago

If we redefine almighty_cap to mean CHERI checks disabled in a simpler manner (to allow the RISC-V memory wrapping case to be compatible) then the proof could be much simpler, as in "bypass the checks" as oppose to "the checks still pass but it's complex to demonstrate that". Again, I think we need that anyway for the memory wrapping case.

By the privilege level enable bits do you mean Xenvcfg? And yes - should they be allowed to use CHERI instructions... it's agood question - non-CHERI aware RISC-V core arguably shouldn't get any extra features added to it