Memory permissions clearing

[mndstrmr]

According to the Sail, when loading a capability permit_store should be cleared if the authorising capability does not have load_mutable and the loaded capability is both tagged and unsealed.

Similarly, if the authorising capability doesn't have permit_load_store_cap the tag of the loaded capability should be cleared. In the Sail this check is done after the load_mutable check, but in CherIoT-ibex it is done before.

Specifically, in mem2regcap_fmt0 the call to mask_clcperms should look like so: mask_clcperms(cperms_mem, clrperm, msw[32] & addr33[32], sealed), since this doesn't include clrperm[3] which should come later.

Also, if the incoming permissions bits are x10001 (SD), and clr_sdlm is set, then currently the output permissions would be x10000, which is not correct (and breaks monotonicity), since that decodes to giving SD+MC. Instead the output permissions should be 0.

Instead of

end else if (cperms_in[4:2] == 3'b100) begin
    cperms_out[0] = cperms_in[0] & ~clr_sdlm;
end else if (cperms_in[4:3] == 2'b01) begin

I believe we should have

end else if (cperms_in[4:2] == 3'b100) begin
   cperms_out[4:0] = (clr_sdlm & ~cperms_in[1])? 5'h0:
                     { cperms_in[4:1], cperms_in[0] & ~clr_sdlm };
end else if (cperms_in[4:3] == 2'b01) begin

[rmn30]

I debated a bit when writing the Sail what order to put the checks in. I don't think it matters for security and I think the order I chose was because I thought it would allow more parallelisation in hardware.

It could potentially affect memcpy. If the capability to the source buffer does not have permit_load_store_cap then we are doing a 'tag clearing' copy. As the Sail is currently this would have the side-effect of also clearing permit_store on all tagged capabilities from the source (if a capability does not have permit_load_store_cap it certainly does not have load_mutable). It's not clear what semantics are actually desirable there but that might be surprising. @nwf-msr @davidchisnall ?

[mndstrmr]

Apologies if my initial comment wasn't clear, but I take no issue with the Sail.

The problem is that the SV does the tag clearing before the permissions clearing - but the permissions clearing only happens if the tag is set. I agree that this doesn't affect the security of anything since the tag was cleared anyway, but again - it's a discrepancy between Sail and SV, which our proofs find.

The other issue is (I think) a security issue - I'm happy to be corrected though.

[nwf-msr]

I think I would be surprised if cbuildcap with suitable authority were not a left-inverse of tag-clearing memcpy (as might arise in paging in a bigger system, if not in CHERIoT itself). That makes me think our Sail spec is not what we intended (being a spec, it can't have bugs per se, right?).

ETA: The other issue does indeed sound like a security bug.

[kliuMsft]

I am fixing both issues in RTL in the next commit (hopefully out next week). Sorry it's been taking a while..

[kliuMsft]

RTL fix added in commit ba458ab, please verify. thanks.

[davidchisnall]

The problem is that the SV does the tag clearing before the permissions clearing - but the permissions clearing only happens if the tag is set.

I think that this is a case where the Ibex was correct and the specification was wrong. Clearing the tag if you don't have load-capability permission and then not modifying the resulting value is the less-surprising behaviour. Any code that depends on this is probably wrong, but it might impact some telemetry-gathering things.

[mndstrmr]

Seems correct, thanks - need to get this conclusive but no counter examples are being found.