MCS: Remove grant right from reply cap #808
Conversation
corlewis
added
MCS
corlewis
force-pushed
the
corlewis/mcs-grant-via-reply
branch
from
675db24
to
ab4e713
Compare
proof/refine/RISCV64/KHeap_R.thy
Outdated
| apply (clarsimp simp: obj_at'_def) | ||
| apply wpsimp | ||
| apply wpsimp | ||
| apply (clarsimp simp: obj_at'_def) |
There was a problem hiding this comment.
this pattern is a bit long-winded, any way to shorten it? I guess passing obj_at'_def to wpsimp is probably going to not go where we want, but as this is terminal, maybe a (wpsimp | ...)+?
There was a problem hiding this comment.
I ended up going with apply (wpsimp | normalise_obj_at' | erule obj_at'_weakenE)+, as an attempt to make it less likely to go down unintended paths if anything changes.
There was a problem hiding this comment.
Well done getting this done so quickly, it's been pending for a long while, good to have it cleared. Apologies review took so long.
Apart from small nitpicks (rt proofs seem to have more verbosity in places, maybe it's the general vibe on that branch), I have one extra concern: I'm seeing changes to the manual in the corresponding seL4 PR, and some of those descriptions look to originally have been copied from our Haskell spec comments. However, this PR does not change any Haskell or abstract comments, which seems suspicious. Either we never added/changed them for MCS (also not great), or it feels like something should get updated. Thoughts?
Hmm, I haven't done an exhaustive search but I can't see any equivalent comments in the specifications. |
corlewis
force-pushed
the
corlewis/mcs-grant-via-reply
branch
from
ab4e713
to
eda3dfe
Compare
There was a problem hiding this comment.
Excellent, and as Raf said this went much quicker than I thought it would. Good work.
I don't think this interferes with anything @michaelmcinerney has in flight, so we should be able to merge after squashing.
In MCS configurations, a server's ability to grant capabilities when replying to a call were previously determined entirely by the grant right on the reply capability the server supplied when calling `receiveIPC`. If the server had sufficient untyped memory, it could create arbitrary reply capabilities, giving itself the ability to grant to its clients. Consequently, the only way to restrict a server's ability to grant to its clients was to avoid giving it untyped memory. This would break the expected authority confinement property. Contrast this with non-MCS configurations, where the grant rights on a server's receive endpoint control the server's ability to grant capabilities when replying to calls. This makes it much easier to restrict a server's ability to grant when replying. This commit makes MCS configurations behave more like non-MCS configurations: In order to grant capabilities when replying to a call, a server must have a grant right on the receive endpoint capability when it calls `receiveIPC`. This commit also removes the grant right from reply caps, as following the previous change this right has no clear use case. Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
corlewis
force-pushed
the
corlewis/mcs-grant-via-reply
branch
from
eda3dfe
to
870da47
Compare
This commit is the corresponding specification and proof updates for seL4/seL4#945, the second alternative described in https://github.com/seL4/rfcs/blob/main/src/active/0130-mcs-grant-reply.md.
The updates to the specifications, abstract invariants and refine proofs are complete. As crefine for MCS is still in progress, I have only updated it as needed to maintain its current state. In particular, this means that I have not proven refinement to the C code for the changes made to
receiveIPC, since that would require first updating that proof for all of the other unrelated MCS content.receiveIPCis a relatively complicated function, so this could be a significant amount of work and should probably be done separately.Test with: seL4/seL4#945