> I wrote an essay explaining the issues here
This essay only addresses my second point - capabilities within a program. It doesn't address OS level capabilities at all.
But even in the space of programming languages, I find this essay extremely unconvincing. Like, you raise points like this:
> Here are some problems you’ll have to solve in order to sandbox libraries: What is your threat model? How do you stop components tampering with each other’s memory?
The threat model is left pad cryptolockering your computer via a supply chain attack. The solution is to design a language such that if I import leftpad, then call it, my computer can't get hacked.
You stop components tampering with each others' memory by using a memory safe language.
> its main() method must be given a “god object” exposing all the ambient authorities the app begins with
So what? The main function already takes arguments. I don't understand the problem.
Haskell already passes a type object as an argument to anything which does IO. They don't do it for security. Turns out having pure functions separated from non-pure functions is a beautiful thing.
Then there's these weird claims:
> Any mutable global variable is a problem as it may allow one component to violate expectations held by another.
You don't need to ban mutable global variables! Lets imagine we did this in safe rust. I think the only constraint is that a global variable can't be shared over the boundary between crates. But - nobody does that anyway. Even if you did share a global over a crate boundary, the child crate would still only be able to access it through methods on the type.
Sneaky developers could leverage globals to violate the security boundary. But it would be hard to do by accident. Maybe just, don't do that.
Your essay talks about some research project making a capability based java subset. And I understand that the resulting ergonomics weren't very good. But that isn't evidence that capabilities themselves are a bad idea. If a research student wrote a half baked C compiler one time, you wouldn't take that as evidence that C compilers are a bad idea. I do, however, accept that the burden of proof is on me to demonstrate that its a good idea. I hope that I can some day rise to that challenge.
> The filesystem is a trusted entity on any OS design I'm familiar with
Thats not how capability based microkernels like SeL4 work. The filesystem is owned by a specialised process. Other processes only modify files by sending messages to the filesystem process via a capability handle. If nobody created a writable file handle, the file can't be arbitrarily mutated by another module. Copyfail happened because in linux, any code can by default interact with the page table. One piece of code was missing access control checks. In capability based systems, its basically impossible to accidentally forget access control checks like that.
> The only techniques we have to stop bugs like this are garbage collection or use of something like Rust's affine type system. You could in principle write a kernel in a language like C#, Java or Kotlin and it would be immune to these sorts of bugs.
Copyfail is a logic bug. C#, Java or Kotlin wouldn't save you from it at all.
The article talks about OS capabilities in the second part when it discusses Mojo, which is based on IPC.
> The solution is to design a language such that if I import leftpad, then call it, my computer can't get hacked.
That requirement may seem clear right now, but the moment you talk to other people about your language you'll find there's no agreement on what "get hacked" means. Some people will consider calling exit(0) repeatedly to be "hacked" because it's a DoS attack, others will say no code execution or priv escalation happened, so that's not being hacked. Some will say that left-pad being able to read arbitrary bytes from your address space is being hacked, others will say no harm done and thus it wasn't being hacked. The details matter and you need to nail them down in advance.
It turns out for example that one of the top uses of the Java SecurityManager was just to stop plugins accidentally calling System.exit() and tearing down the whole process. It wasn't even a security goal, really.
> You stop components tampering with each others' memory by using a memory safe language.
That's not enough. See languages like Ruby or JavaScript, which are memory safe but not sandboxable due to all the monkeypatching they allow.
> Haskell already passes a type object as an argument to anything which does IO. They don't do it for security. Turns out having pure functions separated from non-pure functions is a beautiful thing.
But almost nobody uses Haskell, partly because of poor ergonomics like this! So if you want a language that gets wide usage and has a good library ecosystem, monads for everything probably isn't going to take off.
> If nobody created a writable file handle, the file can't be arbitrarily mutated by another module.
We're talking about critical bugs in the filesystem so what the FS processes idea of a file handle is doesn't really matter. If you can confuse or buffer overflow the FS process by sending it messages, you can then edit state inside that process you weren't supposed to be able to access, and as that process controls the security system for everything it's game over. Microkernels have no way to stop this, which is one reason very few operating systems move the core FS out into a separate process. You can't easily survive a crash of the core FS code, and it being exploited is equivalent to an exploit of the core microkernel anyway in terms of adversarial goals. So you might as well just run it in-kernel and reap the performance benefits.
> > Haskell already passes a type object as an argument to anything which does IO. They don't do it for security. Turns out having pure functions separated from non-pure functions is a beautiful thing.
> But almost nobody uses Haskell
Sad, but true
> partly because of poor ergonomics like this!
I'm somewhat dubious that's the reason, partly because I find such ergonomic excellent! Especially those provided by my capability system Bluefin: https://hackage.haskell.org/package/bluefin