6 ms·
The other thing I wonder about is that in 2040, will we be still worrying about buffer overflows?
by architgupta 14y ago
The other thing I wonder about is that in 2040, will we be still worrying about buffer overflows?
- tptacek 14y agoI really doubt that we'll be using programming environments where memory corruption is possible in 2040.
- adrusi 14y agosomeone's gotta write the kernels though, I can't think of any way to write kernels or compilers where memory corruption is impossible.
- sixcorners 14y agoDidn't Microsoft make an experimental kernel with managed code?
- reginaldo 14y agoIndeed. It is the Singularity Research OS. Links: http://en.wikipedia.org/wiki/Singularity_(operating_system) http://en.wikipedia.org/wiki/Singularity_(operating_system) http://research.microsoft.com/en-us/projects/singularity/ http://research.microsoft.com/en-us/projects/singularity/
- zobzu 14y agoNote that managed code is just one feature of Singularity. They have many other important concepts (like SIPs). Plan9 ain't bad either. There's also different C# clones (that aren't based on Singularity)
- zurn 14y agoI wonder if SIPs are new or did eg the various Java OSes or the Burroughs ALGOL based system do something similar?
- jstclair 14y agoIIRC, though you write in a managed language, it's jitted at install time so it doesn't run under a managed runtime.
- Arelius 14y agoIn 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 you will always be able to gain access.
- gvb 14y agoThe 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_research_and_development 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 http://en.wikipedia.org/wiki/Turtles_all_the_way_down
- sanxiyn 14y agoWell, 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.
- gvb 14y agoI 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 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.
- ktosiek 14y agoYou 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 :-)
- marshray 14y agoC can represent the type "array of 10 ints": int array[10]; But probably you meant runtime variable values.
- jackpirate 14y agothe type of that is an (int*) if I'm not mistaking
- marshray 14y agoThere's an automatic conversion to int* when necessary, but the array is nominally a distinct type. This is particularly apparent in C++ where you can do things like instantiate a template from the array type and create a compile-time function to return the number of elements.
- ktosiek 14y agoWell, here the compiler won't help you with bounded access - you can easily read array[42], and it would compile (and maybe even work... but just a little bit funny ;-)). 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.
- fusiongyro 14y ago
- jerf 14y agoYou 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 up, could do something like memory corruption, it will be made as small as possible, verified as rigorously as possible, and get the tar beaten out of it until it's as safe as humanly possible. This will not be a security paradise, because there's plenty of other ways to screw up. Even if we magick a perfect capabilities-based system into existence in 2040, with every desirable property that is promised fully manifested, programmers will still fail to correctly use it, because security is profoundly a Hard Problem. But the same freaking buffer exploit for the ten millionth time should be a thing of the past. (Library support should also be well on its way to making cross-site scripting a thing of the past, too.)
- tptacek 14y agoI 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.
- jerf 14y agoI 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.
- wvyar 14y agoI'm personally unfamiliar with the languages you mention in the first paragraph. Would you mind linking to some information about them?
- xyome 14y agoHere's a paper describing how to escape from a VM using memory errors. They're causing memory errors by putting a lit light bulb close to the memory chips: http://sip.cs.princeton.edu/pub/memerr.pdf http://sip.cs.princeton.edu/pub/memerr.pdf Neat hack :)
- rheide 14y agoThis was a fascinating read. Thanks.