With millions of LoCs, it is no surprise there are bugs.

Worse yet, the kernel runs in supervisor mode.

This kernel design is bankrupt. There's much better available, such as seL4+Genode.

Please try keeping your snide comments to issues they actually apply to. This is a logic bug, with the kernel missing a piece of abnormality handling. You can get the exact same bug in a microkernel (or, FWIW, a memory safe, e.g. Rust) implementation; neither of those concepts help here.

▲

snvzz a day ago | parent [-]

>You can get the exact same bug in a microkernel

Absolutely. And yet, it is that much easier to keep a tiny codebase bug-free.

And only that tiny codebase has to run with supervisor privileges.

▲

eqvinox 21 hours ago | parent [-]

Of course a tiny microkernel code base won't have NFS bugs. It doesn't implement NFS. The bug will instead be in the NFS process/daemon/service/… which considering it's an fs service won't exactly be unprivileged either, even if only by returning maliciously corrupted contents. (e.g. a SUID root file that should not exist.)

And, sure, a microkernel could have better security properties. However, (1) this has no connection at all to this specific bug, and (2) the Linux kernel seems to be doing reasonably well on security properties; or rather the industry seems to have decided it's sufficiently secure, even if not perfect.

▲

snvzz 12 hours ago | parent [-]

Not only is the damage contained, but it is also much easier to protect an isolated NFS server.

For instance, instead of being able to read/write/jump literally anywhere in memory, it would only have capabilities to the resources it needs.

And these capabilities would be enforced strictly, by the bug-free microkernel. The likes of seL4 even have formal proof of correctness.

	▲	eqvinox 9 hours ago \| parent [-]
		And you are still making these arguments on the discussion of a bug that they have absolutely no bearing on. If Linux were written with the same exact development history, but as a microkernel, the exact same bug could (and likely would) exist in the NFS client component. The impact is spurious unavailability of service, and would be the same on a microkernel; it is not exploitable for memory corruption. And any file system service, by its function, will be in a position of relative privilege, even if less so on a microkernel. Your arguments are likely valid, with other bugs. Please take them there. Wedging this discussion in here just makes you look like a proselytizing zealot.

▲

burnt-resistor a day ago | parent | prev | next [-]

seL4 exhibited great advances in software engineering processes and advances in correctness, zero-copy microkernel IPC performance, and capabilities-based security, but these need explanation, adaptation, and evangelism to real-world use-cases like Linux.

Microkernels have severe limitations when it comes to transactional boundaries of calling multiple subsystems and rolling back on failure.

Linux has too much inertia to reinvent itself instantly or completely into XYZ.

What would add more value would be gradual conversion to Rust and adding formal verification to C and Rust like specifying invariants in comments/metadata like frama-c and/or flux.

PS: Religious judgement opinion wars are rarely constructive.

▲

eddythompson80 a day ago | parent | prev | next [-]

seL4+Genode is equally as bankrupt. I run my code in the SMM anyway.

▲

lotharcable a day ago | parent | prev [-]

> This kernel design is bankrupt. There's much better available, such as seL4+Genode.

I am sure that the tech community would love to read the details of your great success in deploying microkernels for large variety of production workloads.