search

microsoft / cheriot-ibex

cheriot-ibex is a RTL implementation of CHERIoT ISA based on LowRISC's Ibex core.
Apache License 2.0
73 stars 14 forks source link

CSEQX #6

Closed mndstrmr closed 11 months ago

mndstrmr commented 1 year ago

The Bug

According to the spec CSEQX should do a comparison of the in memory representation of two capabilities. Currently CSEQX compares the decoded bounds, not the encoded bounds. These are not necessarily the same.

Example Case

Let A = {base = 0x100, exp = 24, tag = 0, ... = X} and B = {base = 0x000, exp = 24, tag = 0, ... = X}. Then A and B decompress their bases to the same base32, as the top bit of A.base will be dropped. This means CSEQX will claim they are equal when the Sail would not.

A could not be stored by the processor with its tag bit set, but it could still be loaded and compared with the tag bit clear.

Fix

I suggest simply doing the comparison on the encoded bounds instead.

kliuMsft commented 1 year ago

@rmn30 Robert, what do you think here - should we consider the 2 caps equivalent or not. Also, should we include the reserved bit as well in the comparison?

kliuMsft commented 1 year ago

Adding @davidchisnall @nwf-msr to the issue.

davidchisnall commented 1 year ago

This instruction is intended for bitwise comparison of untyped memory, so it would be a problem if two I tagged bit patterns that are identical compared not equal (or vice versa).

kliuMsft commented 1 year ago

Ok I have checked in the RTL change (to compare all fields per memory presentation), commit 3e1e7d2. @mndstrmr, a previous commit (33feabd) fixed the CSC instruction decoding and the memory cap format (permission field size and top/base swap).

mndstrmr commented 11 months ago

Apologies for taking a while to get back to you, but I can confirm the CSEQX fix is correct. I'll take a look at the memory stuff next - if there are any further problems I'll open a new issue for them.