Defence in depth [LWN.net]

Defence in depth

Posted Sep 26, 2011 20:23 UTC (Mon) by nevets (subscriber, #11875) [Link]

There ARE totally secure networked multi-user kernels. Here it is: http://ertos.nicta.com.au/research/l4.verified/

From their own FAQ.

Is seL4 proven secure?

No, it is not. The proof states and shows functional correctness, not security. Functional correctness implies the absence of many security common problems, provided the proof assumptions hold (see also the longer version), but it does not mean that the kernel or system as a whole is "secure". Such a statement would first require a precise mathematical definition of what secure means. We are working on proving precisely defined, high-level security properties of seL4 in the future. These proofs will provide stronger assurance than what is possible of current systems, but they will still be up to assumptions and classes of attack vectors.

[bold added by me]

So a secure OS is still not possible. At least no one has done so yet.

Defence in depth

Posted Sep 26, 2011 20:51 UTC (Mon) by smurf (subscriber, #17840) [Link]

Also, from the same FAQ:

Microkernels typically do not provide device drivers, file systems or network stacks.

A secure kernel without storage or networking is somewhat under-featureful to run on machines like kernel.org, I'd say. Have fun formally specifying the operation of your typical high-end network adapter or SATA controller. You'll need it; see you in a few years. ;-)

There's also no formal proof for multi-core systems, arguably also a necessity these days.

Defence in depth

Posted Sep 26, 2011 21:27 UTC (Mon) by dgm (subscriber, #49227) [Link]

> So a secure OS is still not possible. At least no one has done so yet.

I would be more correct to say that, even if someone did a completely "secure" OS, we cannot prove it as we don't know precisely what "secure" means. But this doesn't rule out the existence of a it, just that we cannot be sure.

Defence in depth

Posted Sep 26, 2011 22:15 UTC (Mon) by cmccabe (guest, #60281) [Link]

Well, there is Quebes, which is a little less pie-in-the-sky.

http://qubes-os.org/Home.html

disclaimer: I haven't actually gotten around to trying this "distro."

Probably the most interesting thing they've done so far is sandbox networking code using IOMMU/VT-d.

Defence in depth

Posted Sep 27, 2011 16:18 UTC (Tue) by nix (subscriber, #2304) [Link]

Probably the most interesting thing they've done so far is sandbox networking code using IOMMU/VT-d.

That assumes you have a machine on which this works, and is secure. Even the first is hard (my machines are top-end systems less than two years old and VT-d works on neither of them: on one it just fails to do anything useful and on the other it locks up the system hard on boot unless VT-d is turned off): the second is probably impossible given that huge holes requiring firmware-level changes were still being found in VT-d as recently as a few months ago. Are there any left? Do you feel lucky?

Defence in depth

Posted Sep 27, 2011 20:59 UTC (Tue) by cmccabe (guest, #60281) [Link]

Hmm, I didn't realize this feature was still so buggy. Still, in a few years, it will probably be considered as standard as the VT-x extensions.

IOMMUs are an interesting feature. I think if they had existed back in the 80s or 90s, operating systems might have evolved quite differently. Putting device drivers in userspace doesn't seem quite so absurd if they can access I/O ports safely. Of course, there are a lot of other things that would need to happen to make that a realistic choice, but it at least opens the door.

Defence in depth

Posted Sep 27, 2011 23:06 UTC (Tue) by mpr22 (subscriber, #60784) [Link]

Didn't Sun boxes have IOMMUs in the 90s? (OK, not exactly commodity hardware...)

Defence in depth

Posted Sep 27, 2011 3:37 UTC (Tue) by Cyberax (✭ supporter ✭, #52523) [Link]

Well, it depends on a definition of 'secure'. At least, SeL4 is formally correct and verified which automatically kills a lot of possible attack vectors.

Capability-based security properties are easily proven, but not very interesting.

Defence in depth

Posted Sep 29, 2011 12:49 UTC (Thu) by trasz (guest, #45786) [Link]

Of course it is. STOP (XTS-400), for example.