Hey, davidk01, do you know if there’s any use on these things of MS Research’s verification tools like VCC, the static analyzer, and so on? I know they did at least 20% of Hyper-V with separation logic back in Verisoft project. I try to keep track of what real-world projects they’re using their excellent tooling on.
I’m skeptical of the “hypervisor as exploit mitigation” fallacy. All virtualization does is add more surface area for attackers. Hypervisors, as currently implemented, do not stop exploits.
They worked fine when they did them high-security. They contained many OS-level attacks. That would seem to counter your point unless you just mean these mainstream VMM’s with big OS’s and such (“as currently implemented”). The tricks were that they had to be simple, have rigorous design, and use hardware techniques for mitigations. Often use formal methods, static analyzers, and so on on top. Nova microhypervisor and Muen separation kernel are examples of this design strategy.
Hey, davidk01, do you know if there’s any use on these things of MS Research’s verification tools like VCC, the static analyzer, and so on? I know they did at least 20% of Hyper-V with separation logic back in Verisoft project. I try to keep track of what real-world projects they’re using their excellent tooling on.
Good question. I’m not sure.
… and surely there won’t be a way to break out of it! Zero trust. VMWare and Virtualbox virts are broken out of all the time as headlines. Next!
I’m skeptical of the “hypervisor as exploit mitigation” fallacy. All virtualization does is add more surface area for attackers. Hypervisors, as currently implemented, do not stop exploits.
They worked fine when they did them high-security. They contained many OS-level attacks. That would seem to counter your point unless you just mean these mainstream VMM’s with big OS’s and such (“as currently implemented”). The tricks were that they had to be simple, have rigorous design, and use hardware techniques for mitigations. Often use formal methods, static analyzers, and so on on top. Nova microhypervisor and Muen separation kernel are examples of this design strategy.