6 ms·

SeKVM verified hypervisor based on KVM

65 points by cvwright 5y ago

posix_me_less 5y ago
I don't know whether to laugh or cringe. "Machine checked formally verified" is a long-known buzzword that screams bullshit marketing. It does not mean that your VM will be securely isolated, data-breach-proof in practice. If you care about security of your VMs, you need to run them yourself on hardware that you control, using security patched customized Xen/KVM. If you run VMs in the cloud, you do not actually care about security. Some people care really only about appearances and compliance checkboxes, maybe this formally verified thing will catch on for those.
- monocasa 5y ago
  We'd have to see their code to know for sure, but they're doing the right things to follow in the footsteps of non bullshit formal verification like sel4. Reducing the size of the checked code to ~4kloc, only checking ARM which (thanks to projects like sel4) has the correct infrastructure built up, etc. Can you point to some truly formally verified software that turned out to be bullshit so we can compare their techniques?
  - posix_me_less 5y ago
    I didn't say formally verified software is bullshit. I said the marketing here is. FV software exists but its benefits are very limited (basically it's a debugging tool). Running VMs on x86 or ARM in cloud has much more serious problems related to security than using not-formally-verified hypervisor.
    - monocasa 5y ago
      It's more than a debugging tool as it allows you talk confidently about entire classes of vulnerabilities rather than the wack-a-mole of fixing bugs traditionally. And it's a big enough deal that the rumor is that Amazon and Microsoft's type 1 hypervisors have been formally verified. I wouldn't be surprised if Google's is too.
      - posix_me_less 5y ago
        It allows academics and other informed scientists to talk confidently about their design. Everybody else like Linux admins and VM users is still working with a black box software. Sure cloud vendors may get on board and start announcing how their solution is the best verified software out there. Did I mention bullshit marketing yet?
        touisteur 5y ago
        I don't understand. If I've proved the absence of runtime errors in some code, in addition to classical tests, are you saying that the software is not less likely to crash? Yes, there can be errors everywhere but I don't get this complete rejection of Formal verification tools as 'just a debugging tool'.
        posix_me_less 5y ago
        It is less likely to crash after you complete the proof than if you couldn't complete the proof, but this does not mean this benefit will be worth much. In general, all things being equal, software less likely to crash in production is an improvement, but: 1) all things are usually not equal, because verified software is hard to produce and typically much more restrictive and hard to modify 2) how often do standard industry solutions for hypervisor like Xen or KVM crash? Uptime/customer loss due to hypervisor crashes is a negligibly small problem. The user software should rather work with the assumption that crash can happen. That is much more robust architecture than relying on some proofs that nobody checked.
        touisteur 5y ago
        Though I agree about being 'crash proof' we're talking security here, so DoS or RCE might happen because of a buggy parser, crash or no crash. If I can create a parser that won't produce any error whatsoever, and always return something (be it 'malformed message'), haven't I increased the security of my external interfaces, compared to, let's say, a shit parser full of UB and no check because the program is crashes happen anyway?
- tyingq 5y ago
  I agree that formal verification isn't, by itself, some kind of panacea. Reading the paper, though, the effort did uncover some issues. Two examples, though there are more: "When proving invariants for page ownership used in the noninterference proofs, we identified a race condition in stage 2 page table updates" "KCore initially did not check if a gfn was mapped before updating a VM’s stage 2 page tables, making it possible to overwrite existing mappings" So mapping out the rules/flow in Coq, and then seeing what actually happened did uncover some flaws. As to whether the juice was worth the squeeze, I don't know this space well enough to comment.
  - posix_me_less 5y ago
    Yes, formal methods can be useful, they help uncover bugs. It's a debugging tool, albeit a very demanding one. For some software, it makes sense to use it. Real deployment of VMs has larger problems with security than not formally verified hypervisor so I think the answer for most hosting companies is "the juice is not worth the squeeze" here, the squeeze being the restriction to academic verified design. Hosting VMs is mostly about features and reliability. Those who need also real security, will host on their own HW and won't allow foreign VMs, so formally verified hypervisor is less of a requirement there too. It's a "nice to have".
    - exdsq 5y ago
      Is it a debugging tool if the work is done upfront before writing code?
      - posix_me_less 5y ago
        Yes. Debugging tool reduces number of bugs in the product. Formal design specification and design verification can do that. And even with something lackluster like gdb, you may be forced to do some redesigning before writing more of new code.
