top33[32] flip during bounds decompression

[mndstrmr]

The Bug

Currently neither the spec nor cheriot-ibex implement a bit flip for top33[32] when the decoded bounds either should or should not wrap the address space as is seen in Cambridge's version. This makes CSetAddr and family disagree with the Sail on when a new address is representable.

Example

Consider a reasonable capability A:

A = {
    address: 0x000002fe,
    tag: 1,
    base: 0x17c,
    top: 0x17d,
    exp: 8
}

Currently both Cheriot-ibex and the Sail decode the bounds of A to base = 0xffff7c00 and top = 0x1ffff7d00. I personally consider this already surprising.

However, now consider running cincaddrimm B, A, -2046. This gives, according to the Sail,

B = {
    address: 0xfffffb00,
    tag: 0,
    base: 0x17c,
    top: 0x17d,
    exp: 8
}

Where the tag was cleared because it decoded the bounds to be base = 0xffff7c00 and top = 0xffff7d00, which is not a match.

Cheriot-ibex did not clear the tag, which is incorrect under the current specification.

Fix

While technically it is the processor that is failing to conform to its specification, I am not under the impression that the spec is right. I personally fail to be convinced that the behavior observed without the flip Cambridge has present is desired. If the flip is done, the decoded top33 bounds of both A and B are 0xffff7d00, and in every case the output of CIncAddr (and its family) will be at least as strict as the Sail.

Therefore I would suggest adding Cambridge's bit flip to both the SystemVerilog in reg2fullcap, and in the Sail.

[kliuMsft]

I think the question is that in a CHERIoT system whether it's possible to have a capability like A, with tag not cleared. Note that we starts with a fixed set of root caps and all derived capabilities have to be either by set_bounds or set_address (hopefully, of course w have to prove that). @rmn30, I thought as you mentioned in the email thread, this is proven by SMT?

[kliuMsft]

Copying @davidchisnall @nwf-msr on the issue

[mndstrmr]

I see. Is there some way to characterise what those valid capabilities are? We do now ensure that capabilities loaded with their tag bit set must have base <= top.

Otherwise we will have to create some unpleasant logic to ensure that only capabilities that are stored can be loaded, which I would probably prefer to avoid.

[kliuMsft]

This is a bit challenging. We know what the capability roots are, and we can assume that capabilities won't be tampered with when in memory, so we always read back exactly what's written to memories. Hopefully we can prove (or disprove) that if we starting from a valid and representable capability we can never get to a unrepresentable one without clearing the tag. I think we consider any capability with 0 < address - base32 < 2^(exp+9) is representable (signed math).

[davidchisnall]

@rmn30 did some work with the SMT output from Sail. I’m not sure what your tools can consume, but possibly we can combine those in some way to prove that the core will do valid things with anything that is a valid derivation chain from one of the roots?

[mndstrmr]

I think we consider any capability with 0 < address - base32 < 2^(exp+9) is representable (signed math).

Just to be clear, is this a necessary condition, or just sufficient? I assume it is sufficient but not necessary since I can create counter examples to it: i.e. without getting memory involved I can find tagged capabilities where e.g. address < base.

[rmn30]

The SMT proof only considered capabilities that could be created by csetbounds with a top less than or equal to $2^{32}$ (followed by csetaddr). Note that the top representable bound can be larger than $2^{32}-1$ but we don't treat that as wrapping around. I think the bit flip in CHERI is designed to accommodate such capabilities and it is like that mainly for compatibility with the fast representability check, not because it is useful to have a representable range that wraps the address space. CHERIoT uses a different representability check so doesn't need the flip. If you can find a case where it actually makes a difference I'm interested but I'd rather not have it if we can avoid it as it's more hardware and I'd need to do some more SMT checks.

[mndstrmr]

My apologies for the delay. I am a full time undergrad, so time has been a bit sparse the last few weeks, but I can confirm I can finally prove the correctness of the instructions this issue affects. In the end requiring top <= 2**32 as well as a relaxed form of base <= top did it.

Thanks for all the help from you all.

[kliuMsft]

Fully understood and thanks for wrapping up the issue!

-Kunyan

From: Louis-Emile Ploix @.> Sent: Friday, November 17, 2023 8:44 AM To: microsoft/cheriot-ibex @.> Cc: Comment @.>; Subscribed @.> Subject: Re: [microsoft/cheriot-ibex] top33[32] flip during bounds decompression (Issue #7)

My apologies for the delay. I am a full time undergrad, so time has been a bit sparse the last few weeks, but I can confirm I can finally prove the correctness of the instructions this issue affects. In the end requiring top <= 2**32 as well as a relaxed form of base <= top did it.

Thanks for all the help from you all.

- Reply to this email directly, view it on GitHubhttps://github.com/microsoft/cheriot-ibex/issues/7#issuecomment-1816748783 or unsubscribehttps://github.com/notifications/unsubscribe-auth/A3V7IMA7DBYMQRTLMNPCWYDYE6H4NBFKMF2HI4TJMJ2XIZLTSOBKK5TBNR2WLJDUOJ2WLJDOMFWWLO3UNBZGKYLEL5YGC4TUNFRWS4DBNZ2F6YLDORUXM2LUPGBKK5TBNR2WLJDUOJ2WLJDOMFWWLLTXMF2GG2C7MFRXI2LWNF2HTAVFOZQWY5LFUVUXG43VMWSG4YLNMWVXI2DSMVQWIX3UPFYGLLDTOVRGUZLDORPXI6LQMWWES43TOVSUG33NNVSW45FGORXXA2LDOOJIFJDUPFYGLKTSMVYG643JORXXE6NFOZQWY5LFVE2TSMBRGM3DKOBZQKSHI6LQMWSWS43TOVS2K5TBNR2WLKRRHA4DOOJUHE4DKMFHORZGSZ3HMVZKMY3SMVQXIZI. You are receiving this email because you commented on the thread.

Triage notifications on the go with GitHub Mobile for iOShttps://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675 or Androidhttps://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub.