Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

A Tale of Two Pwnies (Part 1)

blog.chromium.org

Post reply on HN
Print view View original

51–60 of 82 posts

Re: A Tale of Two Pwnies (Part 1)

#51

Post by gvb »

Arelius wrote: post #18
adrusi wrote: post #11

Earlier quoted context omitted.

someone's gotta write the kernels though, I can't think of any way to write kernels or compilers where memory corruption is impossible.

In theory, it's possible to use a formally verified approach to ensure this can't happen, and there is a lot of research into that. There is a version of the L4 microkernel that has been formally verified which should prevent memory corruption in kernel space, but I don't know the exact details. This of course won't prevent corruption due to physical sources, such as radiation, but with physical access to a machine y…

The L4 microkernel was verified that it faithfully implemented the system specification. The system specification is written in (executable) Haskell. http://en.wikipedia.org/wiki/L4_microkernel_family#Current_r... So, how do they know the Haskell specification is correct???

I guess it's turtles all the way down. http://en.wikipedia.org/wiki/Turtles_all_the_way_down

Re: A Tale of Two Pwnies (Part 1)

#52

Post by comex »

Arelius wrote: post #18
adrusi wrote: post #11

Earlier quoted context omitted.

someone's gotta write the kernels though, I can't think of any way to write kernels or compilers where memory corruption is impossible.

In theory, it's possible to use a formally verified approach to ensure this can't happen, and there is a lot of research into that. There is a version of the L4 microkernel that has been formally verified which should prevent memory corruption in kernel space, but I don't know the exact details. This of course won't prevent corruption due to physical sources, such as radiation, but with physical access to a machine y…

The first thing about L4.verified is that formal verification, while admirable, doesn't really matter, at least not in a world where exploits are commodities, exploitation a continuous process: if a program is only a few thousand lines long and written with attention to security, the number of vulnerabilities can at worst be counted on one hand, and attackers will find them all for you in short order. If you're Iran and have an attacker capable of pouring millions of dollars into a single hack, it might make a difference; if you're Microsoft, not so much.

The second thing is that while a microkernel (if used with an IOMMU to prevent a malicious driver from DMAing all over your code) appealingly prevents an attacker from exploiting a malloc overflow in some random network driver and immediately gaining full access to anything (the current state of kernel security!-- but performance is key), it doesn't prevent an attacker from using that network driver pwn to hijack the user's Facebook session; full access is appealing, but in a complex system there are many, many "lesser targets" that are just as bad from a user's point of view.

Microkernels and their little cousin sandboxing can help, but the resulting trusted computing base is still much, much larger than we can formally verify in the foreseeable future.

(A sibling of this comment mentioned Singularity, but that's a fairly different beast: instead of proving that fast code is safe, you try to make obviously (memory) safe code fast. The only reason Singularity is able to make interesting performance claims is that it uses verification to completely avoid system calls: pretty cool, but a NaCl-like kernel could do something fairly similar for C; it doesn't really change the correctness/performance tradeoff.)

Re: A Tale of Two Pwnies (Part 1)

#53

Post by marshray »

tptacek wrote: post #43
moldbug wrote: post #40

Earlier quoted context omitted.

Pinkie Pie is a frickin' genius. But I'm curious about this equation, interesting == effective == intricate. Intricate == complex, right? So, the exploit certainly reveals that Chrome's security model is complex . And this is supposed to be a good thing? Seems like a good thing, if you're Pinkie Pie...

That's not an equation. I don't know the right word to use for Chrome's model yet, but unlike some people, I am very bullish on sandboxing.

I too am bullish on sandboxing, but I suspect, like all security boundaries that have come before it, that it will be secure in inverse proportion to the amount of functionality that is allowed to pass through it. App developers will poke more and more holes through the sandbox to enable new ways to cater to users. E.g. the WebGL^H^H^H^H^HGPU command buffers channel leveraged by PinkiePie.

Re: A Tale of Two Pwnies (Part 1)

#54

Post by marshray »

ktosiek wrote: post #28
adrusi wrote: post #11

Earlier quoted context omitted.

someone's gotta write the kernels though, I can't think of any way to write kernels or compilers where memory corruption is impossible.

You can use a language with dependent types (types depending on values, so you can have arrays of type "array of 10 ints" etc.) - it adds some type-level work, but makes a lot of mistakes not even compile. But complicated type systems are, unfortunately, rarely used in languages suitable for system programming. I only know about ATS in this group actually :-)

C can represent the type "array of 10 ints":

     int array[10];
But probably you meant runtime variable values.

Re: A Tale of Two Pwnies (Part 1)

#55

Post by saurik »

skeletonjelly wrote: post #47
wtracy wrote: post #35

Earlier quoted context omitted.

What's the problem if they run out of bugs to find? Would that not imply that there are no exploits left to be made?

Because if they get bored, they'll find other things to exploit/break. It's in their nature.

Then, by definition, you would not have run out of bugs.

Re: A Tale of Two Pwnies (Part 1)

#56

Post by jerf »

wvyar wrote: post #45
jerf wrote: post #30

Earlier quoted context omitted.

You don't write them in C. You write them in a not-yet-existing language that allows low-level, but safe, access. (Prototypes of this language certainly already exist, I'm not convinced any are ready for this level of prime time.) You probably also have some additional hardware support not yet existing. And while, yes, deep at the heart of the system there will be something or some set of somethings that, if screwed…