- teakettle42 5y ago
  > "Machine checked formally verified" is a long-known buzzword that screams bullshit marketing. Long-known to who, exactly? How is "formal verification" even remotely a marketing buzzword?
  - posix_me_less 5y ago
    To people interested in software process. There is a consensus that formal verification and automatic checks in software (even hardware) are a debugging tool, not a comprehensive success/security policy like the linked article would suggest.
    - cvwright 5y ago
      "People interested in software process" have been trying, and failing, to write secure C code for 50 years. But they've made a ton of money trying!
      - posix_me_less 5y ago
        C was not initially intended for such a thing, although later people tried to restrict it. Also, "secure C code" is too vague. It depends on the scope. Grep is quite secure in what it does. Linux, less so.
    - touisteur 5y ago
      I'm curious where you get this consensus. It's not at all shared by everyone, especially with the huge strides SPARK and Frama-C have made.
      - posix_me_less 5y ago
        I didn't mean academic consensus. More like industry / security-aware people in IT consensus - almost nobody in software does formal verification and it would be foolish for any user, whether person, business or government, to take this as solution to their VM hosting security problems. Yes formal verification has made advancements and is a useful tool, in proper context. Not in the context the article is selling the work of the researchers.
tyingq 5y ago
Discussed a couple of weeks ago based on a different article: https://news.ycombinator.com/item?id=27275707 https://news.ycombinator.com/item?id=27275707 Also see: http://nieh.net/pubs/ieeesp2021_kvm.pdf http://nieh.net/pubs/ieeesp2021_kvm.pdf (The paper) https://microv.org/ https://microv.org/ (A website with more detail, Coq source, etc)
- xpuente 5y ago
  Right and... > Side-channel attacks [20],[21], [22], [23], [24], [25] are beyond the scope of the paper If all current hardware (i.e. OOO and caches) is vulnerable to speculative side-channel attacks, how they dare to say that is secure? With current hardware, nothing is secure (full stop)
  - tyingq 5y ago
    Most of the angst here seems to be around the phrase "provably secure". I don't think they meant that in the same sense that it's being received here. "Provably <xyz>" is just the common terminology in the theorem prover space. Though they seem to be familiar enough with the real world to have known that would have sounded overly grandiose. I think what they really meant was something like "Provably Implements Whatever Security Boundaries That It Claims To".
  - naasking 5y ago
    > If all current hardware (i.e. OOO and caches) is vulnerable to speculative side-channel attacks, how they dare to say that is secure? The software is provably secure. That doesn't mean a complete solution consisting of software and hardware is necessarily secure, and it has never meant that.
    - xpuente 5y ago
      Then, what is the value of making the software secure if the hardware isn't? The hardware issue is terrifying. And the worst part, it seems not possible to fix it without trowing away decades of performance enhancements. This epic screw-up of epic dimensions from computer architecture guys won't go away that easy.
IncRnd 5y ago
> SeKVM Makes Cloud Computing Provably Secure > Columbia University researchers have created a secure Linux-based hypervisor > Now computer scientists at Columbia University have developed what they say is the first hypervisor that can guarantee secure cloud computing. > The researchers dubbed their new technique microverification, which reduces the amount of work needed to verify a hypervisor. It breaks down a hypervisor into a small core and a set of untrusted services, and then goes on to prove the hypervisor secure by verifying the core alone. The core has no vulnerabilities for a hack to exploit, and this core mediates all the hypervisor's interactions with virtual machines, so even if a hack undermines one virtual machine, it does not compromise the others. It sad how IEEE's Spectrum carried this nonsense. There clearly wasn't any real technical review of these statements prior to publishing.
- pizzazzaro 5y ago
  Im skeptical of the way these researchers declared so much to be "out of bounds." Where can I find the source code? I wanna see if I can... Idk, patch that. Since this is derivative of gpl code in Linux Kernel, whats our chances of getting to inspect it ourselves?

