"OpenBSD is an ultra-secure, freely available, multi-platform BSD-based UNIX-like operating system. And is arguably the most secure operating system in the world. After using OpenBSD for over 9 years I decided to place online some useful information for first time users of OpenBSD. The information here covers the current release of OpenBSD."
To read all comments associated with this story, please click here.
Member since:2005-08-08
> If the OpenBSD folks really cared about security and correctness, they'd use things like static typechecking and runtime boundschecking to ensure that they eliminate all buffer overflows -- or other methods that you can prove will eliminate those classes of errors.
First, they are doing runtime bounds checking (totally on the heap; partially on the stack).
Second, they are using static checking tools, too (they even developed some themselves !)
Third, static type checking does not prove anything anyway; it can detect errors but it will not prove a program does not contain errors. Indeed, there are methods to prove programs but it is a very lenghty (if ever doable) process on huge codebases such as OpenBSD's.
Fourth, nothing will ever replace careful code reviews by human developers.
Fifth, it is a real-world project; not a university playground project.
Sixth, they probably have more experience in designing and maintaining secure software than you have, so they know better what suits their needs.
Member since:"First, they are doing runtime bounds checking (totally on the heap; partially on the stack). "
That's better than nothing. But much better would be writing critical programs that mustn't have buffer overflows in a language that can be statically typechecked (and running with a runtime to make sure that array indexing errors don't happen). You can get that any number of ways (e.g. use ML), but using "C" (even with ad hoc checks) is not as complete.
Although static type checking doesn't fix everything, given that half of all security problems are due to buffer overflows, static type checking (or even dynamic) eliminates half of them, once and for all. If your goal is to critical systems correct (not just typesafe), you'll probably be using a notation (language) different from "C" -- you'll want something that works better with your automated proof technology. This has been done already, for cryptographic protocols. But again, that's not what OpenBSD folks want -- they just want to hack "C", as best as they can.
Your bit about it being a "real world" project is specious -- that's the same "logic" that MSFT uses: although OpenBSD does some critical things better than MSFT, because it is a marginal project (not quite a "university playground project" -- but close) it is acceptable to ignore what it does better than Windows.
My original point is that although OpenBSD says security is their primary goal, that's clearly not the case. If that was their only goal, their methods would be more attuned to the problem.
Member since:
It seems the OpenBSD programmers want the most security they can get using traditional techniques (e.g. "C").
If the OpenBSD folks really cared about security and correctness, they'd use things like static typechecking and runtime boundschecking to ensure that they eliminate all buffer overflows -- or other methods that you can prove will eliminate those classes of errors.
They won't do this. I think this is the sort of thing that leads to them being called "close-minded".
Unfortunatley, OS folks (Olin Shivers excepted) tend to be disinclined to such methods.
The oddest are folks like Dawson Engler, who used very lispy techniques (run-time code generation), but in "C", in his exokernel. This got done away with -- the extra speed wasn't worth it, and non-ninjas couldn't maintain it.