I'm personally unfamiliar with the languages you mention in the first paragraph. Would you mind linking to some information about them?

There's a whole range of passes being made at this. I think the last ten years have been about the interpreted "scripting" languages and it's become obvious the next major PL niche is one of these safer-yet-systems-level languages, so in addition to the ongoing research it seems to me like there's been a burst of work on these, with more to come. D is among the most mature, and the least revolutionary, with all that entails. Mozilla is doing Rust. Go arguably fits into this area, though I'm not sure it's quite meant for kernels per se. (It is a systems level language, though.)

But given that 2040 was the year tossed in, I was also thinking the next generation after that, where some of the next-next generation of verification would be folded in. There you're looking at Haskell as being the gateway into that world (even though it is not really that verifiable in the strongest sense itself, it gets your foot in the door), and the Coq and Agda and the slowly-but-surely increasingly usable proof assistants, which would be useful for a provable-not-corruptable (via normal software means) software kernel.

Though... if one looks at the rate of advance in kernels over the past 30 years and then project out to the next 30, we get a distressingly high probability of it still being in C. Still, I cautiously optimistically (or pessimistically, depending) think that the hardware revolution that we are still only at the beginning of as we run out of Moore's Law is going to produce non-C languages that will eventually be irresistible to produce kernels in. There's going to be ever more constraints we want to maintain and it's going to get harder and harder to maintain them without some sort of language support beyond what C can supply.

Re: A Tale of Two Pwnies (Part 1)

#57

Post by Arelius »

comex wrote: post #52
Arelius wrote: post #18

Earlier quoted context omitted.

In theory, it's possible to use a formally verified approach to ensure this can't happen, and there is a lot of research into that. There is a version of the L4 microkernel that has been formally verified which should prevent memory corruption in kernel space, but I don't know the exact details. This of course won't prevent corruption due to physical sources, such as radiation, but with physical access to a machine y…

The first thing about L4.verified is that formal verification, while admirable, doesn't really matter , at least not in a world where exploits are commodities, exploitation a continuous process: if a program is only a few thousand lines long and written with attention to security, the number of vulnerabilities can at worst be counted on one hand, and attackers will find them all for you in short order. If you're Iran…

You have many strong and valid points, But I think it's possible to engineer a world where "Memory corruption related exploits" cease to exit. There are many high-level programming techniques that can be used to prevent those, and I was making a point that we can fix the low-level ones also, most likely formal verification is not the way there, but it does exist as a possibility.

That is a very far cry from saying we can live in a world with perfect security, which I think is the point you are trying to make.

Re: A Tale of Two Pwnies (Part 1)

#58

Post by jerf »

tptacek wrote: post #38
jerf wrote: post #30

Earlier quoted context omitted.

You don't write them in C. You write them in a not-yet-existing language that allows low-level, but safe, access. (Prototypes of this language certainly already exist, I'm not convinced any are ready for this level of prime time.) You probably also have some additional hardware support not yet existing. And while, yes, deep at the heart of the system there will be something or some set of somethings that, if screwed…

I definitely don't think that eliminating memory corruption vulnerabilities will produce security shangri-la. Most of the vulnerabilities we find every day aren't memory corruption.

I certainly didn't mean to imply that you had that belief by any means. My world (much smaller than yours, of course) is utterly dominated by the cross-X/injection complex of security vulnerabilities (cross-site scripting, SQL injection, shell command injection, all the same thing in the end really). I've also lost track of the times I've encountered the moral equivalents of "limited admin permitted to make new user accounts is capable of creating a full admin account and controlling its password" or some equally brain-dead simple privilege escalation that doesn't even involve anything "clever". I was just contextualizing.

Re: A Tale of Two Pwnies (Part 1)

#59

Post by wizzard »

Arelius wrote: post #41
wizzard wrote: post #31

Earlier quoted context omitted.

L4 was verified to the tune of about $4.6 million dollars, or $500 per line of code. And that's for a microkernel under 10 KLOC. And that's assuming no changes are made. Ever.

The idea of having a small kernel that is properly verified, and properly run user-level code in a memory-protected manner isn't absurd. And when put into the context of Operating System budgets, 4.6 Million dollars is completely reasonable. Again, we're also talking about a hypothetical 2040 OS. not something we're going to have working tomorrow.

I didn't mean to imply it's not possible, or won't be possible in the future, just that I don't think it's on the immediate horizon for anything but small kernels. 4.6 million dollars may be reasonable, but if you have to add on another million dollars and another month of verification time for every patch release... it's just not practical yet.

Re: A Tale of Two Pwnies (Part 1)

#60

Post by emmelaich »

Natsu wrote: post #12
tptacek wrote: post #4

What's amazing about this bug is that at every step you learn something that makes Pinkie Pie more terrifying while simultaneously making the Chrome security model sound more and more forbidding.

And the worst is yet to come.... --- In an upcoming post, we’ll explain the details of Sergey Glazunov’s exploit, which relied on roughly 10 distinct bugs. While these issues are already fixed in Chrome, some of them impact a much broader array of products from a range of companies. So, we won’t be posting that part until we’re comfortable that all affected products have had an adequate time to push fixes to their us…

I'm looking forward to that one too.

Previous reference on hackernews here: http://news.ycombinator.com/item?id=3682664

Post reply on HN