4 ms·

Columbia Engineering Team Builds First Hacker-Resistant Cloud Software System

9 points by billyharris 5y ago

lettergram 5y ago
This seems like all cloud software? Seriously, what do they think Google and AWS do?
- deleted 5y ago
  [deleted]
- latch 5y ago
  > what do they think Google and AWS do Reading the article, it seems they think Google and AWS don't do formal verification of the hypervisor. Since they won a grant from Amazon to do this (1), I'm going to guess that maybe they're right? (1) https://www.amazon.science/research-awards/recipients/ronghui-gu-2020 https://www.amazon.science/research-awards/recipients/ronghu...
peterbonney 5y ago
“This system is provably secure.” Okay, against what specific threat model? Can it protect against an admin’s password/key being stolen/hacked/guessed or any of the other extremely mundane attacks you’re actually likely to encounter in the real world? I’m sure the CS is novel and excellent. But the grandiose framing seems a bit… much.
- marmaduke 5y ago
  > But the grandiose framing seems a bit… Appropriate/necessary for a publicly funded research project?
  - craftinator 5y ago
    Inappropriate, because to someone who has real knowledge on the subject, it sounds like bullshit, and to everyone else it sounds like a quantum leap. Smells like Theranos.
    - dvfjsdhgfv 5y ago
      The main job of the PR manager who wrote this piece is to make stories like these heard. The researchers did a very good job indeed and I doubt any of them would use such a silly title - since the very core of their research is formal verification, it means they're very precise folks and would never call their system "hacker-resistant"; there are several other names, more adequate but less clickbaity.
      - craftinator 5y ago
        I don't disagree with you, but on the same line of thinking, why not call it "A system that solves all hacking everywhere, permanently"? When going down the rabbit hole of disingenuousness for the sake of wider reach, the more you lie about the actual subject, the less you are actually talking about the subject, and the more you're talking about something that doesn't exist. It is very bad marketing to describe a precise system using very little precision.
  - rambojazz 5y ago
    Your comment actually matches my experience. Projects with grandiose descriptions that sound completely BS. Why do publicly funded research project need to use these "tactics"? In my experience these projects attract the very kind of people that I don't like to work with; people with long CVs that like to speak with buzzwords and that don't build anything interesting or valuable.
bearjaws 5y ago
What even is hacker resistant? Security is far more than secure VM hosting... one person opens a phishing email
imranhou 5y ago
When something seems too good to be true, it usually is.
ct0 5y ago
What do you have to do, mail in your data?
geofft 5y ago
Ignore the overly-excited university press release office and read the paper, A Secure and Formally Verified Linux KVM Hypervisor: http://nieh.net/pubs/ieeesp2021_kvm.pdf http://nieh.net/pubs/ieeesp2021_kvm.pdf > Commodity hypervisors are widely deployed to support virtual machines (VMs) on multiprocessor hardware. Their growing complexity poses a security risk. To enable formal verification over such a large codebase, we introduce microverification, a new approach that decomposes a commodity hypervisor into a small core and a set of untrusted services so that we can prove security properties of the entire hypervisor by verifying the core alone. To verify the multi-processor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we introduce data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data, while retaining KVM’s functionality and performance. Our work is the first machine- checked security proof for a commodity multiprocessor hypervisor.
- tyingq 5y ago
  This site also has the coq source: https://microv.org/ https://microv.org/
- marmaduke 5y ago
  this is the interesting bit
- caust1c 5y ago
  No mention of Spectre or Meltdown? I'm all for improving formal verification but their method ignores the fact that there are leaky abstractions throughout the stack, those of which enable vulnerabilities. That is, this seems like total BS: > we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification Edit: they do mention it: > Side-channel attacks [20],[21], [22], [23], [24], [25] are beyond the scope of the paper So basically they've developed a method for formally verifying components of systems, by making assumptions about the periphery.
duckfang 5y ago
This sounds like dumb marketing material of "This is the only security software you need!" Turing completeness means there's nigh infinite ways to convolute malware that will evade all scanners. And as long as users have capabilities to their data, they will be subject to attacks against data they have access to. Tl;dr. Grandiose claims require grandiose proof.
- geofft 5y ago
  > Turing completeness means there's nigh infinite ways to convolute malware that will evade all scanners. No, it does not. Turing-completeness simply means that for certain properties which could be true or false about some software (like whether it halts), given an arbitrary piece of software, you won't always know whether or not it satisfies the property. It does not prevent you from assuming "No" in the cases where you don't know. Nor does it prevent there from being other properties (e.g., ability to access another user's data) for which the answer is always no.
  - duckfang 5y ago
    I work in this area. And yes, for any function that does malware, there's an infinity of similar functions that do the same. And you cannot catch them all. What you typed is good for an academic setting, in the "wellactually technical correct" sense of the term.
    - geofft 5y ago
      The solution I outline is exactly how countless real-world systems, from cloud computing to web browsers to eBPF, safely run user-provided arbitrary code.
rambojazz 5y ago
That looks like a title from The Onion.

9 points by billyharris 5y ago

lettergram 5y ago

This seems like all cloud software? Seriously, what do they think Google and AWS do?

