Tom 7 Radar:
all comments
[ next 25 ]
It's supposed to be a cool stunt that may yield interesting results, just like the whole AAD thing in the first place.
I mostly agree with the substance of your points, but you offend me with style. Your general tone seems to be that people who are doing real-world stuff are drawing with crayons and should grow up.
I've experimented a little bit with Scheme and Haskell (not SML), so I am not allergic to higher-level languages. Here are a few reasons they may not be in wider use:
1. Performance, disk space, memory usage, etc. I know it's trendy nowadays to suggest that these are no longer concerns, and for us rich kids with new PCs, maybe they're not. But OpenBSD (for example) builds and runs on a lot of older machines that you would consider pretty slow. There's also embedded usage to consider, and small machines -- OpenBSD runs on the Zaurus, a handheld machine too small to fit libraries with debugging symbols -- and there's donated computers in third-world nations, and so on.
True, you can write just your most performance-critical code in C, but that doesn't save you from the disk and RAM requirements.
2. Operating system kernels have to do a lot of low-level stuff. That really calls for a low-level language. There's microkernels, but they're only beginning to get past the research-project stage.
3. These languages are moving targets. C has essentially been the same since 1989, and there's something to be said for that.
Even if the high-level languages are fairly old, like Lisp which has been around half a century, they've only been put to limited real-world use. The best way of doing such-and-such a thing may still be in the process of being hashed out. The libraries and implementations are less mature, in other words.
4. The implementations are big, and OS project leaders may see them as clunky, poorly designed, etc. In particular, OpenBSD has a very high standard for code quality in its base system, and these high-level language implementations, being relatively immature, may have hackish parts to them. There may also be licensing issues, since a lot of language implementations are unfortunately under the GPL/LGPL or worse. (Not SBCL, GHC, MLton, SML/NJ, or TILT, though.)
It's worth pointing out that not too long ago, OpenBSD rewrote their package management tools in Perl, partly to avoid having to worry about buffer overflows. I'm not saying Perl was the best choice, but there you go. I've also noticed you wrote Escape in C++; why is that?
By the way, why can't you run your compiler through your proof checker? I can understand the issues with proving correct the runtime system or the proof checker itself, but the compiler? There shouldn't be any problem checking that.
|
| |
|
|
| |
I want to keep this above the belt, but I feel the need to respond to these unfair remarks:
"... please look up 'argument from authority.'" I mentioned my credentials only in response to your accusation that I am "commenting on something [I] know nothing about." It's simply not true that I am ignorant. This is not argument by authority, because I never claim that my arguments follow from my expertise, just that they are informed by it.
Second, you are misrepresenting my remarks. I never said that there exists a more secure operating system today than OpenBSD. I never said OpenBSD is a waste of time. You seem to inrepret my remarks as insisting that people should drop what they're doing and switch to a magical solution that is not yet available outside of research communities. How could I insist that? I'm running linux this very second. But I do think it makes sense to own up to problems with the way we build software, and be open to new techniques for solving them.
So, let me say again what I am actually claiming. I'll number them so that if you'd like to say I'm saying something, you can just point to the number and respond.
1. Even if OpenBSD is the most secure practical operating system available, it is not secure. I am completely confident that there will continue to be security patches for your installation of the OS over the next year.
2. Observe that these bugs resulted (as far as I know) from accidental mistakes. Therefore, code review does not catch all accidental mistakes.
3. This contest reminds us that it's easy to maliciously embed bugs. Anything we can do by accident we can do on purpose, and I'm assuming that maliciously hidden bugs are harder to find than accidental ones, which I hope is not controversial. So if this is true, code review finds even fewer maliciously hidden bugs than accidental ones.
4. Formal techniques are superior because the intention of the coder is irrelevant, and the attention of the reviewer is unlimited. Whether he makes a mistake or deliberately tries to hide devious behavior, the proof-checking problem is just as easy. Computers are supremely patient, and thus can do a much more thorough job, much more often, than people.
5. Because the codebase is getting larger, and the contributors more diverse, we can expect more accidental bugs and more malicious bugs. So, not only are current techniques unable to find all bugs, the problem is getting harder. We need new techniques!
This is all I was saying in my original post. Some things have come up since then that I'd like to clarify my position on.
A. I stick by my statement that the countermeasures that we listed make it "more difficult (but seldom impossible) to exploit the bug." (Note this doesn't imply that it never makes them impossible, as you seem to claim I was saying (?)) Techniques based on randomization are not impossible to exploit (StackGuard, ProPolice, randomized malloc/mmap), nor do they address all kinds of bugs. W^X (and the analogous part of PaX) does absolutely protect against code injection, which is great, but not against returning to parts of code that already exist and might implement the malicious behavior for you. You know this, naturally; people on bugtraq have demonstrated attacks and the documentation for the software admits to the fact that the protection is not perfect.
B. Even though they are not perfect, the existence of these countermeasures does increase security. I hope that vendors of all operating systems start turning them on by default, the speed penalty be damned.
C. Nonetheless, I think the focus looking to the future is wrong. By accepting that some programs have almost completely unpredictable behavior under bug conditions (ie., most C/C++ programs, ie., most BSD/Linux/Windows programs) and then attempting to limit the damage that can be caused by that wild behavior, we're giving ourselves a much harder security problem than we need. Instead, I maintain that we should use formal techniques to guarantee that such "undefined behavior" can't arise in the first place. The great thing about these techniques is that the protection is automatic and absolute (up to bugs in the implementation of the proof checker or compiler, which are limited to a single source rather than every application, and which C/C++ programmers already have to live with anyway).
D. Some formal techniques, like static typing, are available today in practical form for many applications. If you want to write applications that can't have buffer overflows, integer overflows, heap corruption, double-free, format-string vulnerabilities, etc., are easier to write (and review) than their C counterparts, and have very competitive performance, you can download an SML or O'caml compiler today and go for it. I write almost all my software in SML, and it's perfectly practical for real applications today. It doesn't give you a proof of correctness, but it does give you a guarantee of memory safety. That's enough to exclude with certainty a large class of security problems that we have to patch our BSDs and Linuxes several times a year for. It also addresses other problems of large software programming (like debugging and blame assignment); it's really a win on many fronts.
I can't predict when we'll have practical tools for writing applications and proving them correct. There are lots of people working on it. I'm even less optimistic for near-term mainstream acceptance. One of the reasons is that communities like OpenBSD's are very closed to the possibility of using new languages. ML is over 30 years old; just in the last decade have we seen some small fraction of the ideas there make it into mainstream languages like Java. (PS. I don't think Java is a good language or representative of what I'm arguing for.) I wish I knew how to reach slashdot kind of folks with these languages, because I genuinely believe that they would be appealing to exactly the same kind of person who chooses Linux or BSD because they are better than Windows, despite being less popular. Unfortunately from my perspective there is a kind of Zeitgeist that it is better to suffer through writing painfully low-level C code, carefully avoiding its many dangers--that somehow through suffering one produces a better product. I think that the OpenBSD folks are especially guilty of this. Suffering is not virtuous. We have better ways already--especially if security is your #1 goal--and your original post is a good example of the kind of allergic reaction that many people from the "hacker" community have when faced with languages more modern than C. I don't really understand this, and I wish I did. Perhaps you have some insight. Academics absolutely do have the responsibility to make their work accessible, but "real world" programmers also have the responsibility to then try that stuff out and make concrete criticisms--or at least not demand to see futuristic stuff if they have not yet looked at stuff that's 10 or 20 years old. The mainstream should not flow only one way.
As for your challenge, I'm not really sure I understand the point. I'm not saying that writing correct code and proving it is fast, so the 1-day time limit seems undue. I also think the cost of errors in sound synthesis isn't very high, so the challenge of proving it correct also seems undue. But I will say that if I were to write some procedural music software (which is actually high on my list, so it may happen) today I would definitely use SML. Can you explain what it's supposed to demonstrate, or propose an alternate challenge?
|
| |
To "make a lot of attacks impossible" is precisely to make it more difficult, but not impossible, to exploit a bug. It is impossible to exploit a bug if and only if all attacks based on it are made impossible. |
| |
Sorry, if that message sounded dismissive it wasn't at all intentional. =) I appreciate all bug reports! Thanks! |
| |
4467. sylvia (194.42.43.134) –
21 Apr 2006 08:51:00
[ B & S? ]
It goes on Portugal tv, all twesdays,6 p.m. In my childwood..it was the best cartoons of ever...it always made me cry....
Congratulations to who did that story...it should exist some more cartoons at the same type...not wars...only happy storyes...
|
| |
4466. Anonymous (194.42.43.134) –
21 Apr 2006 08:44:49
[ B & S? ]
I found it to buy on a site named arabian towers...but i guess they only have it in their own language not in english...It was about 56€....
|
| |
My mistake 32bit color is not more colors in RGB. And yes I see what you mean. I guess I did not this this all the way through. |
| |
I eagerly await Tom7BSD, where all the code is proved to be correct.
No, I'm sure your work has value, but for the time being, I don't see anyone using it to write operating systems. And you say you have "damning" evidence against OpenBSD as though you've exposed them as a bunch of frauds. Show me the more secure OS that I can use today. If you can't do that, don't try and sink their work and say it's a waste of time.
In theory, your way might be better once it gets out of the research phase, but that's just speculation, isn't it? In practice, the bad code in your examples would be easily spotted.
You said some stuff that's downright silly. For example: "...protections... make it more difficult (but seldom impossible) to exploit the bug." That's simply not true; they do make a lot of attacks impossible. Then you say "the OpenBSD methodology of code scrutiny simply doesn't work" based on "security patches... for BSD (and Linux, etc.)". The other BSD projects and Linux etc. are obviously not using the OpenBSD methodology. My one-year-old release of OpenBSD (3.7) has in fact only had eight security patches, which is not that much. You're not being realistic with your criticisms.
Finally, regarding your mentions of PhD work, following Bugtraq, etc., please look up "argument from authority." (Spoiler: It's fallacious.) I don't think proof-carrying code is worthless -- I would lose that argument. But that doesn't make your attacks on OpenBSD any less ridiculous.
So how near term do you expect this proof stuff to enter the mainstream? 5 years? 20 years? When hell freezes over?
Say, here's a challenge for you. Make an AAD using sound synthesis software written and proven correct in the same day. Can you do it? I've been thinking of trying the same, except without the proof part.
|
| |
They're coming out of the woodwork! I suspect Google is involved here...
Seriously though, I think we can agree that the current state-of-the-art in developing exploit-free code involves some kind of combination of the following:
1.) Code Reviews
2.) Testing
3.) Static Analysis Tools
Each one of these has its drawbacks. Code reviews certainly can find exploits, but their primary drawback is that they don't scale very well. The result is that they are used on large software projects, but will only cover a small percentage of the actual code-base (when doing formal code reviews) or don't usually cover it very thouroughly (in more ad-hoc style code reviews).
The point is that even now code reviews must be combined with other techniques. The patchwork of different techniques can lead to relatively well performing software, depending on how well they are each done. I think OpenBSD does a relatively good job because they've tried to focus their attention on security. But this is certainly is not an ideal solution.
I eagerly await proof carrying code and provably correct software. For now, we can just use what seems to work best. |
| |
dc-dc: Sure, I know about all of that stuff. What makes you think I don't? But they are just last resorts for handling broken C code. By that I mean, in the case that a C program goes wrong, protections like StackGuard or PAX or whatever just make it more difficult (but seldom impossible) to exploit the bug. Fine, that does add some security in practice, but it's not nearly as secure as writing correct code in the first place. Moreover, they do nothing to protect against maliciously concealed backdoors except to modestly limit the variety of techniques that can be concealed. I claim the OpenBSD methodology of code scrutiny simply doesn't work--this is easily seen by the number of security patches that continue to be released for BSD (and Linux, etc.) and BSD software like openssh. I know, I subscribe to bugtraq, and I have been rooted on an up-to-date system running minimal services.
I don't know if you're actually interested in having a dialogue about this, or if you're just spitting venom, but my criticism is in fact based on knowledge and study of the problem. I'm studying for my PhD in Computer Science on a related problem, even. If you'd like to respond to my actual points, perhaps by explaining why you think Proof Carrying Code is an inappropriate solution, or how code scrutiny can scale to larger and larger programs despite its apparent failings on current code, I am listening. I promise a level-headed reply. Honestly, my guess is that you don't actually know what PCC is about, but I wouldn't criticize you for that as it is more a failing of the academic community for not making these ideas accessible to the mainstream. Still, if my guess is right, you do yourself a disservice by being so dismissive of it. Mathematics is nothing but clear thought, and clear thought is precisely what is required for the analysis of complex programs. |
| |
Yuck!! I was in the bathroom washing my face when I looked down and saw a mushroom growing from the base of the toliet. I freaked out and made my husband come see it!! I am really suprised at how fast it showed up, because I just cleaned the bathroom a few days ago. And when I cleaned the bathroom I made sure that I cleaned under the toilet and around the base. I just can't believe that it popped up so fast. My husband took a picture and then cleaned it up, I refused to touch it. The mushroom released a black fine dust around the base, so I am guessing we will probably see more in the future. I have never ever heard of such a thing!! If it continues I will be calling the company we rent from and have them fix it. |
| |
Your slander against OpenBSD is quite ridiculous. I might skim these code entries and think they were okay, if rather poorly written, but they would hardly hold up to "substantial scrutiny." Furthermore, auditing is not at all the only thing OpenBSD does. Have you not heard of W^X, ProPolice, or the recent randomized mmap()/malloc() work? Why are you commenting on something you know nothing about?
My advice is, go back and stick to your proof toys. Whatever floats your boat. But spitting on people who provide real security -- which you have demonstrated your ignorance of -- will only make you look like a joke. |
| |
4459. dsidnsudbwu (cpe0010b5780bbc-cm000e5c701b5a.cpe.net.cable.rogers.com) –
19 Apr 2006 16:22:49
[ Space Names! ]
gbrrf |
| |
4458. Anonymous (nott-cache-5.server.ntli.net) –
19 Apr 2006 14:00:41
[ FLAMING TEXT ]
BATTY BOI
|
| |
4457. RIGBY (nott-cache-5.server.ntli.net) –
19 Apr 2006 14:00:16
[ FLAMING TEXT ]
IT GD BUT THE HTML CODES SOME OF DEM DONT WORK BUT A GD WEB SYT!!!
|
| |
> Was the Scrambled-Hackz thing by Brian Whitman? Just a guess.
No. That guy looks pretty cool, though. |
| |
max: ok, so it is a simple idea, but a very good one. |
| |
Was the Scrambled-Hackz thing by Brian Whitman? Just a guess. |
| |
jcreed: http://www.linuxdevices.com/articles/AT9665830722.html
Tom can attest to the fact that this is almost exactly the same design as my invention!! |
| |
> Often when I have a good idea it is in fact the case that it has already been invented.
Yeah - something like that happened to me just a couple hours ago. One day several years ago at Aladins you asked if there was some computer vision technique that could be adapted to make a good cubase (or whatever) plugin and I was like "apply Bill Freeman's VISTA to make one thing sound like some other thing", and today i saw a Wired article for something called "sCrAmBlEd?HaCkZ!" which is sort of the same idea. Except VISTA is still much cooler than S.C. because it forces the adjacent sound clips to blend naturally together using a markov random field, in addition to just sounding like the original. Hopefully it would sound a lot more like the source database. |
| |
|
|
| |
Is there something more to what "electronic sheet music" that I should know about? Alls I'm picturing is, like, Finale or something. |
| |
4449. Tom 7 (pool-70-17-170-4.pitt.east.verizon.net) –
18 Apr 2006 20:05:23
[ UPD: Escape Beta 3 ]
It might be counterintuitive, but it's not really that unusual. Programs usually perform better in 32-bit color mode, the reason being that 32-bit computers are most efficient at manipulating 32-bit values. In fact, despite what the number of colors says, 32 bit graphics is usually the same as 24-bit with an extra eight bits tucked in and wasted, just to make each pixel the same as the word size of the machine. And actually, there's pretty much no reason for a modern computer to use anything other than 32-bit color, so I don't even really know why it's an option any more. |
| |
Yeah my inventions keep getting invented too. See: two-door mailbox, electronic sheet music, etc. |
| |
[ next 25 ]
|