Re: Cons and Security Validation

[Pavel Kankovsky <peak () ARGO TROJA MFF CUNI CZ>]

On Tue, 6 Feb 2001, Crispin Cowan wrote:

> Proving the "nothing else" part is astonishingly difficult.  The academic
> community basically failed completely on that one, and punted to the BS in

There are some mathematical ways of defining security (e.g. non-
interference by Goguen and Meseguer) and deciding whether a given program
is secure. Unfortunately, those methods are still quite infeasible for
anything more complicated than a tiny system described by a few lines
of some process algebra.

> the Orange Book, which is really just a recitation on some motherhood and
> apple pie guidelines for good security design and good software engineering
> implementation.  You can get an A1 secure rating and still be vulnerable.

In fact, there is only a single correspondence (security model <-> formal
top-level specification) that is required to be verified formally in order
to satisfy A1.

--Pavel Kankovsky aka Peak  [ Boycott Microsoft--http://www.vcnet.com/bms ]
"Resistance is futile. Open your source code and prepare for assimilation."