Formal security models are a superset of informal ones... not the other way as many people think. This is why users like rcgreen and chsh that have no experience with formal models simply do not understand them. The idea of something beyond their own knowledge set puts them on the defensive. Close mindedness is an unfortunate thing...

I have never heard anyone ever who was familiar with formal security models and systems based on them that didn't feel they were significantly better. Seriously... how many PhDs can you find how are Information Security experts that feel informal security models are better? Or even comparable.

If you think about security as a process... an informal solution is a generic answer.

"What system can do X?" "System Y seems popular, so it'll prolly do what we need."

"What system can do X?" "First we must define X to quantify all of specific requirements: X(1,2,3...), now we have a requirement. System Y must have matching charactoristics for every X. If Y(1,2,3...) == X(1,2,3...) then Y is verified... for every exception Z, Y must be modified or supplemented until Z is an empty set."

Do you notice the difference? Of course people who do not understand the quantification of requirements and the verification of their solutions will think this is a silly, wasteful process.

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.
Ada2005 is now out... you can pick up a free copy of GNAT with 2005 support at adacore.com

cheers,

catch