Columbia Engineering Team Builds First Hacker-Resistant Cloud Software System | Hacker News Reader

Columbia Engineering Team Builds First Hacker-Resistant Cloud Software System

engineering.columbia.edu

9 pointsbillyharris21 comments

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

> 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.

This site also has the coq source: https://microv.org/

this is the interesting bit

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.

I believe most public cloud providers pin different user VMs to separate physical cores, which defends a lot against these attacks because you aren't sharing a branch predictor or an L1 cache with other people.

And qemu comes with other mitigations: https://www.qemu.org/2018/02/14/qemu-2-11-1-and-spectre-upda...

“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.

> But the grandiose framing seems a bit…

Appropriate/necessary for a publicly funded research project?

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.

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.

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.

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.

What even is hacker resistant?

Security is far more than secure VM hosting...

one person opens a phishing email

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

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

> 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/ronghu...

That looks like a title from The Onion.

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

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.

> 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.

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.

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.

Reply on news.ycombinator.com