5 ms·
Dick Kemmerer always talks about how he formally verified the UCLA Unix security kernel in the 1970s, together with Bruce Walker and Gerald Popek. See <a href=
by ljosa 17y ago
Dick Kemmerer always talks about how he formally verified the UCLA Unix security kernel in the 1970s, together with Bruce Walker and Gerald Popek. See <a href="http://dx.doi.org/10.1145/358818.358825>their http://dx.doi.org/10.1145/358818.358825>their 1980 paper</a>. How is the new work different?
- Hoff 17y agoMost any product that was aiming for the old NCSC/TCSEC Class A1 security rating would have inherently received the formal verification Class A1 required.
- abecedarius 17y agoI'd be surprised if the 1970s proof was both machine-checked and about the actual code (not an abstraction of it).
- kragen 17y agoUnfortunately it's an ACM paper, so I guess we'll never know.