AArch64 Information Flow - #1018

Merged

lsf37 merged 11 commits into

aarch64-infoflow

Aug 7, 2026

Commits on Aug 5, 2026

arm+riscv64 infoflow: relax assumptions
ryybrr
committed
9da39fd
access: strengthen domain_sep_inv
ryybrr
committed
4efb42d
aarch64 infoflow: copy riscv64 theories
ryybrr
committed
b6414ff
aarch64 access: strengthen vcpu integrity relation
ryybrr
committed
cb6f8fd
aarch64 infoflow: prove noninterference
ryybrr
committed
4bd1e0c
aarch64 infoflow: prove refinement
ryybrr
committed
a0af1c6
aarch64 infoflow: update example state proofs
ryybrr
committed
1525485
arm+riscv infoflow: proof update for infoflow changes
ryybrr
committed
a6e5018
infoflow refine: add InfoFlowC_Image_Toplevel
ryybrr
committed
daaf777
run_tests: enable InfoFlow for AARCH64
ryybrr
committed
93394a5
aarch64 infoflow: add example state fixmes for kernel ELF changes
ryybrr
committed
5395db2