Mastodawn

Christine Lemmer-Webber 1d ago

The fact of the matter is, most vulnerabilities fall under extremely common patterns, with known solutions:

- Confused deputies: capability security can fix/contain this in many cases, more on that later
- Injection attacks: primarily caused by string templating, using structured templating also fixes this (quasiquote, functional combinators, etc)
- Memory vulnerabilities: solved by memory-safe languages, and yes that includes Rust, but it also includes Python, Scheme/Lisp, etc etc etc

There are other serious vulnerabilities, such as incorrectly written or used cryptography, and others from there, but my primary point is: most damage can be either avoided in the first place or contained (especially in terms of capability security for containment)

And... patching AIgen patches is going to get tough and tiring... (cotd...)

Christine Lemmer-Webber 1d ago

I don't think human reviewers are going to be able to keep up with the number of vulnerabilities we're seeing appear. I really don't. Humans won't be able to review at scale, and I also think that there's serious risks for blindly accepting AIgen patches, which for critical infrastructure could also be a path to *inserting new* vulnerabilities.

We need to attack this systemically.

I have more to say. More later. But that's the gist for now.

@cwebber we need microkernel based operating systems with capability-based security enforcement, isolation of components from each other as a baseline assumption, and formal verification of the whole thing at both the code and spec level, and we need all of this quite urgently

Daniel Lakeland

I'd set aside the formal verification requirement to get the rest of it. I really do think microkernels were the right way to go, it's just that in 1992 or whatever the consumer hardware wasn't up to the task. I think probably around 2005 or so the hardware started to be able to afford to do that. But that's approximately the time that VMs and containers took off. Now we have this giant mess.

@dlakelan @cwebber i do not think that setting aside the formal verification is wise, and i also do not think it poses a technical barrier that we cannot surpass. especially since we already have formally verified microkernels with capability-based security that can be used today within full desktop operating systems

what needs to happen is for people to put the pieces together and polish it into a system regular folks can actually use

Daniel Lakeland 1d ago

If you mean formally verifying the microkernel itself... yeah. I'm good with that. Isn't L4 formally verified? If you mean formally verifying every userspace daemon... Nice to have but I'm not holding my breath.

@dlakelan @cwebber kernel is the bare minimum, i'd also want verification of at least specs around the hardware abstraction layer and how hardware related daemons talk to everything else. but it should definitely be possible for common system components and daemons as well, and i think should be mandatory for trusted daemons that supervise or manage other untrusted ones

i doubt everything will be formally verified, but it is nonetheless a goal that should be worked towards, while finding ways to develop standard practices and make it easier to apply everywhere

@dlakelan @cwebber i'm glossing over a lot with the "trusted" vs "untrusted" here, and i recognize that. i've been thinking about this for the better part of a decade and conveying my mental model for this is not possible in a few pots in a social media thread

i just have not had the motivation or resources to spend on taking existing work in seL4/genode and assembling it with other pieces into the thing i'd like, writing specs, finding people to collaborate with on this, etc. life is busy and i already have so many projects

Daniel Lakeland 1d ago

I agree it would be nice to have, but I honestly think it primarily prevents progress. We'd be wildly better off with microkernel OSes that are at the same level of hackiness as the Linux kernel, and maybe have decent interfaces that could get replaced piecemeal as people came up with alternative implementations in memory safe languages, and then maybe formally verified at a later date.

Right now, you have to be comfortable working in kernel space to even do anything

@dlakelan @cwebber right now, this minute, you can go download SculptOS and have a microkernel-based OS with capability security that can run on a laptop and use its iGPU and run a web browser and virtualize linux and build itself using the Genode framework it is based on. and you can use that framework to swap out the process-level-virtualization-based default microkernel (NOVA iirc) with the formally verified seL4 (or other L4 family kernels) and never have to care about the API/ABI differences between microkernels because it abstracts that for you, nor the code inside the kernel.

Daniel Lakeland 1d ago

That's cool! I honestly had not followed any of this. I might have to dedicate an older laptop I have no real use for to this just for fun.

@dlakelan @cwebber this is to say, what you are asking for exists, and has existed in a usable state for well over a decade, and is in some cases more feature complete than some other open source operating systems that people use and even daily drive

you can run it on a pinephone, too

Christine Lemmer-Webber 20h ago

@linear @dlakelan I am aware of Sculpt / Genode and have run it on physical hardware before! I am also working on tech that is also part of the answer.

There is real work happening! It's going to take multiple efforts from multiple angles to get there

Daniel Lakeland 20h ago

@cwebber @linear

Sculpt/Genode seems really cool. I have long wanted to be able to hack OS components by working in userspace with languages like Scheme/LISP or Julia or Erlang or whatever. We have enough speed that we could let say firewalling / bridging / Routing be done in slightly less close-to-the-metal languages and gain tremendous flexibility. We can already see this kind of happening with eBPF and nftables and whatnot.

Kirtai 🏳️‍⚧️22h ago

@dlakelan @linear @cwebber
The Amiga had a very fast microkernel based OS in the 1980s, though memory protection was unfortunately not part of it.

Something like that in a memory safe language would be nice.

ティージェーグレェ 20h ago

"I really do think microkernels were the right way to go, it's just that in 1992 or whatever the consumer hardware wasn't up to the task."

100% microkernels were the right way to go!

They still are.

Alas, something threw a very angry GURU MEDIATION at the "in 1992 or whatever the consumer hardware wasn't up to the task" part of your statement. Amiga Workbench (a microkernel derived from the TripOS provenance) was absolutely the bees' knees on economical consumer hardware in the 1980s, and Commodore hadn't yet declared bankruptcy in 1992.

Heck, it's 2026 and I am pretty sure that there will probably still be Amiga related entries at @[email protected]
this weekend (wish I were there, alas $12,000ish USD in debt and it was going to cost around $2k USD just to fly there and have lodgings, so not this year).

Admittedly, the Amigas were pretty awesome insomuch as you could bypass the OS entirely. Kickstart was hella fast. Still is! Pretty sure my Amiga 2000 booted faster decades ago, with a SCSI hard drive (and my A1200 with IDE) than any contemporary "consumer" grade hardware shipping today, despite the Ghz in CPU clockspeeds these days (my Amigas' CPUs were measured in MHz and still sooooo speedy and usable).

CC: @[email protected] @[email protected]