[HN Gopher] SeKVM verified hypervisor based on KVM
___________________________________________________________________
SeKVM verified hypervisor based on KVM
Author : cvwright
Score : 61 points
Date : 2021-06-08 12:13 UTC (10 hours ago)
(HTM) web link (spectrum.ieee.org)
(TXT) w3m dump (spectrum.ieee.org)
| posix_me_less wrote:
| 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.
| tyingq wrote:
| 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 wrote:
| 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 wrote:
| Is it a debugging tool if the work is done upfront before
| writing code?
| posix_me_less wrote:
| 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 wrote:
| > "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?
| naasking wrote:
| 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.
| posix_me_less wrote:
| 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.
| naasking wrote:
| > 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.
| posix_me_less wrote:
| 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.
| exdsq wrote:
| Might be of interest but a few blockchain projects use
| formal methods like Agda, Coq, TLA+, etc
| posix_me_less wrote:
| 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 wrote:
| "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 wrote:
| 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 wrote:
| 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 wrote:
| 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.
| monocasa wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| 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.
| madsbuch wrote:
| Just entering this troll thread for a small correction:
|
| > ... relying on some proofs that nobody checked
|
| It is indeed check every single time the software
| compiles.
| touisteur wrote:
| 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?
| posix_me_less wrote:
| @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.
| tyingq wrote:
| Discussed a couple of weeks ago based on a different article:
| https://news.ycombinator.com/item?id=27275707
|
| Also see:
|
| http://nieh.net/pubs/ieeesp2021_kvm.pdf (The paper)
|
| https://microv.org/ (A website with more detail, Coq source, etc)
| xpuente wrote:
| 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 wrote:
| 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 wrote:
| > 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 wrote:
| 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.
| Nullabillity wrote:
| 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.
| Veserv wrote:
| 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.
|
| [1] https://zerodium.com/program.html
|
| [2] https://www.zdnet.com/article/google-this-spectre-
| proof-of-c...
| krapht wrote:
| 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(tm).
|
| 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.
| stonewareslord wrote:
| What are you using for JS whitelisting? I used to used
| uMatrix before it died.
| krapht wrote:
| 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.
| IncRnd wrote:
| > 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 wrote:
| 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?
___________________________________________________________________
(page generated 2021-06-08 23:02 UTC)