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 Thanks :)
"Jessie Frazelle (TUPPERWARE)" <jessfraz@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. Regards, Anthony Liguori
Thanks :)
_______________________________________________ Kata-hypervisor mailing list Kata-hypervisor@lists.katacontainers.io http://lists.katacontainers.io/cgi-bin/mailman/listinfo/kata-hypervisor
participants (2)
-
Anthony Liguori
-
Jessie Frazelle (TUPPERWARE)