[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.
Regards,
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