RE: Re: Trusted OS...

[Rick Smith <rick_smith () securecomputing com>]

At 10:41 AM 03/31/2000 -0800, Starkey, Kyle wrote:
> Todd...
> I am with you on the fact that the TOS certification is a little much for
> the corporate standard, but I can not accept the fact that there is any
> other way to certify that the OS is truly tursted.  The OS and ALL of it
> subcomponents must be broken down and mathematically proven to adhere to the
> security structure that the OS was designed for.  Most of us have no time to
> read through 4000 pages of mathematical proofs, but to be a TOS you must be
> able to provide this document before I will accept that certification.

4000 pages is a good guess. Todd Fine, a colleague, had roughly a dozen 2"
binders that held the LOCK machine-checked proofs, and they only addressed
the TCB interface. They did not include proofs of the underlying
instruction sequences.

As far as I know, there are no "operating systems" in the commercial sense
of a "platform used by unrelated third parties to develop applications"
that have up to date formal proofs consistent with the Orange Book
expectations. There are perhaps a handful of products (like the LOCK guard)
with the canonical bucket of proofs, but I don't know of any that are
really "state of the art."

> Tha being said, a TOS like that would be a PIA to work with in the corporate
> environment and is a little too restrictive for everyday business, but may
> be better suited for the NSA and other such agencies with 3 letter acronyms
> for names.

Not even NSA has much interest in Orange Book-style formal proofs any more,
at least, not for use in "practical" applications.

The most promising thing I've seen is the use of formal proofs to identify
crucial security features of an architecture. We leaned more towards that
as the LOCK effort wound down, and applied such lessons to Sidewinder,
though of course we never came close to doing a formal analysis of it. A
better and more recent example is the way that Jonathan Shapiro analyzed
the EROS security mechanism. It's not a full-interface proof like
traditional Orange Book proofs, so it's smaller, more accessible, and
therefore more convincing in a lot of ways.

Rick.
smith () securecomputing com