On 18 Mar 2020, at 09:08, Demi M. Obenour <demiobenour@gmail.commailto: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