Adam Shostack wrote:
I agree that the Linux kernel probably couldn't pass because of lack of documentation. This is even more true for "GNU/Linux", the loosely defined collection of software that makes up a real Linux system. If wuftpd has a buffer overflow, is that a hole in "GNU/Linux", or a hole in wuftpd? What about the Foo Linux distribution that only comes with proftpd?I don't think that Linux would pass EAL4; as you've pointed out, that requires a documented and followed QA process.
At the same time, I think a specific distribution probably could be evaluated. Red Hat have a well defined QA process for example.
Another problem might be the granularity of access controls. IIRC Unix systems that were evaluated to C2 had to include some kind of ACL system. The user/group/others split wasn't good enough. SELinux would pass this requirement easily, but vanilla Linux systems might have a problem.
On another note, I'd be interested to hear more about how Eros is going to get EAL7. Formal verification of a whole OS sounds horribly difficult, but very exciting if it can be done. One problem I've always had with correctness proofs is that they prove the program to satisfy some statement of the problem. They don't prove that the problem stated is the one you intended to solve. How will you avoid this with your proofs of Eros' security?
As an example of what I mean, here is a statement of what it means for one list to be the concatenation of two others:
concat([], X, X).
concat([H | T], X, [H | U]) :- concat(T, X, U).
In other words, the empty list concatenated with any other list gives that list unchanged. Then, in general, a list X is the concatenation of Y and Z iff: (i) X and Y have the same head, and (ii) the tail of X is the concatenation of the tail of Y with Z.
Unfortunately, not only is this a statement of the problem, it is also a Prolog program which solves the problem. :-) So, it's provably correct, because the solution and the statement of the problem are the same thing. Of course it's provably correct in a rather useless way...
--
Pete
---------------------------------------------------------------------
The Cryptography Mailing List
Unsubscribe by sending "unsubscribe cryptography" to [EMAIL PROTECTED]
