AArch64 Information Flow - #1018
Conversation
3eb8d6c to
eca4978
Compare
eca4978 to
04465e5
Compare
ac7b505 to
5bb57dc
Compare
|
Hello! I am caring about this pr because I want to integrate this into the seL4 deployment in my company. It is known that Isabelle version updates break proofs often. What Isabelle version should I use to run isabelle build on these? I tried Isabelle2025 but it errors. |
I'd recommend waiting until this PR is merged, because cleanup is still in progress and while that happens the proofs might break in between (as happened just now). Should be at most another week or two.
If you follow the setup instructions in https://github.com/seL4/l4v/blob/master/docs/setup.md you will get the correct Isabelle version automatically. You will also get the seL4 version the proof applies to. (To get the proofs in this PR , after the repo checkout, you need to go into the The current version this repo is using is Isabelle2025, but we may change to Isabelle2025-2 in the next month or two. |
This comment was marked as resolved.
This comment was marked as resolved.
37aedf9 to
2b6bde2
Compare
29535b7 to
1863e34
Compare
|
I spent a while hunting which commit the changes came from for the infoflow refine interfaces... would be nice to get a bit more commit text for the relevant |
| (* FIXME AARCH64 IF: move *) | ||
| locale_abbrev numlistregs :: "'s state \<Rightarrow> nat" where | ||
| "numlistregs s \<equiv> arm_gicvcpu_numlistregs (arch_state s)" | ||
|
|
||
| (* FIXME AARCH64 IF: move *) | ||
| locale_abbrev current_vcpu :: "'s state \<rightharpoonup> obj_ref \<times> bool" where | ||
| "current_vcpu s \<equiv> arm_current_vcpu (arch_state s)" |
There was a problem hiding this comment.
Should we do this move before we merge? To ASpec or AInvs?
There was a problem hiding this comment.
If we agree these abbreviations are preferable, it would be nice to have broader adoption throughout the proof stack. I feel that's beyond the scope of this PR, however
There was a problem hiding this comment.
I'm not sure how much these abbreviations help really; can you elaborate? These don't exist on any arches other than Arms, and the abbreviation hides the arch_state dependency. I can probably be persuaded on the current_vcpu, but the numlistregs seems too specialised.
|
I missed where this happened exactly, but there were a couple of: |
|
Done with review pass from my side. Overall, really nice work and thank you for all the cleanup and improvements (some of which I yoinked to be able to deal with Syscall_R). I would ask that this goes in after the Syscall_R arch-split PR, which I hope to be done with today or tomorrow. There's mostly style stuff, mostly related to existing infoflow style. A few things to consider, especially the situation with those interface locale instantiations picking up increasing amounts of logic, which I really would prefer to be as non-thinking as possible. |
d781948 to
8363f9d
Compare
8363f9d to
7860411
Compare
Remove various instances of pspace_aligned, valid_vspace_objs, and valid_arch_state from the preconditions of valid and equiv_valid predicates. Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
When the irqs parameter is false, domain_sep_inv asserts that all non-timer IRQs must be disabled. This change asserts that the interrupt state of any non-kernel IRQ is inactive, and therefore not a timer IRQ. Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Use the RISCV64 InfoFlow proofs as a basis for AARCH64. Proofs have been copied verbatim modulo renaming the architecture. Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
The vgic_lr field is defined as a total function from nats to virqs, with the domain restricted only in practice via the parameter arm_gicvcpu_numlistregs. To establish value-level equivalence between vcpus in the InfoFlow proofs, the vcpu integrity relation must therefore ensure out-of-bounds list registers remain untouched. Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Add a top-level image to the InfoFlowC proofs, mirroring the top-level image introduced to the InfoFlow proofs. Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
Example states were designed with an overlapping kernel window and ELF window in mind. Recent changes to how the ELF window is implemented on AARCH64 mean these windows no longer overlap. This commit comments out affected parts of the example state until the changes can be properly addressed. Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
7860411 to
5395db2
Compare
|
This is now good to merge from my side. We'll do a separate cleanup pass for some of style questions raised in the review. |
4 participants
Completed information flow proofs for AARCH64. Please see c10da23 when reviewing the non-interference proofs and 8f7e892 when reviewing the refinement proofs, as these provide the most minimal diffs. The main additions are:
equiv_hyprelation equating VCPU machine/architectural state. The equivalence is only enforced when the current VCPU, if it exists, belongs to the domain under consideration. Certain fields need only be equivalent when the VCPU is active.equiv_fpurelation equating FPU machine state. The equivalence is only enforced when the current FPU belongs to the domain under consideration.