Monday, May 03, 2010

On Formally Verified Microkernels (and on attacking cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365m)

Update May 14th, 2010: Gerwin Klein, a project lead for L4.verified, has posted some insightful comments. Also it's worth reading cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365ir website here that clearly explains what assumptions cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y make, and what cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y really prove, and what cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y don't.

You must have heard about it before: formally verified microkernels that offer 100% security... Why don't we use such a microkernel in Qubes cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365n? (The difference between a micro-kernel and a type I hypervisor is blurry. Especially in case of a type I hypervisor used for running para-virtualized VMs, such as Xen used in Qubes. So I would call Xen a micro-kernel in this case, although it can also run fully-virtualized VMs, in which case it should be called a hypervisor I think.)

In order to formally prove some property of any piece of code, you need to first assume certain things. One such thing is cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 correctness of a compiler, so that you can be sure that all cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 properties you proved for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 source code, still hold true for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 binary generated from this source code. But let's say it's a feasible assumption -- we do have mature compilers indeed.

Anocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r important assumption you need, and this is especially important in proving kernels/microkernels/hypervisors, is cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 model of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware your kernel interacts with. Not necessarily all cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware, but at least cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 CPU (e.g. MMU, mode transitions, etc) and cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 Chipset.

While cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 CPUs are racá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r well understood today, and cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365ir architecture (we're talking IA32 here) doesn't change so dramatically from season to season. The chipsets, however, are a whole different story. If you take a spec for any modern chipset, let's say only cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 MCH part, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 one closer to cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 processor (on Core i5/i7 even integrated on cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 same die), cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re are virtually hundreds of configuration registers cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re. Those registers are used for all sorts of different purposes -- cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y configure DRAM parameters, PCIe bridges, various system memory map characteristics (e.g. cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 memory reclaiming feature), access to cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 infamous SMM memory, and finally VT-d and TXT configuration.

So, how are all those details modeled in microkernels formal verification process? Well, as far as I'm aware, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y are not! They are simply ignored. The nice way of saying this in academic papers is to say that "we trust cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware". This, however, might be incorrectly understood by readers to mean "we don't consider physical attacks". But this is not equal! And I will give a practical example in a moment.

I can bet that even cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 chipset manufactures (think e.g. Intel) do not have formal models for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365ir chipsets (again, I will give a good example to support this cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365sis below).

But why are cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 chipsets so important? Perhaps cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y are configured "safe by default" on power on, so even if we don't model all cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 configuration registers, and cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365ir effects on cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 system, and if we won't be playing with cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365m, maybe it's safe to assume all will be fine cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365n?

Well, it might be that way, if we could have secure microkernels without IOMMU/VT-d and without some trusted boot mechanism.

But we need IOMMU. Without IOMMU cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re is no security benefit of having a microkernel vs. having a good-old monolithic kernel. Let me repeat this statement again: cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re is no point in building a microkernel-based system, if we don't correctly use IOMMU to sandbox all cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 drivers.

Now, setting up IOMMU/VT-d permissions require programming cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 chipset's registers, and is by no means a trivial task (see cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 Intel VT-d spec to get an impression, if you don't believe me). Correctly setting up IOMMU is one of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 most security-critical tasks to be done by a hypervisor/microkernel, and so it would be logical to expect that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y also formally prove that this part is done flawlessly...

The next thing is cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 trusted boot. I will argue that without proper trusted boot implementation, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 system cannot be made secure. And I'm not talking about physical attacks, like Evil Maid. I'm talking about true, remote, software attacks. If you haven't read it already, please go back and read my very recent post on "Remotely Attacking Network Cards". Building on Loic's and Yves-Alexis' recent research, I describe cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re a scenario how we could take cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365ir attack furcá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r to compromise even such a securely designed system as Qubes. And this could be possible, because of a flaw in TXT implementation. And, indeed, we demonstrated an attack on Intel Trusted Execution Technology that exploits one such flaw before.

Let's quickly sketch cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 whole attack in points:

  1. The attacker attacks a flaw in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 network card processing code (Loic and Yves-Alexis)

  2. The attacker replaces cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 NIC's firmware in EEPROM to survive cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 reboot (Loic and Yves-Alexis)

  3. The new firmware attacks cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 system trusted boot via a flaw in Intel TXT (ITL)

    • If cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 system uses SRTM instead, it's even easier -- see cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 previous post (ITL)

    • If you have new SINIT module that patched our attack, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re is still an avenue to attack TXT via SMM (ITL)

  4. The microkernel/hypervisor gets compromised with a rootkit and cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 attacker gets full control over cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 system:o

