Open lsf37 opened 4 months ago
An alternative would be to remove the behaviour part of DSpec
entirely, remove all of DRefine
, and directly prove capDL separation logic properties about the parts of the kernel API that are used by the initialiser. This would essentially fuse the refinement proof with the capDL-api proofs.
This would have the advantage that state that is currently invisible to the initialiser proof, such as TCB priorities, becomes accessible in that proof, because the full ASpec
state is accessible.
The downside of this alternative is that it is a much larger proof change.
@mbrcknl Do you anticipate needing DSpec
behaviour for things like cap granting over IPC in your work?
One thing to keep in mind is that I remember some parts of the DSpec
state and its behaviour being added to make sure that it accurately represented all of the access authorities granted by corresponding ASpec
states and to allow the Dpolicy
proof to be completed, even though they weren't directly needed for the system initialiser.
Currently
DSpec
has capDL behaviour for most operations in the kernel, including granting caps via IPC and other operations that the system initialiser does not use. Although we had more plans for capDL than that, the only current use forDSpec
is the system initialiser and it seems unlikely that more will materialise, because user-level reasoning with actual kernel behaviour is more useful directly on theASpec
level.One way to reduce proof size and maintenance overhead would be to replace specified behaviour in
DSpec
for these operations with non-determinism instead so that anyASpec
behaviour will still refineDSpec
by trivial refinement, essentially removing that refinement proof. As a consequence, one would no longer be able to reason about such kernel invocations on the capDL level -- but if the system initialiser is the only use case, we never have to.We should investigate how much of the refinement proof in
DRefine
that would eliminate (= how many kernel invocations have a capDL specification, but are not used in the initialiser, and how much proof in DRefine those invocations correspond to).We should also investigate if there are any other use cases or planned system initialiser extensions that would need such behaviour before we remove any.