65 points by cvwright 5y ago

I don't know whether to laugh or cringe. "Machine checked formally verified" is a long-known buzzword that screams bullshit marketing. It does not mean that your VM will be securely isolated, data-breach-proof in practice. If you care about security of your VMs, you need to run them yourself on hardware that you control, using security patched customized Xen/KVM. If you run VMs in the cloud, you do not actually care about security. Some people care really only about appearances and compliance checkboxes, maybe this formally verified thing will catch on for those.

monocasa 5y ago
We'd have to see their code to know for sure, but they're doing the right things to follow in the footsteps of non bullshit formal verification like sel4. Reducing the size of the checked code to ~4kloc, only checking ARM which (thanks to projects like sel4) has the correct infrastructure built up, etc. Can you point to some truly formally verified software that turned out to be bullshit so we can compare their techniques?
- posix_me_less 5y ago
  I didn't say formally verified software is bullshit. I said the marketing here is. FV software exists but its benefits are very limited (basically it's a debugging tool). Running VMs on x86 or ARM in cloud has much more serious problems related to security than using not-formally-verified hypervisor.
  - monocasa 5y ago
    It's more than a debugging tool as it allows you talk confidently about entire classes of vulnerabilities rather than the wack-a-mole of fixing bugs traditionally. And it's a big enough deal that the rumor is that Amazon and Microsoft's type 1 hypervisors have been formally verified. I wouldn't be surprised if Google's is too.
    - posix_me_less 5y ago
      It allows academics and other informed scientists to talk confidently about their design. Everybody else like Linux admins and VM users is still working with a black box software. Sure cloud vendors may get on board and start announcing how their solution is the best verified software out there. Did I mention bullshit marketing yet?
      - touisteur 5y ago
        I don't understand. If I've proved the absence of runtime errors in some code, in addition to classical tests, are you saying that the software is not less likely to crash? Yes, there can be errors everywhere but I don't get this complete rejection of Formal verification tools as 'just a debugging tool'.
        posix_me_less 5y ago
        It is less likely to crash after you complete the proof than if you couldn't complete the proof, but this does not mean this benefit will be worth much. In general, all things being equal, software less likely to crash in production is an improvement, but: 1) all things are usually not equal, because verified software is hard to produce and typically much more restrictive and hard to modify 2) how often do standard industry solutions for hypervisor like Xen or KVM crash? Uptime/customer loss due to hypervisor crashes is a negligibly small problem. The user software should rather work with the assumption that crash can happen. That is much more robust architecture than relying on some proofs that nobody checked.
        touisteur 5y ago
        Though I agree about being 'crash proof' we're talking security here, so DoS or RCE might happen because of a buggy parser, crash or no crash. If I can create a parser that won't produce any error whatsoever, and always return something (be it 'malformed message'), haven't I increased the security of my external interfaces, compared to, let's say, a shit parser full of UB and no check because the program is crashes happen anyway?
tyingq 5y ago
I agree that formal verification isn't, by itself, some kind of panacea. Reading the paper, though, the effort did uncover some issues. Two examples, though there are more: "When proving invariants for page ownership used in the noninterference proofs, we identified a race condition in stage 2 page table updates" "KCore initially did not check if a gfn was mapped before updating a VM’s stage 2 page tables, making it possible to overwrite existing mappings" So mapping out the rules/flow in Coq, and then seeing what actually happened did uncover some flaws. As to whether the juice was worth the squeeze, I don't know this space well enough to comment.
- posix_me_less 5y ago
  Yes, formal methods can be useful, they help uncover bugs. It's a debugging tool, albeit a very demanding one. For some software, it makes sense to use it. Real deployment of VMs has larger problems with security than not formally verified hypervisor so I think the answer for most hosting companies is "the juice is not worth the squeeze" here, the squeeze being the restriction to academic verified design. Hosting VMs is mostly about features and reliability. Those who need also real security, will host on their own HW and won't allow foreign VMs, so formally verified hypervisor is less of a requirement there too. It's a "nice to have".
  - exdsq 5y ago
    Is it a debugging tool if the work is done upfront before writing code?
    - posix_me_less 5y ago
      Yes. Debugging tool reduces number of bugs in the product. Formal design specification and design verification can do that. And even with something lackluster like gdb, you may be forced to do some redesigning before writing more of new code.