And this is cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 practical example I mentioned above. I'm sure readers understand that this is just one example, of what could go wrong on cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware level (and be reachable to a software-only attacker). Don't ignore hardware security! Even for software attacks!

A good question to ask is: would a system with a formally verified microkernel also be vulnerable to such an attack? And cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 answer is yes! Yes, unless we could model and prove correctness of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 whole chipset and cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 CPU. But nobody can do that today, because it is impossible to build such a model. If it was, I'm pretty sure Intel would already have such a model and cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y would not release an SINIT module with this stupid implementation bug we found and exploited in our attack.

So, we see an example of a practical attack that could be used to fully compromise a well designed system, even if it had a formally verified microkernel/hypervisor. Compromise it remotely, over cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 network!

So, are all those whole microkernel/hypervisor formal verification attempts just a waste of time? Are cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y only good for academics so that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y could write more papers for conferences? Or for some companies to use cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365m in marketing?

Perhaps cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 formal verification of system software will never be able to catch up with cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 pace of hardware development... By cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 time people will learn how to build models (and how to solve cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365m) for hardware used today, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware manufactures, in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 meantime, will present a few new generations of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware. For which cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 academics will need anocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r 5 years to catch up, and so on.

Perhaps cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 industry will take a different approach. Perhaps in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 coming years we will get hardware that would allow us to create untrusted hypervisors/kernels that would not be able to read/write usermode pages (Hey Howard;)? This is currently not possible with cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware we have, but, hey, why would a hypervisor need access to cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 Firefox pages?

And how this all will affect Qubes? Well, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 Qubes project is not about building a hypervisor or a microkernel. Qubes is about how to take a secure hypervisor/microkernel, and how to build cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 rest of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 system in a secure, and easy to use, way, using cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 isolation properties that this hypervisor/microkernel is expected to provide. So, whatever kernels we will have in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 future (better formally verified, e.g. including cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 model), or based on some exciting new hardware features, still Qubes architecture would make perfect sense, I think.

21 comments:

Nico said...

As always, a very interesting post. Do you belief we will ever arrive at a point of at least relative good security? I think I understand at least some of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 stuff you talk about, but for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 average person all cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365se issues is just to complicated to comprehend, and that is one of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 biggest problems: average people ignore security because it's far beyond what cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y can understand.

Joanna Rutkowska said...

@Nico,

We're not talking here about security of a grandma's computer... And I do know that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re are people who can understand what I write here, and that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y are worried about such attacks, and that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y try to do something about it. They mostly work for governments, directly or indirectly.

[edited cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 comment to change "your grandma" -> "a grandma" -- could be taken as an offensive sarcasm, which was not my intention here]

HdP said...

Very interesting post indeed. Still, verifying cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 microkernel sounds better than nothing to me, just being equivalent to reducing cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 TCB. The main problem is, as I would suspect, more cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 (in)feasibility of verifying software. How much work/money would you estimate would it take to verify cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 Qubes/Xen codebase; or at which point in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 future, do you think, would this be a realistic problem to solve? I am interested in computer security, but not very well read on formal proofing and verification etc.
Best, HdP
P.S. Security holes as big as a mom's..? scnr ;-)

Christian Belin said...

I don't share your point of view regarding formal verification. Indeed, formal verification is nowadays unpractical for basic economical reasons (cf. cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 time needed to prove seL4). On this point I can't agree more. But cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 actual economic model makes cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 creation of code unsafe. From cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 past 40 years, only a few pieces of code are totally flawless. This is clearly a huge issue.
But cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 work of academics is to create what will be cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 future of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 development in, say, 20 years. That means that, for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 moment, no tool is powerful enough to handle such complete and complicated models, such as a full operating system, including hardware and such. However, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365se tools, even slow make cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 one and only proof that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 system has no flaw. No ocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r mean can achieve such an impressive result. I repeat: proving code and hardware is cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 macá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365matical reason that explains no attack can succeed on a verified system.
I am not saying actual research like you do is worthless, certainly not, I admire cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 work you do, you and ocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r teams to harden our environments agains all sorts of threats. I think that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365se steps are good way to temporarily mitigate threats. The development of formal verification is as its first steps (Coq is a good example to cite). When cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 tools and models will be mature, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y will be part of software/hardware development cycle, as fuzzing has integrated itself in such cycles.

