Not logged in
Log in now
Create an account
Subscribe to LWN
LWN.net Weekly Edition for May 16, 2013
A look at the PyPy 2.0 release
PostgreSQL 9.3 beta: Federated databases and more
LWN.net Weekly Edition for May 9, 2013
(Nearly) full tickless operation in 3.10
Formally verified kernels which are immune to stack overflow and other low-level hacks are a-plenty. Even hardware IOMMU is common already.
So a secure OS is possible and probably would be implemented sooner or later.
Defence in depth
Posted Sep 26, 2011 20:23 UTC (Mon) by nevets (subscriber, #11875)
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.
Posted Sep 26, 2011 20:51 UTC (Mon) by smurf (subscriber, #17840)
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.
Posted Sep 26, 2011 21:27 UTC (Mon) by dgm (subscriber, #49227)
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.
Posted Sep 26, 2011 22:15 UTC (Mon) by cmccabe (guest, #60281)
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.
Posted Sep 27, 2011 16:18 UTC (Tue) by nix (subscriber, #2304)
Posted Sep 27, 2011 20:59 UTC (Tue) by cmccabe (guest, #60281)
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.
Posted Sep 27, 2011 23:06 UTC (Tue) by mpr22 (subscriber, #60784)
Posted Sep 27, 2011 3:37 UTC (Tue) by Cyberax (✭ supporter ✭, #52523)
Capability-based security properties are easily proven, but not very interesting.
Posted Sep 29, 2011 12:49 UTC (Thu) by trasz (guest, #45786)
Copyright © 2013, Eklektix, Inc.
Comments and public postings are copyrighted by their creators.
Linux is a registered trademark of Linus Torvalds