4 ms·

One of the discussions that always forms when talking about formally verified software is the whole verifying-the-verifier scenario. AKA, all of the reasons why

One of the discussions that always forms when talking about formally verified software is the whole verifying-the-verifier scenario. AKA, all of the reasons why you still can't trust it. And while that is an interesting conversation to have, it does a disservice to the practical benefits of the software verification process. The Linux CVE database was recently analyzed and it was determined that 96% of the vulnerabilities would be mitigated to at least non-critical status, if not completely eliminated, if linux were a microkernel architecture. Now throw in capabilities oriented security, and most of non-critical exploits become non-exploits. Throw in formal verification of the kernel, and you've basically eliminated everything except for hardware exploits. Assuming mass adoption, what seL4 effectively does is turn million dollar black market zero days into billion dollar zero days...possibly more. A million dollar exploit probably isn't even a line-item in the FBI budget. A billion dollar exploit would be a "needs-congressional-approval" type of line-item in the national US intelligence budget. Unless your job revolves around protecting the nuclear arsenal of a major nation-state, you won't ever have to worry about OS vulnerabilities, and you can rely on the security characteristics of the OS to drastically narrow down your attack surface. To me, that is a pretty big deal. It is slowly becoming a moral imperative that we start adopting this sort of security as a core standard.

pjmlp 5y ago
The irony is that in cloud environments with dozen of layers on top of Linux kernel, the whole mikrokernel vs monolith is a moot point. So much for monolith performance, when one needs to pile layers and layers of security on top.
dmos62 5y ago
I'm fuzzy on what it would take for there to be a mainstream formally-verified micro-kernel capability-based OS. Is it probable for Linux to be gradually refactored into that, or are will it take a fundamentally new OS?
- CameronNemo 5y ago
  I think it would be possible to adapt some Linux drivers to run in a sandboxed capacity within a capability/microkernel system. IIRC there was once an L4 based project that integrated with Linux. https://en.wikipedia.org/wiki/L4Linux https://en.wikipedia.org/wiki/L4Linux
  - shandor 5y ago
    L4Linux is just the usual Linux paravirtualized on top of one the L4 microkernels. We previously ran two instances of it on top of L4/Fiasco The problem with that is that you don't actually get that much benefits from the underlying microkernel. Linux is just the same old monolith, just better isolated from the other resources not exposed to this particular (para)virtualized kernel instance, so you end up isolating more or less complete systems from each other rather than getting the normal benefits of capability based microkernel architecture inside a single system. Now that's not nothing of course, but not usually what people are after when they're hoping for a usable, modern microkernel system.
- darksaints 5y ago
  There are already some attempts at creating new operating systems off of seL4. The most complete at the moment is Genode. There are also attempts to port existing OSes to seL4, such as qubes. None of these are particularly mature. In terms of creating a Linux replacement, drivers are the biggest hurdle. There are some attempts to programmatically port the netbsd suite of drivers, which seems to be the most promising. Apart from that, drivers will likely need to be ported manually. The GNU userland is also unlikely to be ported easily en-masse due to the capabilities-oriented security model, although some projects would definitely be easier than others. Things like SystemD would be a monstrous task. I personally think that apart from drivers, which can use traditional microkernel approaches, it's probably time to start implementing some of the better OS ideas that have come out in the last 30 years, as opposed to just trying to replicate a posix environment. For example, NuShell has a ton of promise, but isn't particularly posix-y.
  - deleted 5y ago
    [deleted]
anp 5y ago
I’d love to dig into that CVE analysis if you have a link!
- darksaints 5y ago
  http://ts.data61.csiro.au/publications/csiro_full_text/Biggs_LH_18.pdf http://ts.data61.csiro.au/publications/csiro_full_text/Biggs...
lallysingh 5y ago
Summary acronyms: IoT should be on SeL4 on RISC-V. RISC-V fits the embedded space, and IoT usually doesn't need much more software on top than a kernel and a dumb control service. If an open-source control service (effectively just controlling some I/O pins depending on a config) can get verified, the entire threat vector of IoT would be devastated.
SkyMarshal 5y ago
Are there any projects anywhere developing a microkernel with a capability security model?
- y7 5y ago
  Yes, the seL4 project that is being discussed.
  - SkyMarshal 5y ago
    Oh, duh, thx. I hear linux and automatically think monolithic kernel.
mcguire 5y ago
"The Linux CVE database was recently analyzed and it was determined that 96% of the vulnerabilities would be mitigated to at least non-critical status, if not completely eliminated, if linux were a microkernel architecture." If Linux were a microkernel architecture, or if Linux were based on seL4? If Linux were based on the OSI Mk microkernel (I think that was the name; it was Mach-based), every system operation would be roughly an order of magnitude slower[1]. As for formal methods, I'm singing in the choir. [1] I've got the performance paper from the early '90s somewhere; it's hilarious. One benchmark was dhrystones: they didn't manage to physically slow down the processor. :-)
- darksaints 5y ago
  The mach microkernel was definitely slow, but I think you'd be surprised at how fast the L3 and L4 family of microkernels are. L4 IPC calls are some 20x faster than mach IIRC. L4Linux, which is Linux running on top of L4, is only 6-7% slower than native Linux. Cache locality is one hell of a drug. With seL4, the entire kernel consumes ~160KiB, which easily fits in most CPU caches.