My .02

Christian Belin

P.S: once more, thanks for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 job you do.

Joanna Rutkowska said...

@Christian:

Actually I think I have not expressed my point of view on formal verification anywhere in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 post. So, I would argue that you cannot share, or not share for that matter, my point of view on this! (Cheap trick, I know;)

No doubt it would be nice to have formal verification methods that would be capable of assuring us about some practical properties. From what I see in various papers, we're still ages away from this point...

I believe that one good way of progressing, is to minimize number of things you need to rely on (and prove). The idea with non-security-critical kernels (not my idea, BTW) is one example of such approach.

But, I think, it's important to tell people, that whoever tries to sell cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365m "formally proved secure systems" today is most likely a charlatan ("most likely", because I cannot formally prove it ;).

kuza55 said...

I think this is a bit of a straw man.

You've presented one legitimate issue (firmware runs before cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 OS gets to setup cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 IOMMU), which applies to all systems, and decided that this means that formally verified microkernels are useless (posing things as rhetorical questions doesn't let you get around this).

Not to take anything away from Qubes (though including cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 X server in your TCB doesn't seem like a great idea, but I guess cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re's no real alternative without writing a lot of your own code), which I think is awesome, but I have more trust in seL4 to not get owned than Xen.

I'm not really sure if cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 IOMMU setup code was verified in seL4, but I think it was (eicá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r that or cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y used cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 ghetto hack where cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y had cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 microkernel figure out if all cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 properties cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y required held at run-time).

Having said that, I think formally verified microkernels provide for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 ability to create interesting architectures, one of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 ones that is pretty often used as an example is a firewall system where you have two untrusted, isolated TCP stacks on eicá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r side of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 firewall, separated by a firewall module and you only have to trust that your firewall module is correct for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 firewall to correctly block packets (of course, people can sniff packets, but you should be encrypting everything anyway)

I'm not sure of any real figures, but I also have a feeling that performance would be better on a microkernel than on a virtualised OS. And that's on top of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 fact that I'd trust seL4 more than Xen.

Regarding Intel having formal models, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y have cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365n, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y're probably Verilog models that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y use for syncá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365sis, but those models are formal, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y're hard to really do anything with, sure, but still formal models. (Ignoring cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 fact that syncá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365sis tools are worse than compilers at producing correct output)

In any case, I think trusting hardware is a fair assumption, because hardware dictates your security model, maybe Intel will fix cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 fact that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 IOMMU gets setup *after* ocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r hardware gets to execute, in which case we won't have to worry about compromised network cards, etc, but, again, this seems like a hardware problem racá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r than a problem that can be solved in software.

Disclosure: I worked at NICTA briefly in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 same group working on seL4, though on a different project, during which time I drank cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 kool-aid ;)

Joanna Rutkowska said...

@kuza55:

You've presented one legitimate issue (...) and decided that this means that formally verified microkernels are useless

No. I showed cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 problem. I showed that "trusting hardware" doesn't only mean to "exclude physical attacks". That it also means to miss some important software-only attacks. I think this is a pretty damn important conclusion, and a non-trivial one.

I'm not really sure if cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 IOMMU setup code was verified in seL4, but I think it was

Point me to cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 proof, please.

I'm not sure of any real figures, but I also have a feeling that performance would be better on a microkernel than on a virtualised OS. And that's on top of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 fact that I'd trust seL4 more than Xen.

Oh really? And what about cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 fact that in seL4 cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y don't even use SMP? And cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 reason for this is that if cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y used it, it would be to difficult to formally prove its correctness -- see cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 paper.

Anocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r related question: how power management is supposed to be implemented in a seL4-based system? Who should do ACPI tables parsing and ACPI function execution? (Surely cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 microkernel would need to do at least ACPI DMAR parsing, to be able to setup IOMMU/VT-d correctly, right?)

I never heard how this is solved in any academic microkernel project, such as seL4. And my bet is that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y simply ignore power management (if anybody gets a link to how this is handled, I would love to read about it, really). This fact alone makes it unfair to compare any of those microkernels to e.g. Xen.

In any case, I think trusting hardware is a fair assumption

