undefined | Better HN

0 pointsnl10y ago0 comments

0 comments

3 comments · 2 top-level

munin10y ago· 1 in thread

that's a proof that the system corresponds to a specification though

That's right: a formal specification, formal security model, and proof the spec implements it. An implementation formally proven to implement that spec will then posses the security property unless done in by stuff not covered by that model.

Which is where EAL6/7's other assurance activities come in.

nickpsecurity10y ago

One of the best in the field. :) Although I think they just have dev assurance. Not total high assurance. An early one with total was GEMSOS by Schell, one of INFOSEC's founders:

http://www.iwia.org/2005/Schell2005.PDF

Smartcard OS by Karger, another founder of INFOSEC:

https://www.acsac.org/2012/workshops/law/pdf/Lessons.pdf

A comparable one for dev assurance, but maybe easier to emulate, was CompCert. Testing of it against many other compilers validated formal verification gave best reliability.

http://gallium.inria.fr/~xleroy/talks/compcert-lctes08.pdf

Ironically, Microsoft compete neck-to-neck with seL4 in terms of verification with their excellent work on VerveOS:

https://people.csail.mit.edu/jeanyang/papers/pldi117-yang.pd...

j / k navigate · click thread line to collapse