Misaligned RV32 memory access circumvents address bound check when overflowing

[alda-tuk]

We detected a scenario which is a potential security vulnerability. An attacker may access a memory address (0x0) outside of the capability address bounds.

Unaligned RV32 accesses are split into two aligned accesses. If the access is unaligned (crossing the word boundary) and in the top most word, i.e., at address 0xffff_fffd-0xffff_ffff, the first aligned access is to address 0xffff_fffc and the second access causes an overflow/wrap-around to 0x0. This may circumvent the capability address bound checks: Let's assume the 32-bit (expanded) base bound is at 0xfff0_8000, and the 33-bit (expanded) top bound is at 0x1_ffff_0ffc. For an unaligned RV32 access to 0xffff_fffd the first actual memory access (to 0xffff_fffc) is inside the bounds and thus legal. However, the second access (to 0x0) is outside of the capability bounds and thus illegal. But for the second access, the core does not raise an error. A base violation is raised, but not propagated further, because of the addr_incr_req_i flag.

We detected a scenario, where the illegal access was conducted. We used a formal tool for detection and provide a screenshot of a waveform displaying the issue.

As a fix, we propose to never permit misaligned RV32 accesses in the top most address.

Best regards, Anna and Johannes

[kliuMsft]

Hi Anna/Johannes,

Greatly appreciate you working on cheriot-ibex. I will look into the issue and get back to you as soon as possible.

[kliuMsft]

I am actually not sure this is a real issue (after trying to recreate it in simulation). A couple observations

1. currently we do address check based on comparing the target address against top-4 and base bounds (assuming word accesses). cheri_ex/lsu_req_o and cheri_ex/lsu_cheri_err_o are updated once the comparison is done on the base address. The LSU state machine is designed such as if the lsu_cheri_err_o is asserted, it will stays in IDLE, so that addr_incr_req won't be asserted in this case - and thus the 2nd access in a misaligned transaction won't be a factor in comparison
2. this is probably not as relevant, but I just want to point out that while it is allowed by encoding, in real use we will never have the 33-bit top_bound larger than 0x1_0000_0000. Reason being that the core starts with root capabilities set at top_bound=0x1_0000_0000, and we only allow shrinking bounds.

See the simulation waveform below (RV32 word write at 0xffff_ffff, cs1.top33=0x1_0000_0000, cs1.base32=0xffff_fffc).

Please let me know what you think, thanks.

[alda-tuk]

Thank you for investigating the case and for the clarification. Restricting the 33-bit top_bound to values <= 0x1_0000_0000 essentially blocks all misaligned word accesses in the top most word (and thus the overflow).

We will further investigate why our counterexample considers top_bounds larger than 0x1_0000_0000. We may have to add additional constraints to our proofs.

[davidchisnall]

Thanks for investigating this. Properties that arise from monotonicity tend to be tricky for verification of the Verilog because they require dataflow to be tracked via inductive proofs from the reset state. I'd be very interested in tooling that could preserve these properties.

[kliuMsft]

@alda-tuk Should we close this issue?

[alda-tuk]

Yes, thank you. With additional constraints our proofs ran successful.