ganafagol 5y ago
And of all the security issues exploited out there, how many have to do with the kernel? If some crappy javascript library leaks customers secrets for an online shop, where exactly is the OS kernel at fault? If the CEO's secretary gets convinced to wire $1M to an oversees account because somebody made them believe it's the boss requesting it, then how would a verified microkernel have helped? > The Linux CVE database was recently analyzed and it was determined that 96% of the vulnerabilities would be mitigated to at least non-critical status, if not completely eliminated, if linux were a microkernel architecture. In a fair comparison you need to consider the CVEs that a microkernel would suffer which had been eliminated with a monolithical kernel. Oh but it's verified, you say? Then the fair comparison is a verified monokernel vs a verified microkernel. Apples and oranges.
- PoignardAzur 5y ago
  Do verified monokernels exist? You can say that a comparison is unfair, but what matters is the end result of "which system ends up with the fewest vulnerabilities if/when it becomes widely used", and a formally verified microkernel seems like a strong bet on that front.

pjmlp 5y ago

The irony is that in cloud environments with dozen of layers on top of Linux kernel, the whole mikrokernel vs monolith is a moot point. So much for monolith performance, when one needs to pile layers and layers of security on top.

dmos62 5y ago

I'm fuzzy on what it would take for there to be a mainstream formally-verified micro-kernel capability-based OS. Is it probable for Linux to be gradually refactored into that, or are will it take a fundamentally new OS?

CameronNemo 5y ago
I think it would be possible to adapt some Linux drivers to run in a sandboxed capacity within a capability/microkernel system. IIRC there was once an L4 based project that integrated with Linux. https://en.wikipedia.org/wiki/L4Linux https://en.wikipedia.org/wiki/L4Linux
- shandor 5y ago
  L4Linux is just the usual Linux paravirtualized on top of one the L4 microkernels. We previously ran two instances of it on top of L4/Fiasco The problem with that is that you don't actually get that much benefits from the underlying microkernel. Linux is just the same old monolith, just better isolated from the other resources not exposed to this particular (para)virtualized kernel instance, so you end up isolating more or less complete systems from each other rather than getting the normal benefits of capability based microkernel architecture inside a single system. Now that's not nothing of course, but not usually what people are after when they're hoping for a usable, modern microkernel system.
darksaints 5y ago
There are already some attempts at creating new operating systems off of seL4. The most complete at the moment is Genode. There are also attempts to port existing OSes to seL4, such as qubes. None of these are particularly mature. In terms of creating a Linux replacement, drivers are the biggest hurdle. There are some attempts to programmatically port the netbsd suite of drivers, which seems to be the most promising. Apart from that, drivers will likely need to be ported manually. The GNU userland is also unlikely to be ported easily en-masse due to the capabilities-oriented security model, although some projects would definitely be easier than others. Things like SystemD would be a monstrous task. I personally think that apart from drivers, which can use traditional microkernel approaches, it's probably time to start implementing some of the better OS ideas that have come out in the last 30 years, as opposed to just trying to replicate a posix environment. For example, NuShell has a ton of promise, but isn't particularly posix-y.
- deleted 5y ago
  [deleted]

anp 5y ago

I’d love to dig into that CVE analysis if you have a link!

darksaints 5y ago
http://ts.data61.csiro.au/publications/csiro_full_text/Biggs_LH_18.pdf http://ts.data61.csiro.au/publications/csiro_full_text/Biggs...

lallysingh 5y ago

Summary acronyms: IoT should be on SeL4 on RISC-V. RISC-V fits the embedded space, and IoT usually doesn't need much more software on top than a kernel and a dumb control service. If an open-source control service (effectively just controlling some I/O pins depending on a config) can get verified, the entire threat vector of IoT would be devastated.

SkyMarshal 5y ago

Are there any projects anywhere developing a microkernel with a capability security model?

y7 5y ago
Yes, the seL4 project that is being discussed.
- SkyMarshal 5y ago
  Oh, duh, thx. I hear linux and automatically think monolithic kernel.

mcguire 5y ago

"The Linux CVE database was recently analyzed and it was determined that 96% of the vulnerabilities would be mitigated to at least non-critical status, if not completely eliminated, if linux were a microkernel architecture." If Linux were a microkernel architecture, or if Linux were based on seL4? If Linux were based on the OSI Mk microkernel (I think that was the name; it was Mach-based), every system operation would be roughly an order of magnitude slower[1]. As for formal methods, I'm singing in the choir. [1] I've got the performance paper from the early '90s somewhere; it's hilarious. One benchmark was dhrystones: they didn't manage to physically slow down the processor. :-)

darksaints 5y ago
The mach microkernel was definitely slow, but I think you'd be surprised at how fast the L3 and L4 family of microkernels are. L4 IPC calls are some 20x faster than mach IIRC. L4Linux, which is Linux running on top of L4, is only 6-7% slower than native Linux. Cache locality is one hell of a drug. With seL4, the entire kernel consumes ~160KiB, which easily fits in most CPU caches.

ganafagol 5y ago

And of all the security issues exploited out there, how many have to do with the kernel? If some crappy javascript library leaks customers secrets for an online shop, where exactly is the OS kernel at fault? If the CEO's secretary gets convinced to wire $1M to an oversees account because somebody made them believe it's the boss requesting it, then how would a verified microkernel have helped? > The Linux CVE database was recently analyzed and it was determined that 96% of the vulnerabilities would be mitigated to at least non-critical status, if not completely eliminated, if linux were a microkernel architecture. In a fair comparison you need to consider the CVEs that a microkernel would suffer which had been eliminated with a monolithical kernel. Oh but it's verified, you say? Then the fair comparison is a verified monokernel vs a verified microkernel. Apples and oranges.

PoignardAzur 5y ago
Do verified monokernels exist? You can say that a comparison is unfair, but what matters is the end result of "which system ends up with the fewest vulnerabilities if/when it becomes widely used", and a formally verified microkernel seems like a strong bet on that front.