I've been thinking a bit again about modern type systems with respect to operating system design and I think I can describe heuristically some of my old ideas and the open questions I still have. If there are comments or ideas, I'd love to hear them.
I like modern type systems. I also like capabilities. How can we combine them together? I used to think I had more solid leads on this question, but now I feel a little shaky. What I wanted to do was have a set of capabilities, essentially just indexes into some resource mapping in the kernel, be attached to each process. The actual access rights for each resource would be encoded as a phantom type in the capability. So for each resource type you'd have some set of operations that would have preconditions about the phantom types they would find acceptable. If you wanted to pass a capability to another process you can use provided functions for making a copy securely, giving any level of permissions less than or equivalent to your own.
Now there are some things that I think make sense here: the more we can shove questions of safety into the type system, the less we have to do at runtime and the better scalability you can have. Also, I think it encourages a very different UI experience. To see a resource you need to have a capability to it, but if you're dispatching over the type of capability then presumably you could do something like have the only shell commands available for that resource be the ones that match the type signature of the resource. I'm not sure how to actually implement a feature like that, but it seems like it should be feasible on a moral level.
I feel like there's three questions I have to answer in order to take the idea from "oh that's kinda cute" to something real. The first problem is bootstrapping and snapshotting of the OS. I haven't even begun to think about this, honestly.
Another issue is how the process and system call model would have to work. We'd want the system calls to be somehow typechecked for proper capability use. Again, I'm not sure of a good scheme for this that doesn't restrict execution to just the host language. Perhaps the bullet that has to be bitten involves making some form of FFI for each compiler that should target this system so that the system calls are made in the host language and then type checked at compilation.
The last issue that's still fuzzy in my head involves storing capabilities for a process. Now, it's all fine and dandy to say 'it's a set', but most data structures in a language such as Haskell are homogenous. What I need is a heterogenous container that doesn't completly lose type information, which means that using type classes and existentials is right out. I know Oleg Kiselyov has done work with thing like HList, but that's something I don't know much about.
Subscribe to:
Post Comments (Atom)
4 comments:
From what I can tell, a capability is a run-time thing. It's a nature that values in the system have.
To type-check this, you need to properly lift values up to the type level. You and I both know what that means.
So if you're stuck on using a Haskell like type system, I recommend leaving the phantom types as truly phantom, so that the Haskell typechecker can at least prove that compositions of core combinators are correct.
Then you'd have a minimal set of unsafe injectors to lift naked values up to this level to strip all that away at run-time.
If you want to prove anything more sophisticated, you should be looking at proof assistants you can tie to Haskell (or whatever) to avoid repeating the specifics of your capabilities system. The details of how the capabilities work would need to live in the proof assistant and the OS run-time in this scenario.
Am I way off the mark on this? You know more about these topics than I.
Capabilities should be truly linear IMO-- if you give another process a capability, you should lose it. There shouldn't be a way to copy capabilities. Actually, I would probably be in favor of a system where you can't give away capabilities at all.
@Antoine
Well, the kernel is what initially creates a capability from a resource so there are already necessarily functions to do so, they just aren't accessible by anything that isn't the core, trusted code.
I'm not sure if I know what you mean by "leave the phantom types truly phantom".
@jeff
I can understand the idea of not copying capabilities, but how could you ever share files, memory segments, etc. if you couldn't pass a capability at all?
It seems like if you wanted to share something between two processes, both processes should need to independently acquire a capability for said resource.
Post a Comment