diff --git a/archdoc/app-isaquick-riscv.tex b/archdoc/app-isaquick-riscv.tex index f636b3f..63396ab 100644 --- a/archdoc/app-isaquick-riscv.tex +++ b/archdoc/app-isaquick-riscv.tex @@ -96,7 +96,6 @@ \chapter{Instruction encoding summary} \optype{Control-Flow} No special new control flow instructions are added, although RISC-V \texttt{JAL} / \texttt{JALR} become capability instructions \rvcheriasminsnref{CJAL} / \rvcheriasminsnref{CJALR}. - The branch instructions also check that \PCC{} permits at least one 2-byte instruction to be loaded from the target address, otherwise they raise a capability bounds exception. \optype{Memory-Access} \label{quickref:mem} diff --git a/archdoc/chap-changes.tex b/archdoc/chap-changes.tex index f04e85e..952d6e5 100644 --- a/archdoc/chap-changes.tex +++ b/archdoc/chap-changes.tex @@ -12,6 +12,15 @@ \chapter{Version history} Tag clearing is preferable for software because it removes the possibility of a trap when copying untrusted inputs. It is also likely easier to implement in hardware. The capability exception code that was previously used for this (0x16) is now reserved. - \item[] The relocations for \insnref{auicgp} and \insnref{auipcc} are unified and the CHERIoT-specific relocations are now named with CHERIOT, rather than CHERI, as the prefix. + \item[\ghpr{33}] The relocations for \insnref{auicgp} and \insnref{auipcc} are unified and the CHERIoT-specific relocations are now named with CHERIOT, rather than CHERI, as the prefix. + \item[\ghissue{23}, \ghissue{18}, \ghpr{37}] Jumps and branches no longer include bounds checks. + Instead, any \PCC{} bounds error will be detected on the subsequent instruction fetch at the target. + To avoid problems with unrepresentable capabilities the tag of the value stored in \EPCC{} is cleared for instruction fetch bounds exceptions. + \item[\ghissue{30}, \ghpr{37}] Validate \MEPCC{} and \MTCC{} on write. + If either of these is written with a sealed or non-executable capability then the tag is cleared. + If the least significant bit of \MEPCC{}.\caddress{} is set on write then it is cleared and the tag is cleared. + If either of the two least significant bits of \MTCC{}.\caddress{} is set on write then they are cleared and the tag is cleared. + This simplifies both ISA and hardware and avoids potential violations of capability monotonicity due to \asm{mtvec} and \asm{mepc} legalization. + vectored interrupt mode is explicitly unsupported. \end{description} \end{description} diff --git a/archdoc/chap-cheri-riscv.tex b/archdoc/chap-cheri-riscv.tex index 2264ab0..142d3a0 100644 --- a/archdoc/chap-cheri-riscv.tex +++ b/archdoc/chap-cheri-riscv.tex @@ -54,16 +54,22 @@ \section{Instruction encodings} \section{Changes to instruction fetch / control flow} The program counter is extended to a capability, \PCC{}, with \PCC{}.\caddress{} assuming the role of the \PC{}. -If \PCC{} is untagged, sealed, lacks \cappermX, or the instruction is not entirely within the bounds of \PCC{}, then an exception is raised. +If \PCC{} becomes untagged or the instruction is not entirely within the bounds of \PCC{}, then an exception is raised. Note that the bounds check must take account of whether the fetched instruction is 2 or 4 bytes. -Checks on jumps and branches mean the only way for \PCC{} to be untagged, sealed or non-executable is after an \asm{MRET} with an invalid \asm{MEPCC} or a trap with an invalid \asm{MTCC}. - -\insnriscvref{CJAL} and taken branch instructions check the destination address against the bounds of \PCC{}: if the bounds do not permit at least one 2-byte instruction to be loaded from the destination then a capability length violation exception is raised on the jump / branch instruction. +If the program counter is outside the bounds of \PCC{} it might be unrepresentable in the compressed capability format (\cref{sec:bounds,sec:repcheck}). +Therefore, to avoid violating capability monotonicity the value written to \MEPCC{} when there is an instruction fetch bounds violation has its tag cleared. +Due to unrepresentability the bounds of \MEPCC{} might not correspond to the bounds of \PCC{} at the time of the exception in this case. \insnriscvref{CJALR} replaces the \asm{JALR} instruction and uses capabilities for the target and link register. -It checks that the target capability is tagged, unsealed, executable and the address is in bounds before it is installed in \PCC{}. -If the target is sealed with the reserved `sentry' type then it is unsealed before jumping to it. -The link register, including the current \PCC{}, is sealed as a sentry. +It checks that the target capability is tagged and executable before it is installed in \PCC{}. +If the target is sealed with one of the reserved `sentry' types then it is unsealed before jumping to it, while possibly writing \asm{mstatus.MIE} (see \cref{sec:sealing}). +If it is sealed with a non-sentry type an exception is raised. + +The link register written by \insnriscvref{CJAL} and \insnref{CJALR} is sealed as a sentry of the type corresponding to the current value of \asm{mstatus.MIE}. + +The checks on \insnriscvref{CJALR} and special capability writes (\cref{sec:scrs}) prevent execution with a \PCC{} that is sealed or lacks \cappermX{}. +The only ways for \PCC{} to become untagged is by \asm{MRET} with an untagged \MEPCC{} or exception with untagged \MTCC{}. +The latter will result in an unrecoverable exception loop. \section{Changes to memory accesses} @@ -144,20 +150,12 @@ \section{Controlling access to system registers} \section{Special capability registers} \label{subsection:cheri-riscv-scrs} +\label{sec:scrs} -Special Capability Registers (SCRs) are similar to CSRs in that they affect special functions such as exception delivery, except that they contain capabilities rather than integers. -SCRs are accessed via a new instruction, \insnriscvref{CSpecialRW}, which behaves similarly to the RISC-V \asm{CSRRW} instruction. +Special Capability Registers (SCRs) are similar to RISC-V's Control and Status Registers (CSRs) except that they contain capabilities rather than integers. +They are accessed via a new instruction, \insnriscvref{CSpecialRW}, which behaves similarly to the RISC-V \asm{CSRRW} instruction. \asm{CSpecialRW} requires that \PCC{} has \cappermASR{}, otherwise it will raise an exception. -Some SCRs replace existing RISC-V CSRs. -Attempting to access the legacy RISC-V CSR via the \asm{CSR*} instructions results in a Reserved Instruction exception. -Any special meaning or behavior associated with the CSR applies to the SCR's address field. -For example, the lower two bits of \MTCC{}.\caddress{} select the trap mode, and the remaining bits (including the capability metadata) form the trap base address in the same way as \mtvec{}. -Some RISC-V CSRs have write-any read-legal (WARL) bits that implicitly modify the written value to restrict the CSR to legal values. -This legalization must be applied to the SCR's address when reading or writing an SCR. -If this results in the capability becoming unrepresentable then the tag is cleared, as per \insnriscvref{CSetAddr}. -If a sealed capability is written to an SCR with WARL bits then the tag is cleared, even if the bits would be unchanged by legalization. - \cref{tab:risc-v-special-capability-registers} lists the SCRs and their properties: \textbf{Reset} indicates the reset value as one of the capability roots defined in \cref{sec:capenc}. @@ -177,12 +175,33 @@ \section{Special capability registers} } \end{table} +The \MTCC{} and \MEPCC{} SCRs replace existing RISC-V CSRs \asm{mtvec} and \asm{mepcc} respectively. +Attempting to access the legacy RISC-V CSR via the \asm{CSR*} instructions results in a Reserved Instruction exception. +The special meaning associated with the CSR applies to the SCR's \caddress{} field and the value written is validated and legalized as follows: + +\begin{description} + \item[\MTCC{}] Only direct mode is suppported (not vectored). + If either of the two least significant bits of the \caddress{} is set then they are cleared and the tag of the value written is cleared. + If the capability being written is sealed or does not have \cappermX{} then its tag is cleared. + \item[\MEPCC{}] + If the least significant bit of \caddress{} is set then it is cleared and the tag is cleared. + If the capability being written is sealed or does not have \cappermX{} then its tag is cleared. +\end{description} + +These rules avoid potential problems due to legalisation where capabilities might become unrepresentable or sealed capabilties modified. + \section{Changes to exception handling} Exception handling is the same as RISC-V except that \mtvec{} and \mepc{} are replaced by their equivalent SCRs. -When taking an exception the current \PCC{}, with the address set to that of the trapping instruction, is placed in \MEPCC{}. \MTCC{} is then installed in \PCC{} and execution proceeds from the configured trap address according to the usual rules for \mtvec{}. + +When taking an exception the current \PCC{}, with the address set to that of the trapping instruction, is placed in \MEPCC{}. +If the exception is a bounds violation on instruction fetch then the tag on \MEPCC{} is cleared. +\MTCC{} is then installed in \PCC{} and execution proceeds from \MTCC.\caddress{}. When executing an \asm{MRET} instruction \MEPCC{} is moved to \PCC{} and execution proceeds from \MEPCC{}.\caddress{}. +In either case if the new \PCC{} is untagged (due to an untagged \MEPCC{} or \MTCC{}) an CHERI tag violation exception is raised for the new \PC{}. +In the case of an untagged \MTCC{} this will result in an unrecoverable exception loop. + A new RISC-V exception code, 0x1C, is used for all CHERI specific exceptions, with a more detailed CHERI cause placed in \mtval{} as shown in \cref{fig-cheri-tval}. \label{subsubsec-cheri-tval} @@ -605,14 +624,13 @@ \subsection{Representability checks} Note that although \insnriscvref{CJAL} and \insnriscvref{CJALR} also set the address on the link register, it is guaranteed to be representable because its \caddress{} can be at most equal to \PCC{}.\ctop{} given that the jump itself is in bounds. Therefore no representability check is required for these instructions. -Similarly, the value placed in \MEPCC{} on exception should always be representable given that \PC{} is always in bounds (or equal to \PCC{}.\ctop{} in the case of stepping off the end of \PCC{}). -One exception to this is if \MTCC{} is configured in vectored mode and a subsequent exception goes to a \PC{} that is out of the bounds of \MTCC{}. -This would cause a \PCC{} bounds exception and in this case \MEPCC{} might not be representable, in which case its tag should be cleared. -It may be preferable not to support vectored mode, although note that care should also be taken when legalizing \asm{mtvec} (\MTCC.\caddress{}) to ensure that this does not violate sealing or representability. -legalization of \asm{mepc} (clearing the least significant bit) may also cause values read from \MEPCC{} to be unrepresentable if it has been written with an unaligned address. -This includes the implicit read by \asm{MRET}. -In these cases the unrepresentable \MEPCC{} that results from the \PCC{} bounds exception should have its tag cleared. -\TODO{These cases are probably pretty annoying for hardware. Although less in keeping with RISC-V behavior it would probably be easier to clear tag if \MEPCC{} is written with an unaligned address.} +Bounds exceptions on instruction fetch might result in an unrepresentable \MEPCC{}. +To simplify hardware while preserving capability monotonicity the tag of \MEPCC{} is always cleared on instruction fetch bounds violations. +This unrepresentability might mean that the decoded bounds of \MEPCC{} do not match the bounds of \PCC{} at the time of the exception, +but \MEPCC{}.\caddress{} will contain the address of the faulting instruction or instruction fetch. + +Validation of \MTCC{} and \MEPCC{} in \insnriscvref{CSpecialRW} prevents potential unrepresentability due to the legalisation of \asm{mtvec} and \asm{mepc}. +To simplify hardware these special registers are validated on write, with violations clearing the tag of the value stored (\cref{sec:scrs}). \subsection{The NULL capability} \label{sec:null} diff --git a/src/cheri_addr_checks.sail b/src/cheri_addr_checks.sail index ba2fbbe..e5a18a4 100644 --- a/src/cheri_addr_checks.sail +++ b/src/cheri_addr_checks.sail @@ -130,8 +130,15 @@ function ext_fetch_check_pc(start_pc, pc) = { } } -function ext_handle_fetch_check_error(e : ext_fetch_addr_error) -> unit = +function ext_handle_fetch_check_error(e : ext_fetch_addr_error) -> unit = { + if e == CapEx_BoundsViolation then { + // Always clear the tag on PCC when taking a bounds violation on fetch. + // This avoids having to do a representability check on MEPCC + // when the PC goes out of bounds. + PCC = clearTag(PCC); + }; handle_cheri_pcc_exception(e) +} /* CHERI control address checks */ @@ -139,26 +146,18 @@ type ext_control_addr_error = (CapEx, capreg_idx) /* the control address is derived from a non-PC register, e.g. in JALR */ function ext_control_check_addr(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = { - /* We are given the addr without any bit[0] clearing, so the addition - * below may include a set addr[0], and so the bounds checks should - * be accurate. - */ - let target : xlenbits = [pc with 0=bitzero]; - if not(inCapBounds(PCC, target, min_instruction_bytes ())) - then Ext_ControlAddr_Error(CapEx_BoundsViolation, PCC_IDX) - else Ext_ControlAddr_OK(target) + // We used to do bounds check here but this is now performed only on + // instruction fetch + Ext_ControlAddr_OK(pc) } /* the control address is derived from the PC register, e.g. in JAL */ function ext_control_check_pc(pc : xlenbits) -> Ext_ControlAddr_Check(ext_control_addr_error) = { - if not(inCapBounds(PCC, pc, min_instruction_bytes ())) - then Ext_ControlAddr_Error(CapEx_BoundsViolation, PCC_IDX) - else Ext_ControlAddr_OK(pc) + Ext_ControlAddr_OK(pc) } function ext_handle_control_check_error(err : ext_control_addr_error) -> unit = { - let (capEx, regnum) = err; - handle_cheri_cap_exception(capEx, regnum) + internal_error(__FILE__, __LINE__, "ext_handle_control_check_error should be unreachable") } /* CHERI data address checks */ diff --git a/src/cheri_insts.sail b/src/cheri_insts.sail index 314f10b..d7bb73b 100644 --- a/src/cheri_insts.sail +++ b/src/cheri_insts.sail @@ -95,17 +95,20 @@ union clause ast = CJAL : (bits(21), regidx) * ## Exceptions * * An exception is raised if: - * - **PCC**.**address** $+$ *imm* $\lt$ **PCC**.**base**. - * - **PCC**.**address** $+$ *imm* $+$ min_instruction_bytes $\gt$ **PCC**.**top**. * - **PCC**.**address** $+$ *imm* is unaligned, ignoring bit 0. + * + * ## Notes + * - This instruction no longer attempts to check that the destination is + * within the bounds of PCC. In that case an exception will be raised + * raised by the subsequent instruction fetch. EPCC will have the new + * PC as address but will have the tag cleared due to the possibility of + * creating an unrepresentable PCC. The bounds of EPCC will be + * undefined. */ function clause execute(CJAL(imm, cd)) = { let off : xlenbits = sign_extend(imm); let newPC = PC + off; - if not(inCapBounds(PCC, newPC, min_instruction_bytes())) then { - handle_cheri_cap_exception(CapEx_BoundsViolation, PCC_IDX); - RETIRE_FAIL - } else if newPC[1] == bitone & ~(haveRVC()) then { + if newPC[1] == bitone & ~(haveRVC()) then { handle_mem_exception(newPC, E_Fetch_Addr_Align()); RETIRE_FAIL } else { @@ -133,10 +136,15 @@ union clause ast = CJALR : (bits(12), regidx, regidx) * - *cs1* is sealed and is not a sentry. * - *cs1* is a sentry and *imm* $\ne$ 0. * - *cs1*.**perms** does not grant **Permit_Execute**. - * - *cs1*.**address** $+$ *imm* $\lt$ *cs1*.**base**. - * - *cs1*.**address** $+$ *imm* $+$ min_instruction_bytes $\gt$ *cs1*.**top**. - * - *cs1*.**base** is unaligned. * - *cs1*.**address** $+$ *imm* is unaligned, ignoring bit 0. + * + * ## Notes + * - This instruction no longer attempts to check that the destination is + * within the bounds of PCC. In that case an exception will be raised + * raised by the subsequent instruction fetch. EPCC will have the new + * PC as address but will have the tag cleared due to the possibility of + * creating an unrepresentable PCC. The bounds of EPCC will be + * undefined. */ function clause execute(CJALR(imm, cs1, cd)) = { let cs1_val = C(cs1); @@ -151,9 +159,6 @@ function clause execute(CJALR(imm, cs1, cd)) = { } else if not (cs1_val.permit_execute) then { handle_cheri_reg_exception(CapEx_PermitExecuteViolation, cs1); RETIRE_FAIL - } else if not(inCapBounds(cs1_val, newPC, min_instruction_bytes())) then { - handle_cheri_reg_exception(CapEx_BoundsViolation, cs1); - RETIRE_FAIL } else if newPC[1] == bitone & ~(haveRVC()) then { handle_mem_exception(newPC, E_Fetch_Addr_Align()); RETIRE_FAIL @@ -330,6 +335,10 @@ union clause ast = CSpecialRW : (regidx, screg, regidx) * a separate two-operand CSpecialR instruction and interpret *cs1* being * **C0** as a write of **NULL** if the need to use a temporary capability * register proves to be overly problematic for software. + * + * - MEPCC and MTCC are validated and legalized on write. Any invalid write will + * cause the tag to be cleared which might result in a tag violation + * on instruction fetch following MRET or exception. */ function clause execute (CSpecialRW(cd, scr, cs1)) = { let specialExists : bool = match unsigned(scr) { @@ -346,20 +355,37 @@ function clause execute (CSpecialRW(cd, scr, cs1)) = { handle_cheri_cap_exception(CapEx_AccessSystemRegsViolation, 0b1 @ scr); RETIRE_FAIL } else { - let cs1_val = C(cs1); + var cs1_val = C(cs1); C(cd) = match unsigned(scr) { 28 => MTCC, 29 => MTDC, 30 => MScratchC, - 31 => legalize_epcc(MEPCC), + 31 => MEPCC, _ => {assert(false, "unreachable"); undefined} }; if (cs1 != zeros()) then { match unsigned(scr) { - 28 => MTCC = legalize_tcc(MTCC, cs1_val), + 28 => { + /* Validate that the new MTCC is unsealed, executable and + indicates direct trap mode */ + let invalid = cs1_val.address[1..0] != 0b00 | + isCapSealed(cs1_val) | + not(cs1_val.permit_execute); + /* Legalize MTCC.address / mtvec */ + cs1_val.address[1..0] = 0b00; + MTCC = clearTagIf(cs1_val, invalid) + }, 29 => MTDC = cs1_val, 30 => MScratchC = cs1_val, - 31 => MEPCC = cs1_val, + 31 => { + /* Validate that new MEPCC is aligned, unsealed and executable */ + let invalid = cs1_val.address[0] != bitzero | + isCapSealed(cs1_val) | + not(cs1_val.permit_execute); + /* Legalize MEPCC.address / mepc */ + cs1_val.address[0] = bitzero; + MEPCC = clearTagIf(cs1_val, invalid) + }, _ => assert(false, "unreachable") } }; diff --git a/src/cheri_sys_exceptions.sail b/src/cheri_sys_exceptions.sail index 1f86e78..1aff654 100644 --- a/src/cheri_sys_exceptions.sail +++ b/src/cheri_sys_exceptions.sail @@ -72,8 +72,9 @@ function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) - match p { Machine => { let (representable, mepcc) = setCapAddr(PCC, pc); - /* I think TCC could cause violation of this (see below) */ - assert(representable, "mepcc should always be representable"); + // mepcc might be unrepresentable if this is a bounds violation on PCC. + // In that case PCC should have had the tag cleared in ext_handle_fetch_check_error + assert(representable | not(mepcc.tag)); MEPCC = mepcc }, _ => internal_error(__FILE__, __LINE__,"unsupported") @@ -84,59 +85,46 @@ function handle_trap_extension(p : Privilege, pc : xlenbits, u : option(unit)) - function prepare_trap_vector(p : Privilege, c : Mcause) -> xlenbits = { if p != Machine then internal_error(__FILE__, __LINE__,"unsupported"); let tcc : Capability = MTCC; - - match tvec_addr(Mk_Mtvec(tcc.address), c) { - Some(addr) => { nextPCC = tcc; addr }, /* XXX addr could be unrepresentable or sealing violation! */ - None() => internal_error(__FILE__, __LINE__,"Invalid tvec mode") - } + let v = Mk_Mtvec(tcc.address); + /* MTCC should have been validated and legalized on write. + * Only direct mode is supported */ + match (trapVectorMode_of_bits(v[Mode])) { + TV_Direct => (), + _ => internal_error(__FILE__, __LINE__, "unsupported trap mode"), + }; + nextPCC = tcc; + tcc.address } /* * Get the user-visible ?EPC from ?EPCC. This is not used for control flow, - * just for reads from (integer) CSRs. - * - * See legalize_epcc for a discussion of felicity of readback and note that - * updating EPC with a sentry installed in EPCC is expected to fail, even if - * the update does not change the offset. (However, it would be very unusual - * for software to ever bring the core into such a state except in testing.) + * just for reads from (integer) CSRs. EPCC is validated on write + * so no legalization is required here. */ val get_xret_target : Privilege -> xlenbits effect {escape, rreg} function get_xret_target(p) = { if p != Machine then internal_error(__FILE__, __LINE__,"unsupported"); let cap : Capability = MEPCC; - legalize_xepc(cap.address) + cap.address } /* - * Upon setting any of the ?EPCC values using the (integer) CSRs, derive the - * result using the current contents of EPCC. If that's sealed (esp., a - * sentry) this will de-tag, which won't work out very well. - * - * Legalization is deferred until read. + * Setting mepc via CSRW is not supported. MEPCC should be + * written using CSpecialRW instead. */ val set_xret_target : (Privilege, xlenbits) -> xlenbits effect {escape} function set_xret_target(p, value) = { internal_error(__FILE__, __LINE__,"unsupported"); } +/** + * MEPCC is validated and legalized on write, so this just sets + * up the new PCC and returns new PC. + */ val prepare_xret_target : (Privilege) -> xlenbits effect {rreg, wreg, escape} function prepare_xret_target(p) = { if p != Machine then internal_error(__FILE__, __LINE__,"unsupported"); - - /* Similar to prepare_trap_vector above we need to return the absolute address - destined for PC, rather than the offset (architecutral PC) */ let epcc : Capability = MEPCC; - - let epcc = legalize_epcc(epcc); - - /* - * Sentries unseal on transfer into nextPCC; other sealed types will trap - * with a seal violation later, when we go to do a fetch from nextPCC. - */ - let epcc = if epcc.otype == to_bits(cap_otype_width, otype_sentry) - then unsealCap(epcc) - else epcc; - nextPCC = epcc; epcc.address } diff --git a/src/cheri_sys_regs.sail b/src/cheri_sys_regs.sail index 7d472cc..c59cd69 100644 --- a/src/cheri_sys_regs.sail +++ b/src/cheri_sys_regs.sail @@ -139,43 +139,3 @@ function min_instruction_bytes () -> CapAddrInt = { function haveXcheri () -> bool = /* This is a necessary but not sufficient condition, but should do for now. */ misa.X() == 0b1 - -/*! - * Apply tvec legalization to the address of new tcc when assigning in CSpecialRW. - * If legalisation causes the new tcc to be unrepresentable, or if v is sealed - * then the tag of the new tcc will be cleared. This would cause an infinite - * exception loop if a trap or exception occurred subsequently. - */ -function legalize_tcc(o : Capability, v : Capability) -> Capability = { - /* legalize new TCC offset (RISC-V tvec) */ - new_tvec = v.address; - legalized_tvec = legalize_tvec(Mk_Mtvec(o.address), new_tvec); - setCapAddrChecked(v, legalized_tvec.bits()); -} - -/* - * Used during readout (but not assignment!) of ?EPCC registers (CSpecialRW, - * handle_trap_extension) and during control transfer (prepare_xret_target). - * - * The result is that it is only possible to faithfully read out ?EPCC if - * either - * - misa.C is enabled or - * - misa.C is disabled and the EPCC offset is sufficiently aligned - * - * If misa.C is held constant, as it almost always will be, between fault and - * readback, ?EPCC will be faithfully read back, because the alignment will - * adhere to the requirements of the architecture, which is what legalization - * is intending to enforce. - * - * If neither of those conditions hold, the resulting readout will be a lie; if - * ?EPCC has additionally been set to be a sentry, then the result will be an - * untagged lie. - */ -function legalize_epcc (v : Capability) -> Capability = { - let voffset = v.address; - let legalized = legalize_xepc(voffset); - - if legalized == voffset - then v /* avoid possibly attempting to set the offset of a sentry */ - else setCapAddrChecked(v, legalized) /* will clear tag if v is sealed or new address unrepresentable */ -}