Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proofs for SGI API #733

Draft
wants to merge 20 commits into
base: master
Choose a base branch
from
Draft

Proofs for SGI API #733

wants to merge 20 commits into from

Conversation

lsf37
Copy link
Member

@lsf37 lsf37 commented Mar 14, 2024

This PR adds verification for the SGISignalCap API of RFC-17 (seL4/seL4#1222).

Specs and proofs are updated for all architectures (affects mostly ARM, ARM_HYP, and AARCH64), including all affected parts of the proof stack (access control, infoflow, capDL, system initialiser etc). In the system initialiser, SGISignalCaps are currently still excluded via the definition of wellformed specifications.

Test with: seL4/seL4#1222

This is currently still in draft mode until the RFC recommendations have been implemented.

@lsf37 lsf37 added the seL4-PR requires merging a corresponding seL4 pull request label Mar 14, 2024
@lsf37 lsf37 force-pushed the sgi branch 5 times, most recently from 6176090 to 5b40e6f Compare March 15, 2024 19:48
lsf37 added 20 commits March 26, 2024 10:12
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
In preparation for adding an API for software-generated interrupts,
make config_ARM_GIC_V3 visible to the proofs, so values of constants
can be defined conditionally on GICv2/v3 use.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This affects all architectures, because generic interfaces are changing,
but the SGISignalCap API is only added to ARM, ARM_HYP, and AARCH64.
For X64 and RISCV64, we trivially implement the new interfaces, and in
generic code we call those interfaces.

These new interfaces are isArchMDBParentOf and
isIRQControlCapDescendant, for checking in generic code if there are
architecture specific cases in isMDBParentOf and isCapRevocable
respectively.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Define the new constants numSGIs and gicSGITargetMaskBits, plus a new
machine operation ipiSendTarget.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
- add SGISignalCap API for ARM, ARM_HYP, AARCH64
- add generic interface for should_be_arch_parent_of and
  is_irq_control_descendant in the cdt implementation
- add default interface implementations new interfaces for RISCV64, X64

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This contains a slight tweak to generic CSpace_AI and proof adjustments
for the architectures that do not implement the SGISignalCap API.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
For now exclude SGISignalCap from wellformed specs. To be relaxed
later.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Fix + modernise style and proofs.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add separation logic specification lemmas for the new SGISignalCap API
for later use in sys-init.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
@lsf37 lsf37 added the multicore anything related to multicore verification label Mar 26, 2024
@lsf37 lsf37 self-assigned this Mar 26, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
multicore anything related to multicore verification seL4-PR requires merging a corresponding seL4 pull request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant