On 18 Mar 2020, at 09:08, Demi M. Obenour mailto:demiobenour@gmail.com> wrote:
Would verifying seL4 on ARM64 be any more difficult than verifying
seL4 on ARM32 was?
No, as Aarch32 involved a lot of learning. 64-bit challenges have meanwhile been removed on x86 and (soon) RISC-V, and there is somewhat increased architecture abstraction in the proofs now. However, Aarch64 seems a bit more complex, which increases the effort. Also, the privileged architectures are different enough to make this essentially a new port, similar to RISC-V.
What about other architectures like POWER9?
I suspect Power would be significantly more work. A lot of the verification effort goes into verifying virtual memory, and the page table / MMU architecture on Power is quite different, all our other architectures are at least superficially similar there. But I don’t see this happening, there just isn’t demand. We rather focus on getting Aarch64 funded, for which there is strong demand. (Arm, are you listening????)
Gernot
