I’m not familiar with this, but what does “solved” mean in this case? Guaranteed inability to compromise systems?

Pretty much. If you've got a microkernel / capabilities based OS, the amount of mischief that someone can cause is severely reduced.

It's my belief that we can have general purpose, easy to use, secure computing for everyone.

No UAC crap, or horrible systems like AppArmor, no virus scanners, etc... just computers that do what you want, and only what you want.

We could have had it decades ago, if things had happened in a slightly different sequence order, related to the flood of personal computers.

Capabilities-based OSes aren't magic. Their robustness still depends on underlying assumptions, which may or may not hold. See eg relevant disclaimers in seL4 whitepaper(s).

And hardware glitches are a thing (edit: and supply chain attacks).

But I do agree that verified correct software can offer very strong guarantees that go well beyond those of commonly deployed software. We could have been in a much better place today.

their robustness lives in hardware capabilities. amd64 and intel x86_64 have quite good features but people dont use them well. For example you can have your microkernel be at the hypervisor level and thoroughly isolate devices etc through IOMMU and have almost no attack surface to get access deep enough to make significant changes to the security posture.

still not immune to be hacked ofc. I think the last step would be making it common place again to build these things custom. that way they'd have to have more specific information available as threat actors to exploit you. It'd be harder to have generic methods affecting millions of systems.

regardless there are no silverbullets, and tradecraft/opsec will always be a thing. most compromises are because people hand out keys unwittingly rather than 0days and crazy sploits. (they do happen though, but its more expensive than fishing and just loggin on under some dudes credentials)

To clarify: capabilities-based OS != verified correct software.

But there's much synergy there. Each enhances the other.

How much does this limit what a computer can do? E.g. if I converted an Ubuntu desktop into a "secure microkernel", what functionality would be lost?

Everything but the specific usage

But what does that mean? Can I browse a webpage, open a doc, if those are listed as specific usage? And if not, what's the purpose of this and why are people talking about it with such import?

most people dont do a lot on their machines. they have specific tasks they want to do. The idea is to isolate by default and crack open gaps by policy. You can still do 'anything' but you wouldnt want to enable 'anything' to be possible in the policy..

Sounds like security through compartmentalization is more user-friendly: You can run whatever you want and how you want it in a dedicated VM, keeping sensitive things safely isolated, without much thinking of what to enable. Case in point: Qubes OS, my daily driver. Btw it already exists and is stable.

> security through compartmentalization is more user-friendly: You can run whatever you want and how you want it in a dedicated VM, keeping sensitive things safely isolated

My brain hurts. How is a system where you can run whatever you want, however you want, but still keep sensitive things safely isolated possible?

Either you have restrictions on what you can run or access (in which case those limit sandboxed capabilities) or you have a hypothetically secure system, the security features of which you never leverage (because sandboxes have absolute freedom).

Unless you were talking about the ability to guarantee a monitor-only hypervisor or resource slice a machine into multiple tenants? (i.e. no/light touch hypervisor situations)

I'm not sure I understand your question. VMs run full operating systems on top of Xen hypervisor relying on hardware-assisted virtualization (VT-d or similar). You can run untrusted software in a dedicated VM and keep your sensitive data in another offline VM.

The dom0 has no network and doesn't manage, e.g., USB devices.

building such an OS for many years now..Qubes gets close enough but its super heavy, trying to support existing apps. I make my own so its super light weight, but no one will use it but me because their toolz arent supported (nothing is :D).

there are some BSD spinoffs like 5BSD which might end up with a good capability model but even there things like capsicum have their limits and IOMMU based isolation is still a dream. (because entire OS kernel is in one privilege level, accessible as root user, so DMA capable devices kill a lot of those securities).

(my os puts every subsystem, service, device driver, app etc. in their own hardware VM, likely there will be IPC bugs or hypercall bugs still tho in that case)

Nowadays with AI its getting more to a point where people can actually build these systems for themselves. Maybe that is a bigger threat to these big corporate tech companies than some security things. It will allow nations and companies to detach from their Tech...

That would stop a lot of kernel-based exploits but you can also do a lot of damage just as a user of course.

seL4[0] being the formally-proven modern representative.

0. https://sel4.systems/

sel4 is neat. and open source. there are many like it proprietary.

I am not aware of any microkernel actually competitive with seL4, open or else.

Can you recommend any modern systems that behave like that?

https://genode.org

this is a step forward but they need to lean into hw isolation more. definitely a very interesting project. inspiring :)

[deleted]