laarcnew | comments | discord | tags | ask | show | place | submitlogin
Design and Verification of Secure Systems (1981) (
5 points by nickpsecurity to dev security papers acm 787 days ago | 1 comment

I talk about separation kernels a lot as being strongest, building block for secure systems. This is paper that invented the concept. The main innovation was separating mechanism from policy. One thing that might surprise programmers is how they want distributed systems to be more like sequential systems for predictability whereas he wanted a sequential/monolithic system to be a distributed system for security. In any case, the separation kernels did well during NSA pentesting (i.e. INTEGRITY-178B), seL4 was verified down to the binary, and Muen was less affected by Meltdown/Spectre IIRC.

Although beware their zealous marketing, I'm posting INTEGRITY-178B link for architectural details and certification data since they're representative of high-assurance security.

Muen Separation Kernel and Hypervisor (used by secunet AG)

If anyone is interested, I'll post some more examples of security and separation kernels later this week.


Welcome | Guidelines | Bookmarklet | Feature Requests | Source | Contact | Twitter | Lists

RSS (stories) | RSS (comments)