teakettle42 5y ago
> "Machine checked formally verified" is a long-known buzzword that screams bullshit marketing. Long-known to who, exactly? How is "formal verification" even remotely a marketing buzzword?
- posix_me_less 5y ago
  To people interested in software process. There is a consensus that formal verification and automatic checks in software (even hardware) are a debugging tool, not a comprehensive success/security policy like the linked article would suggest.
  - cvwright 5y ago
    "People interested in software process" have been trying, and failing, to write secure C code for 50 years. But they've made a ton of money trying!
    - posix_me_less 5y ago
      C was not initially intended for such a thing, although later people tried to restrict it. Also, "secure C code" is too vague. It depends on the scope. Grep is quite secure in what it does. Linux, less so.
  - touisteur 5y ago
    I'm curious where you get this consensus. It's not at all shared by everyone, especially with the huge strides SPARK and Frama-C have made.
    - posix_me_less 5y ago
      I didn't mean academic consensus. More like industry / security-aware people in IT consensus - almost nobody in software does formal verification and it would be foolish for any user, whether person, business or government, to take this as solution to their VM hosting security problems. Yes formal verification has made advancements and is a useful tool, in proper context. Not in the context the article is selling the work of the researchers.

tyingq 5y ago

Discussed a couple of weeks ago based on a different article: https://news.ycombinator.com/item?id=27275707 https://news.ycombinator.com/item?id=27275707 Also see: http://nieh.net/pubs/ieeesp2021_kvm.pdf http://nieh.net/pubs/ieeesp2021_kvm.pdf (The paper) https://microv.org/ https://microv.org/ (A website with more detail, Coq source, etc)

xpuente 5y ago
Right and... > Side-channel attacks [20],[21], [22], [23], [24], [25] are beyond the scope of the paper If all current hardware (i.e. OOO and caches) is vulnerable to speculative side-channel attacks, how they dare to say that is secure? With current hardware, nothing is secure (full stop)
- tyingq 5y ago
  Most of the angst here seems to be around the phrase "provably secure". I don't think they meant that in the same sense that it's being received here. "Provably <xyz>" is just the common terminology in the theorem prover space. Though they seem to be familiar enough with the real world to have known that would have sounded overly grandiose. I think what they really meant was something like "Provably Implements Whatever Security Boundaries That It Claims To".
- naasking 5y ago
  > If all current hardware (i.e. OOO and caches) is vulnerable to speculative side-channel attacks, how they dare to say that is secure? The software is provably secure. That doesn't mean a complete solution consisting of software and hardware is necessarily secure, and it has never meant that.
  - xpuente 5y ago
    Then, what is the value of making the software secure if the hardware isn't? The hardware issue is terrifying. And the worst part, it seems not possible to fix it without trowing away decades of performance enhancements. This epic screw-up of epic dimensions from computer architecture guys won't go away that easy.

IncRnd 5y ago

> SeKVM Makes Cloud Computing Provably Secure > Columbia University researchers have created a secure Linux-based hypervisor > Now computer scientists at Columbia University have developed what they say is the first hypervisor that can guarantee secure cloud computing. > The researchers dubbed their new technique microverification, which reduces the amount of work needed to verify a hypervisor. It breaks down a hypervisor into a small core and a set of untrusted services, and then goes on to prove the hypervisor secure by verifying the core alone. The core has no vulnerabilities for a hack to exploit, and this core mediates all the hypervisor's interactions with virtual machines, so even if a hack undermines one virtual machine, it does not compromise the others. It sad how IEEE's Spectrum carried this nonsense. There clearly wasn't any real technical review of these statements prior to publishing.

pizzazzaro 5y ago
Im skeptical of the way these researchers declared so much to be "out of bounds." Where can I find the source code? I wanna see if I can... Idk, patch that. Since this is derivative of gpl code in Linux Kernel, whats our chances of getting to inspect it ourselves?