Linux, IRIX, and "POSIX Capabilities"

[Bill Frantz]

At 01:50 PM 11/7/1999 -0800, Ka-Ping Yee wrote:
>At one
>point during his talk he mentioned that there exists an A1-level
>(mathematically-proven) operating system out there, which surprised
>me because i thought that EROS was the only one; he cited SCOMP.

As far as I know, SCOMP is the only A1 system.  SCOMP is a Honeywell
minicomputer OS.

KeyKOS, with some unwritten user mode code, had the requirements for a B3
(which are the same functional requirements as A1), but failed on the
assurance (how sure are we that the code actually implements the specs).
They didn't really approve of systems written in assembler.

Since that user mode code has never been written, neither KeyKOS or EROS
can pass B3 or A1 (or almost any level for that matter).  This is good as
it keeps them from being subject to export restrictions.