[Kata-hypervisor] Formal verification

Anthony Liguori aliguori at amazon.com
Thu Jun 7 19:36:30 UTC 2018

"Jessie Frazelle (TUPPERWARE)" <jessfraz at microsoft.com> writes:

> I didn't want to fork the other thread too far off base but I was
> wondering if people had thought or implemented formal verification for
> hypervisors and if they could share any details.
> Everything I've read on formal verification of hypervisors is purely
> from papers but not from industry so I am wondering if there are
> discrepancies between academia and industry here 

We use it pretty extensively.

One of the things I like about Rust is that a class of problems that you
previously applied model checking to (memory safety) just disappears
entirely.  If a Rust program compiles, it's memory safe.


Anthony Liguori

> Thanks :)
> _______________________________________________
> Kata-hypervisor mailing list
> Kata-hypervisor at lists.katacontainers.io
> http://lists.katacontainers.io/cgi-bin/mailman/listinfo/kata-hypervisor

More information about the Kata-hypervisor mailing list