On 21 Jan 2020, at 14:17, Demi M. Obenour wrote:

Are there plans to verify the IOMMU support on x86? x86 without DMA is not very useful, so IOMMU support is needed for the proofs to apply in practice.

There are plans for many things, as they say ;-). You are completely right that IOMMU verification would be very useful. We don’t have a current project or funding for it, but we would be generally interested if funding could be found. We did have a specification for earlier experimental IOMMU support in the past, but not proofs, and we had to drop it because it diverged too much from the code. Similar for binary verification on x64. We do have a project for binary verification on 64-bit RISC-V, which may provide some progress into this direction, but it’s again a question of funding, maybe as part of a separate larger project, to fill the gap. Cheers, Gerwin