Fix the auipcc reachability challenge #116
Conversation
to B, which solves the problem with CHERI in rv32 becoming unrepresentable in corner cases due to AUIPCC needing to go out-of-bounds by +-2048 in order to constitute an arbitrary address.
|
@LawrenceEsswood does this look correct to you? |
|
Are we intentionally doing this for both RV64 and RV32 or should it be RV32 only? Assuming that the cost is negligible, I don't have a problem with the change as such, although for the reasons discussed on the mailing list I now have a weak preference for redefining auipcc in such a way as to be compatible with any representability definition. |
|
This semantic change is very annoying for the CSR architecture. Pre this PR, the low 7 or 12 bits of a capability's address can be changed without representability checks, so you don't need representability checking for writes to jvt, xepc or xtvec (assuming that vectored mode is not implemented or is implemented with an appropriate alignment requirement). This might also affect the implicit bit zero clear in jalr, and the fuzzy block addressing used by CMOs. |
|
Writes to CSRs change, yes, and we’re aware of this potential concern. I don’t believe any of the other issues you raise are real though; if the capability in use becomes unrepresentable it will be out of bounds of the original capability, and since bounds checks in instructions are done with the original bounds you will take a bounds fault deterministically. |
Yeah, this is what I had proposed. Although I have nothing to add about how it complicates writes to legacy CSRs, I had not considered that would cause issues. |
|
Here's an attempt to implement this in Sail, by the way. https://github.com/CTSRD-CHERI/sail-cheri-riscv/tree/auipcc-representable-fix . To prove we cover all the cases, we probably want to bring https://github.com/CTSRD-CHERI/sail-cheri-riscv-verif/blob/master/cap_properties.sail up to date and add a property. |
|
Are there any opjections to merging this one? |
|
No objections just thought we were waiting for proofs to run before merging. |
|
@PeterRugg agreed to run the proofs in the TG meeting today, so we should hopefully be able to merge this PR soon. |
|
Are the meetings being organized somewhere other than the SIG CHERI lists.riscv.org mailing list? |
|
There is a CHERI SIG / TG meeting slot every other week, present in the RISC-V technical meetings shared calendar. |
|
Fix #56 |
|
FWIW, I think I have proved for RV32 and RV64 that this proposed fix, as implemented in https://github.com/CTSRD-CHERI/sail-cheri-riscv/tree/auipcc-representable-fix, fixes the problem, in the sense that, for all encoded, executable (unsealed, in-bounds, ...) capabilities, and all in-bounds target addresses within the reachable range of AUIPCC and CJALR, the AUIPCC will not break representability and the CJALR will succeed and take you to the intended target address. The property finds the known counterexample for RV32 without the fix, then proves the property once the fix is applied. RV64 goes through fine (albeit slowly!) with or without the fix. There are some issues with making the property and proof flow public that I'll try to get sorted out. I also had to hack in some minor changes to Sail's SMT backend, so take with a pinch of salt! |
As with #116 (comment) I've proved that the decoded bounds from encoded capabilities always have base <= top. It finds the problem before this fix and proves the property after this fix. Same caveats apply, including that I've had to change the SMT backend. Fixes: #149
This is Jon's proposal to change the specification according to Lawrence's suggestion, addressing #56.
Ideally we wouldn't merge it until we implement it, at least in our cheri-cap-lib, to confirm it doesn't affect timing too much to do a MW-bit comparison rather than a 3-bit comparison on these paths, and to make sure it fixes the issue.