Windows 2000 declared secure

[Pete Chown]

Adam Shostack wrote:

> I don't think that Linux would pass EAL4; as
> you've pointed out, that requires a documented and followed QA
> process.

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?

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 majordomo at wasabisystems.com