CTSRD-CHERI / qemu

QEMU with support for CHERI
Other
52 stars 28 forks source link

Morello 'rrlen' instruction is implemented incorrectly. #197

Open jacobbramley opened 2 years ago

jacobbramley commented 2 years ago

Morello specifies a conservative behaviour for rrlen; some representable lengths are rounded up even if they are already representable. However, QEMU appears to use a slightly different implementation that doesn't do this. Specifically, QEMU's rrlen appears empirically consistent with setting the bounds (scbnds) on a null capability, then taking its actual length (gclen).

For example:

I'm taking FVP and Morello hardware as "correct" because they both seem to match the architectural pseudocode.

This is unlikely to break software using rrlen as intended, but may lead to false assumptions.

arichardson commented 2 years ago

QEMU currently sets bounds on a NULL capabability: https://github.com/CTSRD-CHERI/qemu/blob/ef6b6871875931eb77aaa36124fa5cee796d4782/target/cheri-common/op_helper_cheri_common.c#L558, but it should really call the helper in CTSRD-CHERI/cheri-compressed-cap: https://github.com/CTSRD-CHERI/cheri-compressed-cap/blob/6762a19ba9fb6a4291011fa690ce9a2647af10b2/cheri_compressed_cap_common.h#L949

I think that might also be incorrect for Morello, so we need to make two changes: 1) QEMU should use the cheri-compressed-cap helper and 2) cheri-compressed-cap needs to handle the special cases and we should add unit tests.

jrtc27 commented 2 years ago

Note that what Morello does is actually wrong and results in RRLEN not being idempotent for the largest representable length for a given exponent (i.e. the all ones case that you point out), which doesn't matter if you're just using it to pad but does matter if you want to do things like assert things are representable. I have seen such an assertion panic the kernel, as ELF loader code rounded up the length to be representable and then the higher-level code asserted the segment was representable by RRLEN(len) == len, which does not hold despite len being representable. So yes, QEMU should faithfully implement the architecture, but the architecture is flawed and what QEMU does it what Morello should have done.