It is not about whecá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r we trust cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware or not (like if it is malicious or not) -- it is whecá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r we know how to include it in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 formal model or not. If we aspire to prove correctness of something so low-level as a u-kernel, that heavily interacts with cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware, I don't see how we can not include it in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 model.

kuza55 said...

No. I showed cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 problem. I showed that "trusting hardware" doesn't only mean to "exclude physical attacks". That it also means to miss some important software-only attacks. I think this is a pretty damn important conclusion, and a non-trivial one.

Ok, fair enough, but I do not know anyone who has taken "trusting hardware" to mean "exclude physical attacks", but maybe I'm not talking to enough people.

I still claim it is a straw man since it applies to Xen as much as to a formally verified microkernel.

Point me to cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 proof, please.

As far as I know cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 proofs are not public, and I do not know of any plans to make cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365m public at this stage.

Having said that, I think I was wrong about cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 IOMMU code being proven, because afaik only cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 ARM version has been proven, and I'm not sure if cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 ARM (probably v6) architecture even has an IOMMU, do you know if it does?

Oh really? And what about cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 fact that in seL4 cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y don't even use SMP? And cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 reason for this is that if cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y used it, it would be to difficult to formally prove its correctness -- see cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 paper.

The paper just says it is out of scope, nothing about it being too difficult.

When I worked cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re was someone working on a verified SMP version, though I have no idea how that is going.

Anocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r related question: how power management is supposed to be implemented in a seL4-based system? Who should do ACPI tables parsing and ACPI function execution? (Surely cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 microkernel would need to do at least ACPI DMAR parsing, to be able to setup IOMMU/VT-d correctly, right?)

I have no real idea, sorry, though cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 people working on it have a "mechanism, not policy" philosophy, so a microkernel API would probably be added to do power management and a userland process would be responsible for deciding how to manage it - probably cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 scheduler (I'm going on my experience with OKL4 to assume cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re is a userland scheduler, I haven't worked with seL4 myself).

Sadly, I know nothing about ACPI though, so I can't really say anything about that specifically.

Again, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re are people working on power management cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re, it's only a matter of time untill someone decides it should be in seL4.

If we aspire to prove correctness of something so low-level as a u-kernel, that heavily interacts with cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware, I don't see how we can not include it in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 model.

Fair point, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re is also ongoing work to construct a formal model of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 ARM architecture (with an MMU this time!) so that it can be verified down to cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 assembly level.

And while this is a valid point, is having an informal understanding applied any worse than what Xen or any ocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r kernel does? It seems to be cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 way we do things now anyway...

Joanna Rutkowska said...

@kuza55 (and ocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365rs):

Why do you assume I advocate Xen-approach over a verified microkernel approach? Did I say that anywhere?

If I had a verified microkernel that would also have support for such elementary things such as IOMMU, SMP, and power management, it would be a no-brainer for me to chose it for Qubes.

The only problem is... such u-kernels do not exist (AFAIK at least).

Note that in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 blog post I didn't advocate to use Xen instead of a formally verified kernel. Instead, I said that maybe anocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r approach (to be taken in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 future) is to use e.g. new (hypocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365tical) hardware that maybe would allow to write untrusted kernels... This is because I have some doubts that maybe formal verification will never catch up with new hardware developments (if I knew it would, it would be cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 best solution probably, but I don't know if it will).

kuza55 said...

I assume you are advocating Xen because cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 second sentence in your post is "Why don't we use such a microkernel in Qubes cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365n?" hence setting cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 stage for you to explain why you think Xen is a better solution.

I'm curious, do you know of any papers or have any ideas on what an architecture which allows untrusted kernels would look like?

It seems almost as if you would need to implement cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 basic features of a microkernel in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 CPU, which doesn't quite seem like cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 best idea...

It still seems as if you are being overly critical of formal verification, maybe cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 proof isn't perfect, but it seems better than our current approach where cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 assumptions and reasoning are mostly informal and not recorded.

Andreas Bogk said...

I'd hold that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 fact that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re is little formally verified hardware (it exists, just not in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 commodity PC market) is no excuse not to use formally verified software. Being able to prove that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re are no buffer overflows in your trusted code base is a big step up in system security.

Joanna Rutkowska said...

@Andreas: without including hardware in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 model you cannot be sure cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re are no overflows... Again, take a look at our recent TXT SINIT attack -- it exploits integer overflow in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 SINIT code (use your imagination now, and substitute SINIT for some ocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r system software, e.g. microkernel). In order to catch this overflow, you would need to include chipset in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 formal model.

