71–80 of 82 posts
Earlier quoted context omitted.
C can represent the type "array of 10 ints": int array[10]; But probably you meant runtime variable values.
the type of that is an (int*) if I'm not mistaking
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…
"a low level interface to the GPU command buffer" This sounds cool. Is this a standard feature in Chrome?
Earlier quoted context omitted.
There is no way to explain how awesome Pinkie Pie's exploit is without simultaneously explaining how intricate Chrome's security model is. A great way to market a browser is to have a security model so interesting/effective/intricate that any description of a working exploit will also serve as marketing.
I disagree. Marketing does not have to be in every damn blogpost . It's just annoying ;-) While they attempt (and apparently succeed) to make you believe that exploiting Chrome is exceptional and it's such a super high security program: The bottom line is, 2 guys showed up with a complete remote exploit of Chrome. And there are more exploits that are obviously unreleased, and some that will get released each year. Th…
Your contributions, on the other hand, are much more content-free, being mostly value judgements against Chrome's PR or the supposed overconfidence of their programmers. And while you do brush on more technical matters, you do so by name-dropping products rather than being informative and describing the relevant security property.
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 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
So it's not useless.
Earlier quoted context omitted.
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
Well, they don't know whether specification is correct, but verification, while proving correctness, also proved (because you need these to prove correctness) no buffer overflow, no null pointer dereference, no unintentional integer overflow, etc. So it's not useless.
The higher level question is whether the Haskell specification fully and correctly specifies the desired behavior. In my 30-odd years of experience in Mil/Aerospace, I have never seen a fully and correctly specified set of requirements that could be transliterated into correct executable code. If nothing else, they all have had implicit assumptions. That is the Achilles heel of the IBM "Master Programmer" method, reborn as "outsourcing".
Since the specification is executable Haskell, that implies they wrote Haskell test programs to show that the specification implements the desired behavior.
Writing a program to verify the specification that another program implements... and then claiming a formal proof of correctness of the system is now recursive. Turtles all the way down.
Earlier quoted context omitted.
Well, they don't know whether specification is correct, but verification, while proving correctness, also proved (because you need these to prove correctness) no buffer overflow, no null pointer dereference, no unintentional integer overflow, etc. So it's not useless.
I agree that is is not useless, however its usefulness is limited to the implementation level, verifying the translation from the Haskell specification to assembly/C/blub implementation is correct. The higher level question is whether the Haskell specification fully and correctly specifies the desired behavior. In my 30-odd years of experience in Mil/Aerospace, I have never seen a fully and correctly specified set of…
For others: I learned a lot from reading the book "Mechanizing Proof". No knowledge of formal methods is needed (but you will learn something about formal methods while reading). I can't recommend the book highly enough.
http://www.amazon.com/Mechanizing-Proof-Computing-Inside-Tec...
Earlier quoted context omitted.
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.
With dependent types function to get element from array may have type (this is pseudocode): get (array : T[n], index : m) : T {n : nat, m : nat, m < n} which would mean "function get, which takes: n long array of elements of type T, index of type m, where m is smaller than n, and returns T". Type-level naturals and bounded array access are the basic examples of dependent typing, more interesting ones may be red-black trees with guarantees about their shape put in the type or some magic for creating DSLs.
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.
Didn't Microsoft make an experimental kernel with managed code?