On the topic of operating systems and their security.
Computer security obviously falls under math, which means it's something that can be measured and counted. Just like with Boolean, it's a yes or no, quid pro quo, 1 or 0, a logical true a logical false. So I presume this can or will spill over to almost every branch of computer security. A problem with it meshing with an existing infrastructure doesn't make it any less true.

However, as horse pointed out, he must pick and choose his implementations or it's gonna cost money and send his ass packing or sharing an office with the interns. This man exercises authority over 1000's servers each day. horse will point out where I commit folly.

Example from the Dev-proof PDF. It discusses how to develop and prove a multi-level security policy. The SNet system to be exact.

sum(x, y) = x + y;
c = sum(a, b);


A set S of subjects
A set D of data
A set M of messages
A set E of events
A partially ordered set H of histories
A partially ordered set L of levels
A mapping Trusted: S + Boolean
A mapping Subjectlevel: S x H + L
A mapping Maxlevel: S + L
A mapping Messagelevel: M + L
A mapping Destination: M += S
A mapping Data: M + D
A mapping Sender: M + S
A mapping Newhistory: H X E + H

"Verification of computer programs and systems is a difficult problem. This is mainly because most common programming languages are designed from an operational, rather than a mathematical semantics."

I guess this is one of the reasons why catch was suggesting ADA, which has been revised to ADA95 and has incorporated numerical programming into the mix. It was the consensus of the mathematical foundations group at the Verification Workshop (1985). Where you'll find Norman H. Cohen talking about ADA in the ACM. catch will defiantly point out where I commit folly, but I'm pretty sure that's what he was talking about.

Also in the dev-proof paper it mentions that a multilevel secure local area network is under development at Boeing Aerospace Corporation. Couldn't find a paper for that one, but while searching I ran into the High Assurance Multilevel Services For Off-The-Shelf Workstation Applications pdf by: Naval Postgraduate School / James P. Anderson James P. Anderson Co. I figured if it shot off the James P. Anderson John Hancock it was good to go, I wasn't disappointed. You might find some of it redundant though if you have read the "Approach to Identification of Minimum TCB Requirements for Various Threat/Risk Environments".


Just a reminder of the topic:
This list of papers was initially distributed on CD-ROM at NISSC '98. These papers are unpublished, seminal works in computer security. They are papers every serious student of computer security should read. They are not easy to find. The goal of this collection is to make them widely available. This list was compiled by the Computer Security Laboratory of the Computer Science Department at the University of California, Davis. See Acknowledgements.

RC,

One question, how the hell can one be "over educated" on a subject? Humans by nature are educated every day whether you like it or not..........the hunter gather stage.