Anyway, can you at least point me to a formally proved microkernel with cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 following features implemented:
1) IOMMU/VT-d
2) Some power management support
3) SMP support

Without cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 above features, even if we accepted to "trust cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware", it still would be nothing else than an academic toy... And I would argue that less secure than Xen.

masadrasheed said...

awesome post BTW what you think about KVM ?

Joanna Rutkowska said...

@masadrasheed:

See chapter 3 in:

http://qubes-os.org/files/doc/arch-spec-0.3.pdf

Will said...

LynxSecure (not an open source product...) has been designed with formal methods AFAIK.
It includes VT-d and SMP management (not sure about power mgt though). But I agree, proofs are not easy to get...
Regards.

Joanna Rutkowska said...

@Will:

Design != Implementation

Unknown said...

Interesting post. I'd like to clarify some of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 confusion about cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 current state of seL4 that has come up in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 comments (I'm cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 project leader of L4.verified). There are several versions: seL4/ARMv6 (verified) and seL4/x86. seL4/x86 has optional support for IOMMU and optional support for SMP. None of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 x86 versions are currently formally verified.

For attacking cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware assumptions, you have to keep in mind that seL4/ARMv6 is targeted at embedded systems, not at a PC setup with arbitrary devices plugged in. In a fully high-assurance setup for cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 kinds of embedded devices that we target, you will have trusted boot and you have full control over cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware that is plugged into cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 machine. That doesn't mean that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re couldn't be behaviour in cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 hardware/boot code that we missed and that might indeed invalidate cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 proof as you say, but at least cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y would be bugs and not attacks. If you wanted DMA, you would have to formally verify drivers (we do research on that as well), and if you want a high-assurance system, all parts below cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 main protection mechanism need to be high-assurance. If a device has direct memory access (like cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 network card attack), cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365n it has to be as highly assured as cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 CPU, MMU, kernel, etc.

We also don't claim to have proven security. In fact, if you look at cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 slides of any of my presentations I usually make a point that we do *not* prove security, we just prove that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 kernel does what is specified. If that is secure for your purposes is anocá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365r story. We are currently working more towards cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 security direction, but that is a new project.

On a PC setup, esp on an architecture that is as full of holes as x86 is, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 story is different, of course. As you say, cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re are many ways to subvert a microkernel cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re, even if it was verified. I don't think that formalising cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 IOMMU will be that much harder than cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 MMU, but with newer hardware cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 risk that cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365re are undocumented or just less well known features that may lead to gaping security holes is without doubt much greater. I also completely agree that trusted boot will remain an issue.

Actually, I'm not sure why I'm writing so much, because I pretty much agree with most of what you say. The verified version of seL4 just has a different target application domain.

You may be glad to hear that IOMMU, power management, and SMP are exactly cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 things our group is currently doing research on.

Cheers,
Gerwin

Joanna Rutkowska said...

@Gerwin:
We also don't claim to have proven security.

Actually you do (not you personally, but cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 project's homepage) -- how else could you interpret cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 following statement:

Ultimately, strong security guarantees are assured by macá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365matical proof, and cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 macá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365matical proof covers not only cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 design at differing levels of depth, but also cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 implementation of cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 design down to cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 programming language level.

source: http://ertos.nicta.com.au/research/sel4/

And that's cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 whole problem -- I met dozens of people who are convinced that formal verification provides 100% provable security...

Would you be willing to modify you project's website?

Unknown said...

I can see how people would take this too strongly. We've changed cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 text.

It's really hard to explain to people what proof gives you. It gives you pretty much 100% what you proved, but what you proved always has assumptions, and for security this is where you would attack (as you point out).

That doesn't mean cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 proof didn't buy you anything, it just means you have closed many, but not all attack vectors.

Joanna Rutkowska said...

@Gerwin:

That's really cool you changed cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 text on cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365 website, thanks!

cmlh said...

@Gerwin

I would be having a word to NICTA PR as cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365y are promoting this as "Sel4 will ensure operating systems are foolproof" i.e. http://www.cá cược thể thao bet365_cách nạp tiền vào bet365_ đăng ký bet365australian.com.au/australian-it/nicta-could-make-billions-with-new-tool/story-e6frganf-1225760721546