Provable Security: How feasible is it?

Select |




Print


Klein, Gerwin; Murray, Toby; Gammie, Peter; Sewell, Thomas; Winwood, Simon

Klein, Gerwin; Murray, Toby; Gammie, Peter; Sewell, Thomas; Winwood, Simon


2011-05-09


Conference Material


13th Workshop on Hot Topics in Operating Systems


Napa, USA


5


Strong, machine-checked security proofs of operating systems have been in the too hard basket long enough. They will still be too hard for the humongous mainstream operating systems, but even for systems designed from the ground up for security they have been counted as infeasible. There are high-level formal models, nice security properties, ways of architecting and engineering secure systems, but no implementation level proofs yet, not even with the recent formal verification of the seL4 microkernel. This needs to change.


USENIX


security, proof, seL4


http://www.usenix.org/event/hotos11/


nicta:4631


Klein, Gerwin; Murray, Toby; Gammie, Peter; Sewell, Thomas; Winwood, Simon. Provable Security: How feasible is it?. In: 13th Workshop on Hot Topics in Operating Systems; Napa, USA. USENIX; 2011-05-09. 5.



Loading citation data...

Citation counts
(Requires subscription to view)