And if anyone is in Cambridge, the Museum of Technology has both a collection of early printing machines and a load of fixed steam engines. They don’t run the steam engines every day, but will next on the 11th of December. Well worth a trip (my inner geek child enjoyed the steam engine, my inner adult geek enjoyed the typesetting shed).
I have a recording of the presentation, although I’m not a seasoned speaker so it’s a little awkward.
The presentation is actually very good! The brief introduction to the distinguishing features of OpenBSD in the first half of your talk is particularly helpful to me, though the simplicity of BSD demonstrated by the second half is also impressive!
I’d argue that seL4 isn’t an operating system but merely a microkernel. Most of the insecurities in common systems these days happen outside its scope (where, for a long time, the focus was up the stack, but with all the CPU side channels, people are now looking down the stack, too) so whatever you add to seL4 to make it useful needs to be evaluated as well.
For example: Having an “unbreakable” seL4 is a nice basic component (and helps contain some damage) but is of little comfort if your file system server is thoroughly broken, giving attackers unbounded access to your data.
I’d argue that seL4 isn’t an operating system but merely a microkernel.
I’d argue it’s not even that. For example, seL4 has no dynamic memory management in the kernel, rather, dynamic memory management is pushed to userspace. And it’s not that seL4 doesn’t use dynamic memory, in a real system that uses seL4 you have to implement it. seL4 is proven correct in the sense of not violating its invariants regardless of what the userspace is doing, but of course, the interesting part of a production system is in the userspace, not in the kernel.
If you want to formally prove your dynamic memory allocator, you are on your own, seL4 won’t help you.
Not to take anything away from the seL4 folks, what they did is both important and impressive, and I recommend anyone to read the papers, which are very approachable, but comparing components of a system with the system is a category error.
Similarly, comparing an embedded real-time system with an interactive timesharing system is also apple and oranges…
Similarly, comparing an embedded real-time system with an interactive timesharing system is also apple and oranges…
seL4 does both. It implements mixed criticality. Critical realtime tasks and non-critical tasks can share the same system, without detriment to the properties the critical tasks need. The guarantees hold.
in a real system that uses seL4 you have to implement it (dynamic memory).
Not really. Many scenarios can and are in fact often implemented without dynamic memory; Components get what they need as they’re launched and that’s it. Non-deterministic behavior is avoided in critical systems.
Furthermore, in a mixed criticality scenario, a subset of the non-critical tasks might actually get dynamic memory from a memory manager that has a limited pool of memory to begin with, doesn’t deal with non-critical tasks and thus does not need to be part of the TCB, nor formally proven.
comparing components of a system with the system is a category error.
This much is correct. Openbsd is more than the kernel or the base system. It’s the whole thing.
SeL4, however, is a much better kernel than Openbsd’s is, on a fundamental level. But (unlike Minix3’s design) a system built around seL4 is not going to be UNIX-like. At most it will offer POSIX compatibility.
Which is why I suggested “The most secure UNIX-like”. Because seL4 isn’t that, and Minix3 could be but isn’t quite there.
I’d argue that seL4 isn’t an operating system but merely a microkernel.
Fair.
but is of little comfort if your file system server is thoroughly broken
Much emphasis must be put on seL4 being built around the concept of capabilities, making it better on a fundamental level, as it actually allows for security, which isn’t possible with UNIX’s ambient authority, due to the confused deputy problem.
In this case, no matter how broken one instance of filesystem server is, it won’t affect processes that aren’t using it, nor other filesystem servers, nor any block devices that the filesystem server does not have a capability to. The affected fs server might not be part of the TCB. SeL4’s design allows for critical and non-critical (mixed criticality) tasks to run in the same system, with formal proof of enforcement of separation. It might be that the system is at the core of the hard realtime flight system of an helicopter full of people, keeping them safe despite this compromised fs server being stuck in an infinite loop.
Remarkably, filesystems aren’t mounted in a global vfs as they are in UNIX, either. Whereas most processes, even those using files, do not have capabilities to filesystem access. To read a file, all that’s needed is a capability to it. There’s no need to e.g. know where it does reside.
I’m well aware of how things are ideally done in a microkernel system. Thing is, people ask for (see sibling answer) and implement shortcuts.
File system access is among the harder parts to fully redesign due to the many expectations users have when it comes to file management, so I picked that one as an example. See Android and iOS, both which tried to deemphasize files as a category but gave up at some point and ship file system browsers now.
Thus I expect file system access to allow (not necessarily use, in all cases) broad access capabilities instead of the fine grained scheme advocated in microkernel/security kernel design literature (“user wants to open a file, so the editor process asks the file picker service. The file picker provides the UI to select files, but can’t read their contents. When the user has chosen, the file picker sends a capability to the editor process that provides the desired level of access to that file only, without even telling where it resides”)
This definitely feels like a good design. Are there intermediates possible? Such as limiting the effect of troubles in one subsystem onto the other, and bringing more features from microkernels to other operating systems?
After all, MINIX3 is a distribution of NetBSD with the MINIX microkernel…
I’m the author of these slides. I’ve changed the wording to say “most secure general purpose operating system in the world” in order to fix the issue you have with it. I’m a little disappointed the discussion has gone so far in this direction considering it’s meant as an introduction to OpenBSD for non-OpenBSD folk, and not a document of absolute truths.
Good work, I really liked them. I was also happy about the effort promoting Openbsd; There doesn’t seem to be anywhere near enough of that.
I’ve changed the wording to say “most secure general purpose operating system in the world” in order to fix the issue you have with it.
Well-intended change, but still, I stand by “most secure UNIX-like”.
Some people seemingly believe it’s impossible to make a general-purpose operating system out of a microkernel. Like Genode (which implements Sculpt, a general-purpose dynamic scenario), I strongly object to this belief.
I’m a little disappointed the discussion has gone so far in this direction
As an Openbsd user (and fan) I’m also as disappointed that this thread got the discussion this far off track, when my nitpick was explicitly a nitpick.
I am claiming “most secure” just like I’d claim “my dad’s the best dad”. Lightheartedly, but then checking out what OpenBSD does toward security I see there is something going on for real here.
I do not care too much how many the 1 most secure operating systems there are around. I prefer “more secure everyday”, as you cannot reach this goal for real, feels funnier.
Proof of correctness aren’t the same as proofs of security. It’s entirely possible to correctly specify that the wrong person is allowed to access my data – and, in most major security breaches I read about, it seems like that’s precisely what happens: Someone leaves an S3 bucket wide open, and an attacker looks at it. No component of the system has malfunctioned (other than the human in charge of configuring things, arguably).
In my opinion, a secure system is one designed to not only be correct – that’s necessary, but not sufficient. It’s also one designed to restrict what the user-facing components are able to access by default, making it easy to reason who is able to access what, and focusing on reducing the number of places where interactions of correctly-functioning components can lead to unexpected behaviors.
Proof of correctness aren’t the same as proofs of security.
Yet seL4 is provably secure, as the proofs cover security enforcement. The kernel does guarantee confidentiality, integrity and availability. What you do with the kernel is up to you, but it does offer the tools. Building a secure system with it is thus possible. It also ensures safety of time-critical systems, by providing a sound analysis of worst-case execution time. More on this in the whitepaper.
It’s also one designed to restrict what the user-facing components are able to access by default,
Capabilities give explicit access to fine-grained resources, and thus they make POLA a possibility, whereas ambient authority runs contrary to POLA and does hinder efforts to attain security.
Openbsd is no doubt the most secure UNIX-like at the present time, but UNIX isn’t the definitive of operating system design, nor anywhere near perfect by any means.
Still, it doesn’t have the best possible overall design for a UNIX, from a security or reliability perspective. Minix3 is much closer to that, by going much further in privilege separation thanks to its pure microkernel, multiserver design.
It feels like OpenBSD aims protecting the userland in addition to the kernel itself. With alternate implementations incorporating privsep features (the pledge(2) unveil(2) dance).
So maybe OpenBSD userbase, designed to split responsibility and privilege across components communicating (imsg, pipes, unix sockets…) between each other, would be a good fit for something like SeL4 ? Maybe making use of CAmkES (that I still do not know) ?
If I had the resources (time or excess money to buy developer time with), I’d personally give Minix3 (a stalled project) its much needed push.
It’s still limited by the fact it implements a UNIX system, but thanks to its pure microkernel, multiserver architecture and its fault tolerance focus, it can do what Openbsd, limited by its monolith kernel, cannot.
pledge/unveil
Are really clever, and a feature I wish everybody else in the UNIX world adopted. I understand Dragonfly has made some steps into that, but to my knowledge nobody else has.
Selection bias. lobste.rs was originally founded by @jcs who is an OpenBSD developer, this naturally drew a lot of OpenBSD people towards the site. Quick grep hats for “openbsd.org” lists 20 committers with accounts on this site.
I stand by UNIX-like, which is very different from general purpose.
There’s many ways to create general purpose operating systems without making a copy of UNIX. Many of them are fundamentally better equipped for security than UNIX is.
There’s also the quite unfortunate widespread yet baseless belief that microkernels aren’t suitable for the creation of general purpose operating systems. I’ll take steps to prevent supporting these beliefs, if they are easy and harmless to take. Restricting the claim to UNIX-like is one such step.
Openbsd isn’t the most secure operating system in the world.
the article did not state that OpenBSD is the most secure operating system in the world
“openbsd is widely considered to be …” is the claim the author is making; the … is what the author is saying a lot of people believe. this is how english works.
“openbsd is widely considered to be …” is the claim the author is making
And that’s the claim I’ve addressed. I quote myself (top level post) here:
While true (the widely considered part), it definitely isn’t the most secure operating system in the world.
The explicit nitpick was, very specifically, to ensure nobody falls for the “widely considered” trap and walks away with an unfortunately incorrect belief.
To achieve this, it’s necessary to point out why the belief is incorrect (a simple counterexample), and what small change would instead make it correct: The most secure UNIX-like.
So that’s what my post was meant to achieve, and how it was implemented to achieve the intended result.
it’s subjective whether the statement is misleading, or whether a clarification is useful or needed. the response tells you what others think, which is important if you care about clear communication.
my last comment was responding to your statment that “it isn’t true unless qualified,” which is different from what it seems you are now saying, that people might misunderstand the “widely considered” part.
at any rate my subjective opinion is that the statement is fine, and we can expect tech readers not think the author is denying the existence of academic or niche projects that are technically more secure, whatever that means.
The original statement (“widely considered”) only considers sentiment (and describes it reasonably well, I think). Your statement (”[being] the most secure operating system”) is much harder to deal with, not the least because it assumes that one could sort operating system by “security” - but that depends on the definition of security which is vast.
As mentioned somewhere else in the thread, seL4 still uses dynamic memory management in kernel, even though it defers that management to a userspace process. Muen (www.muen.sk) is designed to not need that at all, so there won’t be a kernel-needs-memory-but-can’t-get-it situation. Arguably that could be considered more secure than any seL4 configuration. Then again, the entire security model of Muen hinges on Intel VT-x and VT-d, so… maybe not?
The original statement (“widely considered”) only considers sentiment (and describes it reasonably well, I think).
Sure, and I addressed that on my post at the top level. To be careful and not confuse the two. As a nitpick.
Then again, the entire security model of Muen hinges on Intel VT-x and VT-d, so… maybe not?
I like seL4’s approach to virtualization better anyway. Run VMM (which handles vm exits/exceptions) unprivileged. Since it doesn’t get more capabilities than it needs, an otherwise successful VM escape by attacking the VMM is fruitless.
so there won’t be a kernel-needs-memory-but-can’t-get-it situation.
No worries, seL4’s kernel can’t be in that situation.
BSDCan! https://www.bsdcan.org/
Working on writing a toy 9p library in zig
Playing around with writing sqlite extensions in zig
For anyone interested in what the hot metal typesetting process looks like: https://www.youtube.com/watch?v=EzilaRwoMus
Also, everyone should watch Farewell, Etaoin Shrdlu
And if anyone is in Cambridge, the Museum of Technology has both a collection of early printing machines and a load of fixed steam engines. They don’t run the steam engines every day, but will next on the 11th of December. Well worth a trip (my inner geek child enjoyed the steam engine, my inner adult geek enjoyed the typesetting shed).
I’ve uploaded the talk video to YouTube after many people have asked me for a copy of the video. https://www.youtube.com/watch?v=EkDVKthufAM
The presentation is actually very good! The brief introduction to the distinguishing features of OpenBSD in the first half of your talk is particularly helpful to me, though the simplicity of BSD demonstrated by the second half is also impressive!
Much appreciated.
Slides are meant to complement talks, not replace them.
Nitpick:
While true (the widely considered part), it definitely isn’t the most secure operating system in the world.
That label belongs to seL4, which has formal proof of correctness.
A better statement would be qualified, like: “most secure UNIX-like…”
I’d argue that seL4 isn’t an operating system but merely a microkernel. Most of the insecurities in common systems these days happen outside its scope (where, for a long time, the focus was up the stack, but with all the CPU side channels, people are now looking down the stack, too) so whatever you add to seL4 to make it useful needs to be evaluated as well.
For example: Having an “unbreakable” seL4 is a nice basic component (and helps contain some damage) but is of little comfort if your file system server is thoroughly broken, giving attackers unbounded access to your data.
I’d argue it’s not even that. For example, seL4 has no dynamic memory management in the kernel, rather, dynamic memory management is pushed to userspace. And it’s not that seL4 doesn’t use dynamic memory, in a real system that uses seL4 you have to implement it. seL4 is proven correct in the sense of not violating its invariants regardless of what the userspace is doing, but of course, the interesting part of a production system is in the userspace, not in the kernel.
If you want to formally prove your dynamic memory allocator, you are on your own, seL4 won’t help you.
Not to take anything away from the seL4 folks, what they did is both important and impressive, and I recommend anyone to read the papers, which are very approachable, but comparing components of a system with the system is a category error.
Similarly, comparing an embedded real-time system with an interactive timesharing system is also apple and oranges…
seL4 does both. It implements mixed criticality. Critical realtime tasks and non-critical tasks can share the same system, without detriment to the properties the critical tasks need. The guarantees hold.
Not really. Many scenarios can and are in fact often implemented without dynamic memory; Components get what they need as they’re launched and that’s it. Non-deterministic behavior is avoided in critical systems.
Furthermore, in a mixed criticality scenario, a subset of the non-critical tasks might actually get dynamic memory from a memory manager that has a limited pool of memory to begin with, doesn’t deal with non-critical tasks and thus does not need to be part of the TCB, nor formally proven.
This much is correct. Openbsd is more than the kernel or the base system. It’s the whole thing.
SeL4, however, is a much better kernel than Openbsd’s is, on a fundamental level. But (unlike Minix3’s design) a system built around seL4 is not going to be UNIX-like. At most it will offer POSIX compatibility.
Which is why I suggested “The most secure UNIX-like”. Because seL4 isn’t that, and Minix3 could be but isn’t quite there.
Fair.
Much emphasis must be put on seL4 being built around the concept of capabilities, making it better on a fundamental level, as it actually allows for security, which isn’t possible with UNIX’s ambient authority, due to the confused deputy problem.
In this case, no matter how broken one instance of filesystem server is, it won’t affect processes that aren’t using it, nor other filesystem servers, nor any block devices that the filesystem server does not have a capability to. The affected fs server might not be part of the TCB. SeL4’s design allows for critical and non-critical (mixed criticality) tasks to run in the same system, with formal proof of enforcement of separation. It might be that the system is at the core of the hard realtime flight system of an helicopter full of people, keeping them safe despite this compromised fs server being stuck in an infinite loop.
Remarkably, filesystems aren’t mounted in a global vfs as they are in UNIX, either. Whereas most processes, even those using files, do not have capabilities to filesystem access. To read a file, all that’s needed is a capability to it. There’s no need to e.g. know where it does reside.
I’m well aware of how things are ideally done in a microkernel system. Thing is, people ask for (see sibling answer) and implement shortcuts.
File system access is among the harder parts to fully redesign due to the many expectations users have when it comes to file management, so I picked that one as an example. See Android and iOS, both which tried to deemphasize files as a category but gave up at some point and ship file system browsers now.
Thus I expect file system access to allow (not necessarily use, in all cases) broad access capabilities instead of the fine grained scheme advocated in microkernel/security kernel design literature (“user wants to open a file, so the editor process asks the file picker service. The file picker provides the UI to select files, but can’t read their contents. When the user has chosen, the file picker sends a capability to the editor process that provides the desired level of access to that file only, without even telling where it resides”)
That’d be quite sad. If it helps be more optimistic, know that Genode’s dynamic general-purpose scenario, Sculpt, does not fall into that trap.
This definitely feels like a good design. Are there intermediates possible? Such as limiting the effect of troubles in one subsystem onto the other, and bringing more features from microkernels to other operating systems?
After all, MINIX3 is a distribution of NetBSD with the MINIX microkernel…
I wish Netbsd took Minix3 under its wing. Minix3 is a good idea, and I’m saddened to see it isn’t as active as I’d like it to be.
I’m the author of these slides. I’ve changed the wording to say “most secure general purpose operating system in the world” in order to fix the issue you have with it. I’m a little disappointed the discussion has gone so far in this direction considering it’s meant as an introduction to OpenBSD for non-OpenBSD folk, and not a document of absolute truths.
Don’t worry. With an increase in popularity, the amount of nitpickers increases as well. Thanks for creating and publishing the slides!
Good work, I really liked them. I was also happy about the effort promoting Openbsd; There doesn’t seem to be anywhere near enough of that.
Well-intended change, but still, I stand by “most secure UNIX-like”.
Some people seemingly believe it’s impossible to make a general-purpose operating system out of a microkernel. Like Genode (which implements Sculpt, a general-purpose dynamic scenario), I strongly object to this belief.
As an Openbsd user (and fan) I’m also as disappointed that this thread got the discussion this far off track, when my nitpick was explicitly a nitpick.
I am claiming “most secure” just like I’d claim “my dad’s the best dad”. Lightheartedly, but then checking out what OpenBSD does toward security I see there is something going on for real here.
I do not care too much how many the 1 most secure operating systems there are around. I prefer “more secure everyday”, as you cannot reach this goal for real, feels funnier.
Proof of correctness aren’t the same as proofs of security. It’s entirely possible to correctly specify that the wrong person is allowed to access my data – and, in most major security breaches I read about, it seems like that’s precisely what happens: Someone leaves an S3 bucket wide open, and an attacker looks at it. No component of the system has malfunctioned (other than the human in charge of configuring things, arguably).
In my opinion, a secure system is one designed to not only be correct – that’s necessary, but not sufficient. It’s also one designed to restrict what the user-facing components are able to access by default, making it easy to reason who is able to access what, and focusing on reducing the number of places where interactions of correctly-functioning components can lead to unexpected behaviors.
Yet seL4 is provably secure, as the proofs cover security enforcement. The kernel does guarantee confidentiality, integrity and availability. What you do with the kernel is up to you, but it does offer the tools. Building a secure system with it is thus possible. It also ensures safety of time-critical systems, by providing a sound analysis of worst-case execution time. More on this in the whitepaper.
Capabilities give explicit access to fine-grained resources, and thus they make POLA a possibility, whereas ambient authority runs contrary to POLA and does hinder efforts to attain security.
Openbsd is no doubt the most secure UNIX-like at the present time, but UNIX isn’t the definitive of operating system design, nor anywhere near perfect by any means.
Still, it doesn’t have the best possible overall design for a UNIX, from a security or reliability perspective. Minix3 is much closer to that, by going much further in privilege separation thanks to its pure microkernel, multiserver design.
It feels like OpenBSD aims protecting the userland in addition to the kernel itself. With alternate implementations incorporating privsep features (the pledge(2) unveil(2) dance).
So maybe OpenBSD userbase, designed to split responsibility and privilege across components communicating (imsg, pipes, unix sockets…) between each other, would be a good fit for something like SeL4 ? Maybe making use of CAmkES (that I still do not know) ?
If I had the resources (time or excess money to buy developer time with), I’d personally give Minix3 (a stalled project) its much needed push.
It’s still limited by the fact it implements a UNIX system, but thanks to its pure microkernel, multiserver architecture and its fault tolerance focus, it can do what Openbsd, limited by its monolith kernel, cannot.
Are really clever, and a feature I wish everybody else in the UNIX world adopted. I understand Dragonfly has made some steps into that, but to my knowledge nobody else has.
Way to take the focus off of an already under-appreciated thing.
I don’t know, OpenBSD gets a lot of love on lobste.rs.
It used to, but I think quite some OpenBSD devs have moved away from lobste.rs over the years.
Selection bias. lobste.rs was originally founded by @jcs who is an OpenBSD developer, this naturally drew a lot of OpenBSD people towards the site. Quick grep hats for “openbsd.org” lists 20 committers with accounts on this site.
fallacy of composition, sick burn, next
(please read this as me attempting humor, not me being insulting :) )
I think a better statement would have been: “Widely considered to be the most secure general purpose operating system in the world”
I stand by UNIX-like, which is very different from general purpose.
There’s many ways to create general purpose operating systems without making a copy of UNIX. Many of them are fundamentally better equipped for security than UNIX is.
There’s also the quite unfortunate widespread yet baseless belief that microkernels aren’t suitable for the creation of general purpose operating systems. I’ll take steps to prevent supporting these beliefs, if they are easy and harmless to take. Restricting the claim to UNIX-like is one such step.
no
no need to add qualifications to a true statement which aren’t relevant to the topic. at least here it feels like it would add confustion.
That’s the issue. It isn’t true unless qualified. Openbsd isn’t the most secure operating system in the world.
I doubt the authors themselves do appreciate this sort of advertisement, either.
the article did not state that OpenBSD is the most secure operating system in the world
“openbsd is widely considered to be …” is the claim the author is making; the … is what the author is saying a lot of people believe. this is how english works.
And that’s the claim I’ve addressed. I quote myself (top level post) here:
The explicit nitpick was, very specifically, to ensure nobody falls for the “widely considered” trap and walks away with an unfortunately incorrect belief.
To achieve this, it’s necessary to point out why the belief is incorrect (a simple counterexample), and what small change would instead make it correct: The most secure UNIX-like.
So that’s what my post was meant to achieve, and how it was implemented to achieve the intended result.
What happened instead honestly baffles me.
it’s subjective whether the statement is misleading, or whether a clarification is useful or needed. the response tells you what others think, which is important if you care about clear communication.
my last comment was responding to your statment that “it isn’t true unless qualified,” which is different from what it seems you are now saying, that people might misunderstand the “widely considered” part.
at any rate my subjective opinion is that the statement is fine, and we can expect tech readers not think the author is denying the existence of academic or niche projects that are technically more secure, whatever that means.
The original statement (“widely considered”) only considers sentiment (and describes it reasonably well, I think). Your statement (”[being] the most secure operating system”) is much harder to deal with, not the least because it assumes that one could sort operating system by “security” - but that depends on the definition of security which is vast.
As mentioned somewhere else in the thread, seL4 still uses dynamic memory management in kernel, even though it defers that management to a userspace process. Muen (www.muen.sk) is designed to not need that at all, so there won’t be a kernel-needs-memory-but-can’t-get-it situation. Arguably that could be considered more secure than any seL4 configuration. Then again, the entire security model of Muen hinges on Intel VT-x and VT-d, so… maybe not?
Sure, and I addressed that on my post at the top level. To be careful and not confuse the two. As a nitpick.
I like seL4’s approach to virtualization better anyway. Run VMM (which handles vm exits/exceptions) unprivileged. Since it doesn’t get more capabilities than it needs, an otherwise successful VM escape by attacking the VMM is fruitless.
No worries, seL4’s kernel can’t be in that situation.