deleted 5y ago
[deleted]
latch 5y ago
> what do they think Google and AWS do Reading the article, it seems they think Google and AWS don't do formal verification of the hypervisor. Since they won a grant from Amazon to do this (1), I'm going to guess that maybe they're right? (1) https://www.amazon.science/research-awards/recipients/ronghui-gu-2020 https://www.amazon.science/research-awards/recipients/ronghu...

peterbonney 5y ago

“This system is provably secure.” Okay, against what specific threat model? Can it protect against an admin’s password/key being stolen/hacked/guessed or any of the other extremely mundane attacks you’re actually likely to encounter in the real world? I’m sure the CS is novel and excellent. But the grandiose framing seems a bit… much.

marmaduke 5y ago
> But the grandiose framing seems a bit… Appropriate/necessary for a publicly funded research project?
- craftinator 5y ago
  Inappropriate, because to someone who has real knowledge on the subject, it sounds like bullshit, and to everyone else it sounds like a quantum leap. Smells like Theranos.
  - dvfjsdhgfv 5y ago
    The main job of the PR manager who wrote this piece is to make stories like these heard. The researchers did a very good job indeed and I doubt any of them would use such a silly title - since the very core of their research is formal verification, it means they're very precise folks and would never call their system "hacker-resistant"; there are several other names, more adequate but less clickbaity.
    - craftinator 5y ago
      I don't disagree with you, but on the same line of thinking, why not call it "A system that solves all hacking everywhere, permanently"? When going down the rabbit hole of disingenuousness for the sake of wider reach, the more you lie about the actual subject, the less you are actually talking about the subject, and the more you're talking about something that doesn't exist. It is very bad marketing to describe a precise system using very little precision.
- rambojazz 5y ago
  Your comment actually matches my experience. Projects with grandiose descriptions that sound completely BS. Why do publicly funded research project need to use these "tactics"? In my experience these projects attract the very kind of people that I don't like to work with; people with long CVs that like to speak with buzzwords and that don't build anything interesting or valuable.

bearjaws 5y ago

What even is hacker resistant? Security is far more than secure VM hosting... one person opens a phishing email

imranhou 5y ago

When something seems too good to be true, it usually is.

ct0 5y ago

What do you have to do, mail in your data?

geofft 5y ago

Ignore the overly-excited university press release office and read the paper, A Secure and Formally Verified Linux KVM Hypervisor: http://nieh.net/pubs/ieeesp2021_kvm.pdf http://nieh.net/pubs/ieeesp2021_kvm.pdf > Commodity hypervisors are widely deployed to support virtual machines (VMs) on multiprocessor hardware. Their growing complexity poses a security risk. To enable formal verification over such a large codebase, we introduce microverification, a new approach that decomposes a commodity hypervisor into a small core and a set of untrusted services so that we can prove security properties of the entire hypervisor by verifying the core alone. To verify the multi-processor hypervisor core, we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification, and the top layer specification is refined by all layers of the core implementation. To verify commodity hypervisor features that require dynamically changing information flow, we introduce data oracles to mask intentional information flow. We can then prove noninterference at the top layer specification and guarantee the resulting security properties hold for the entire hypervisor implementation. Using microverification, we retrofitted the Linux KVM hypervisor with only modest modifications to its codebase. Using Coq, we proved that the hypervisor protects the confidentiality and integrity of VM data, while retaining KVM’s functionality and performance. Our work is the first machine- checked security proof for a commodity multiprocessor hypervisor.

tyingq 5y ago
This site also has the coq source: https://microv.org/ https://microv.org/
marmaduke 5y ago
this is the interesting bit
caust1c 5y ago
No mention of Spectre or Meltdown? I'm all for improving formal verification but their method ignores the fact that there are leaky abstractions throughout the stack, those of which enable vulnerabilities. That is, this seems like total BS: > we introduce security-preserving layers to modularize the proof without hiding information leakage so we can prove each layer of the implementation refines its specification Edit: they do mention it: > Side-channel attacks [20],[21], [22], [23], [24], [25] are beyond the scope of the paper So basically they've developed a method for formally verifying components of systems, by making assumptions about the periphery.

duckfang 5y ago

This sounds like dumb marketing material of "This is the only security software you need!" Turing completeness means there's nigh infinite ways to convolute malware that will evade all scanners. And as long as users have capabilities to their data, they will be subject to attacks against data they have access to. Tl;dr. Grandiose claims require grandiose proof.

geofft 5y ago
> Turing completeness means there's nigh infinite ways to convolute malware that will evade all scanners. No, it does not. Turing-completeness simply means that for certain properties which could be true or false about some software (like whether it halts), given an arbitrary piece of software, you won't always know whether or not it satisfies the property. It does not prevent you from assuming "No" in the cases where you don't know. Nor does it prevent there from being other properties (e.g., ability to access another user's data) for which the answer is always no.
- duckfang 5y ago
  I work in this area. And yes, for any function that does malware, there's an infinity of similar functions that do the same. And you cannot catch them all. What you typed is good for an academic setting, in the "wellactually technical correct" sense of the term.
  - geofft 5y ago
    The solution I outline is exactly how countless real-world systems, from cloud computing to web browsers to eBPF, safely run user-provided arbitrary code.

rambojazz 5y ago

That looks like a title from The Onion.