> 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)
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".
> 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.
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.
Because software is the weak link, not the hardware. It only costs Zerodium $200k for a VMware virtual machine escape [1] which would allow GB/s data exfiltration in contrast to a Spectre attack which only has data rates on the order of KB/s [2]. Finding zero-days in mass deployed, foundational software like operating systems or hypervisors only costs on the order of $100k-$1M and occurs routinely. In contrast, finding vulnerabilities in hardware that breach confidentiality (read-protection) or integrity (write-protection) are so rare that it is a media event when one is discovered every decade or so of aggressive searching. Hardware is literally 100x harder to successfully attack than software. We would be lucky if we had systems that were only as secure as their hardware since they would be 100x better than the status quo.
While the hardware situation isn't ideal, secure software + vulnerable hardware is still better a better place to be in than vulnerable software + vulnerable hardware.
Is not an epic screw-up. More like 99.9% of compute is not done in adversarial untrusted sandboxes, so who cares if another process with a lot of work can extract data from another one.
You leave so much performance on the table if you demand cryptographically secure perf for everything. That means no caching, everything runs in fixed, worst case time, and the amount of work must be fixed as well so there is not any variation in power draw.
Here is a simpler solution - do not run untrusted code on your computer. It is just that easy™.
PS: I disable JavaScript by default in my browser, and manually whitelist exceptions, for the same reason. I also turned off Spectre mitigation on my workstation.
uMatrix developer moved on to primarily work on uBlock Origin. It is a good successor.
I think some people do not like UBo because by default it is a little light on blocking so most websites just work. Well, you can configure it to block more things, and if you use uMatrix you already are willing to deal with the pain of this process.
> 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.
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.
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.
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".
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.
I was thinking the same thing. I've never seen "formally verified" used in marketing because almost nobody is willing to put in the money and effort to formally verify software. The only places I've seen it done is when security and reliability is essential to critical operations, like the seL4 kernel.
The marketing for FV is indeed rare in larger software industry, probably because of quite small susceptible market. The latter is small, because 1) the FV process is expensive 2) it gives only limited benefits.
Most of the marketing that exists for FV in software is done by academia and few MIC companies like Greenhills Software or General Dynamics. In practice almost nobody in software produces formally verified software. And when they do, like the few examples that exist, the proof only guarrantees what design could foresee, and only if assumptions are satisfied which is not trivial in real deployments. It may work for avionics on special isolated simple hardware, but cloud hosted VMs on x86/ARM connected to Internet is probably too far.
> And when they do, like the few examples that exist, the proof only guarrantees what design could foresee, and only if assumptions are satisfied which is not trivial in real deployments.
In other words, formal verification can:
1. provide guarantees that the implementation matches the spec,
2. that the spec fulfills certain properties, including but not limited to security, safety, reliability properties
These are typically more guarantees that non-verified software, so I still fail to see how this is bullshit marketing.
In this case, they proved that there are no overt information flow vulnerabilities in the design or implementation, so you're left only with the covert channels. That's clearly a valuable property to know.
If Intel, AMD or RISC-V releases a covert-channel free CPU, then you can even close those and it's secure from top to bottom.
Yes but the spec is often unknown (C language, GCC compiler, Linux) or flawed (speculative execution processors, which we know since Spectre).
The fact there is a formally verified piece of design and software is not bullshit. I said the marketing here is bullshit. This shiny piece of great software won't solve our security problems in multiuser environments, because the proof works only under a very limited set of assumptions. You can't just run your VMs in the cloud on this FV hypervisor and think your software security problems are solved.
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.
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.
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.
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?
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.
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.
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?
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'.
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.
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?
@madsbuch I meant classical "Dijkstra-style" proofs. I know about automated proofs, they are great accomplishment, and software that they produce may be good. I wouldn't believe those automated proofs any more than I would believe human-made proofs. Errors in intent and design can happen, I still want to test the resulting software in action and have the option to easily modify it.
Also see:
http://nieh.net/pubs/ieeesp2021_kvm.pdf (The paper)
https://microv.org/ (A website with more detail, Coq source, etc)