RFC-25: Add post-initialiser to Microkit

[terryzbai]

This RFC proposes a new component type: post-initialiser for the ACPI/PCIe initialisation.

[lsf37]

So this look still very draft-y and needs cleanup (people tend to ignore things that do not look ready for discussion), but I like the idea of allowing the violation of the basic setup assumptions only at initialisation time. That lines up with what we do for the initialiser already. I have a few minor complaints about details, depth and precision of the argument that I will comment on in the PR diff, but the basic idea to me has no major verification problems, is consistent with the design and achieves what is (apparently) needed. (One of my complaints is that the motivation is not expressed clearly).

I'll try to type out why and how the shared CNode feature violates verification assumptions and what impact that would have. Something along those lines should become part of the RFC so that the reasoning is better documented. No need to copy my words, but you are allowed to if you want to.

My main complaint is that alternatives are just listed, but not evaluated. The point of this section is rationale. What are the reasons we are favouring the proposed design over the alternatives? Some look obvious, others do not.

[lsf37]

The reason shared CSpaces break confinement and integrity

Take-Grant

The seL4 capability model is based on the ideas of the take-grant access control model, developed by Jones, Lipton, and Snyder (according to this paper, although the original paper is by Lipton and Snyder'77). The model consists of a graph with nodes (think of kernel objects) and edges that are capabilities. In addition to the standard read/write permissions, it introduces grant which allows you to transfer a capability (and the symmetric take, which seL4 does not implement). The basic question this access control model can answer is "will node X ever be able to perform action A on node Y?". The idea is simple: take the transitive symmetric closure of all grant nodes connected to X. This gives you a set of nodes. Assuming each node has grant authority to itself, any access right in that set of nodes can eventually be used by any of the other nodes in the set. If the entire set does not have a capability to node Y that allows action A, then we statically can answer the question above with "no".

seL4 extends the take grant model in various ways. In particular it adds create (untyped capabilities), store (CNodes), and control (TCB caps and other capabilities that essentially give you full control over the execution of another thread). Relevant to the discussion here is store. While it may be possible to build more constrained setups in seL4, in general, in the abstraction we have to assume that if two nodes have store right to the same CNode (i.e. they posses a CNode cap to it), that this is equivalent to grant in both directions, because either side can put one of its existing capabilities into that node and the other can invoke it.

Authority confinement

Instead of explicitly modelling the transitive closure the authority confinement part of the seL4 integrity theorem models this situation by assigning a label to each kernel and memory object. One can think of the label as the set of kernel objects related to a user-level component (or a protection domain in Microkit). If the capabilities that are collectively contained in that label satisfy certain constraints, then that label is stable, i.e. it can never gain additional authority to other labels in the future over what it already has (this models the transitive closure). Following from the explanation of store above, one of these rules comes out to the fact that if an object in label X has a capability to a CNode, then that CNode must be in label X. Similarly, if label X has a grant authority to an object, that object also has to be in label X. For integrity, these consistency rules only need to be true for the current subject (loosely, the current thread), that is, for the part of the execution that the integrity theorem is applied to. For the information flow theorem, it has to apply to all threads.

How this relates to Microkit

The original Microkit design and RFC fit these constraints perfectly -- Microkit protection domains line up easily with integrity labels, and the integrity theorems is applicable to any protection domain without needing to reason about user behaviour or anything else apart from internal Microkit setup correctness, discharged in large parts by the capDL initialiser.

What we get from the integrity theorem is that the fundamental assumptions that user-level verifications want to make are true: code is stable and does not change at runtime, if a page is not explicitly shared, its contents only depend on what the current PD did, not on what the rest of the system did (i.e. they behave like normal models of sequential memory), if a PD exists now it will still exist after a syscall has been made, etc. This is also what we use to justify the use of formal verification methods that do not directly or fully integrate with the formal seL4 model. They have value, because they a) can assume their models of execution are coherent and related to reality mostly in the way they were designed, and b) the properties we get out of these verifications have some meaning that we can use to plug into the behaviour of the verification of other components. That is, even though there is still hand-waving about all of this fitting together and making any sense, the hand waving has an actual rigorous formal basis and can be reasoned about in isolation.

Impact

The impact of sharing a CNode between two protection domains is that the integrity theorem will now force us to assign the same label to the two components that share the CNode. This means they can no longer be reasoned about in isolation. In particular, they cannot be reasoned about in a sequential model, because the fundamental assumption that memory will be private and preserved came from the integrity theorem that is not longer available to these two components. This is the setting this initialisation phase will need to be verified in, and there are no current tools that achieve this in the seL4 context. Using this for all PDs would mean there is no formal basis any more for any of the user-level verification we have been doing. As the RFC says, making the feature available to users and then saying "do not use it, because it breaks the system" is not a useful policy for a framework whose main argument for existence is that it makes it easy to build systems that are verifiable and securely partitioned by default.

Couldn't we make it more precise?

There was a particular argument in a separate forum that I would like to replicate here, because it is relevant: it may well be possible to set up a shared CNode in seL4 such that it does not have to be equivalent to a two-sided grant permission. While I'm not yet convinced that you actually can and there is no way of circumventing it, let us assume for discussion that there was such a way: first of all, it would not solve the problem this RFC is aiming to solve (actual resource and authority transfer between two components -- this means there is not only effective, but actual transfer of authority going on). Second, this still breaks things in the same way as above, simply because the integrity theorem does not contain this case.

We could start a research project on whether there is a way to model the precise setup under which read-only CNode sharing would be stable and allowed and not lead to label collapse, but it would very likely have to constrain the other assumptions of the setup even more. For instance, the integrity theorem currently allows for a label to have all rights to itself. That is an assumption that makes the integrity proof feasible in the first place -- local reflexivity of the authority graph together with transitivity (and symmetry which follows from the other two) produce very nice formal properties that the take-grant reasoning relies on. So we would likely need to give up on that entire way of reasoning and take a different approach that hard-codes properties the Microkit setup has (e.g. more locked-down protection domains than current integrity requires). So while it does sound possible to change the reasoning, the most likely price is a loss of generality. In particular, the current integrity theorem is well suited to generalise to dynamic system, where trusted management components do not make use of integrity, but the rest of the system does. Encoding things such as "a label only has the CSpace capability in its TCB slot, but not an addressable capability to its own CNodes in its CSpace" would very likely rule out such systems. That is not a price worth paying if there are alternative solutions.

[lsf37]

We do generally want full names for the RFCs. If there is a problem with that, we can discuss.

[lsf37]

It is not fully clear to me if this is an accurate summary of below. We seem to be declaring multiple PDs? (for post-initialisation). I'm also hazy on what the phases mean exactly. Do they declare a sequential execution oder of a set of PDs? And everything else that is not declared implicitly runs only after?

If that is the intent, how does it interact with Microkit's current init phase? (not the capDL initialiser, but the component init code) Should post-initialisation be an official part of that init phase instead? This would avoid the additional concept of post initialisation and "just" give more structure to the initialisation phase in general. Might just be a renaming of concepts.

[midnightveil]

The Microkit PD's init() function is not run in an init-phase, it's really just a function that's run, there's no guarantee that all PD's init() run befores any other code. It's possible that that should be not be the case (but often init() needs to do blocking IO before a component is ready...)

I'll let Terry comment on the other aspect here.

[lsf37]

So the post-initialisation phase would be running before init() of the normal PDs runs?

[terryzbai]

It is not fully clear to me if this is an accurate summary of below. We seem to be declaring multiple PDs? (for post-initialisation). I'm also hazy on what the phases mean exactly. Do they declare a sequential execution oder of a set of PDs? And everything else that is not declared implicitly runs only after?

A post-initialiser might need to be executed after its dependencies are ready, e.g., the PCIe driver needs the extracted resource configurations and the corresponding capabilities from the ACPI driver. Therefore, on single core, the sequential execution model is the simplest way to schedule the post-initialisers if there are no cyclic dependencies. The idea was to have the parameter phase to declare the execution order for simplicity.

So the post-initialisation phase would be running before init() of the normal PDs runs?

Yes, the drawback here is that all the PDs would have to wait all the post-initialisers to be done, even if some of PDs are not dependent on any post-initialiser.

Ideally, independent post-initialisers can be parallelly executed on different cores, and a normal PD can start once its dependent post-initialisers complete.

Also, the ACPI AML has mutex operations for concurrent interpretation specifically, so the ACPI driver has the potential to be multi-threaded for performance. (not sure if we should consider this atm)

If that is the intent, how does it interact with Microkit's current init phase? (not the capDL initialiser, but the component init code) Should post-initialisation be an official part of that init phase instead? This would avoid the additional concept of post initialisation and "just" give more structure to the initialisation phase in general. Might just be a renaming of concepts.

A post-initialiser should be a different type of (non-?)protected domains which have its own programming model, probably just a main() function if we can make sure the notification is not necessary. But it still needs a subset of features from normal PDs, such as shared memory regions.

I think making post-initialisation a part of PD's initialisation phase does not help constrain the capability transfer among components but significantly increase the trusted computing base of each PD.

[lsf37]

This assertion "have to figure things out by interacting with the ACPI tables possibly located anywhere in memory" is not actually true. There are plenty of current x86 systems that do not do this and work fine. For instance, you can boot the system once, figure out what resources there are and then statically specify them.

The real motivation (I think, I might be wrong) is that we want a single unchanged piece of software to run on any x86 system. That is a departure from the design principle that one should know what system one is building for, and it has a few consequences beyond this RFC (i.e. are we aiming for more changes in this direction or not).

Personally I'm Ok with making that departure, it makes sense for x86 (it is very awkward not to) and maybe it will make sense for AArch64 in the future as well, but this is the thing that really changes and that the @seL4/tsc should be thinking about.

[midnightveil]

The real motivation (I think, I might be wrong) is that we want a single unchanged piece of software to run on any x86 system.

Yes.

For instance, you can boot the system once, figure out what resources there are and then statically specify them

Yes, this is strictly speaking, possible, but it is really annoying (minor changes to BIOS versions or placement of cards physically can change things); Peter also says that sometimes the locations can change on every boot.

Personally I'm Ok with making that departure, it makes sense for x86 (it is very awkward not to) and maybe it will make sense for AArch64 in the future as well,

Yes, one of the designs that I think could have been discussed further in the evaluation is whether or not we could make the capDL initialiser do all of this. It's possible that it would make sense to make capDL spec specify PCI deviceId + vendorID instead of bus:dev.func. ACPI is a harder sell because it requires an entire AML interpreter.

[lsf37]

I don't think the capDL initialiser as it is now is a good place to do this, but one design that this suggests is that there could be a separate phase of the capDL initialiser or some kind of plugin system where the capDL initialiser theorem holds for the state just before any custom phases are running.

The main drawback to running more code in the capDL initialiser is that this initialiser is the root task with full authority over the entire system. The principle of least privilege would suggest that authority should be dropped to just what is necessary to do this ACPI task. So maybe the CSpace of the initialiser could be swapped out before this phase runs, so that it is then constrained. This would need no change in Microkit and would make that kind of boot phase available to other kinds of systems as well.

It's very similar to the post initialisation idea, just in a different framework.

It would be a bit fiddly to correctly place this in the capDL init flow. It should probably run before other threads can run, but after the distribution theorem holds. So we'd be missing that one final step (threads start) of the current theorem if we use it, but that's not a complex or failure prone step, so I think that would be fine.

[terryzbai]

Zoltan proposed another similar idea that the post-initialiser threads are created and executed sequentially by the capDL initialiser, so each post-initialiser would have the minimum set of capabilities to finish its job. One of the difficulties is that we will need a sort of interfaces to dynamically declare required resources for next post-initialiser, e.g., the ACPI driver tells the capDL initialiser what the PCIe driver needs for its configurations. Surely, we can also integrate the ACPI and PCIe drivers together, but I prefer to have a generic solution for the users to define custom boot phases tasks.

[lsf37]

Surely it does not need access to all remaining untypeds? That could be enormous amounts of memory. I can understand that it may need a statically unknown amount of memory, though.

This is a separate issue for the capDL initialiser: "give all remaining untypeds" to some CSpace is not a declarative statement about the initial state of the system, it's a procedural interpretation of how the initialiser works. Not sure we need a full separate RFC for this, but it does need discussion on how that should be expressed statically and what it means formally. I.e. what is the correctness property that you want to hold after the initialiser is done with this? Just "this set of CNode slots contains only untyped caps that are distinct from other untyped caps in the system"?

Is an initialiser that just gives you 0 or 1 of them correct or incorrect? Does it have to be all that are mentioned in boot info? How do you know how many of these will be needed for the other objects? What if you haven't provided enough slots? Is the initialiser supposed to dynamically create more CNodes? Where do the caps go for those? What if the initialiser just fills as many as it can? Is that correct? What if those are not enough for your system? Most of these are probably not so hard to answer, but they should have an answer.

[terryzbai]

Surely it does not need access to all remaining untypeds?

The ACPI tables should be located on device-type memory, and the intermediate paging structures of elf image can be reused for table mapping, so ideally no normal untypeds are required.

This is a separate issue for the capDL initialiser: "give all remaining untypeds" to some CSpace is not a declarative statement about the initial state of the system, it's a procedural interpretation of how the initialiser works.

yes, I have been thinking about this and prefer to have more thoughts from the verification people.

Is an initialiser that just gives you 0 or 1 of them correct or incorrect? Does it have to be all that are mentioned in boot info? How do you know how many of these will be needed for the other objects?

For the ACPI driver specifically, it would be very complex to evaluate. The AML has almost all of what we have in a high-level programming language, such as variables (NameOp/FieldOp), functions (MethodOp), algorithmic and logical operators. This means the data that we extract from the tables can change due to different function invocation (called method evaluation in AML) order. It sometimes needs to read physical registers on ECAM or other MMIO to complete the calculation, making it unlikely to justified statically.

In this case, returning 0 can only tell that the capabilities are available regarding to extracted resource configurations, but cannot tell if the interpretation is correct or not.

How do you know how many of these will be needed for the other objects? What if you haven't provided enough slots? Is the initialiser supposed to dynamically create more CNodes? Where do the caps go for those? What if the initialiser just fills as many as it can? Is that correct? What if those are not enough for your system? Most of these are probably not so hard to answer, but they should have an answer.

ye, all of these also confused me. This should be solvable if the post-initialisers are created and executed by the capDL initialiser.

[lsf37]

This should be replaced by text about what the verification problem is so that the RFC is self contained.

[lsf37]

This is very specific to the example you are thinking about right now. The RFC should be proposing a general mechanism. One that also solves your current need, of course, but one that makes sense in more than strictly one situation. So this shouldn't be motivated by "this driver does this", but by what is a good design in general.

Do we need everything to be sequential in phases in such a generalised initialisation phase or should these two drivers implement the phasing amongst themselves with notifications? I.e. should it be framework or implementation?

Are there other situations we can think of where phasing is particularly good/natural or some where it is bad? What if we're doing multicore? Do we want other components to be doing their own initialisation while this is going on or do we want the framework to be able to allow/prevent that or to always prevent that?

[terryzbai]

Do we need everything to be sequential in phases in such a generalised initialisation phase or should these two drivers implement the phasing amongst themselves with notifications? I.e. should it be framework or implementation?

As I mentioned in another comment, a directed dependency model might be more proper when we consider on multi-core cases.

The primary issue is that I still cannot come up with other use cases to generalise the solution. A clock/pinmux driver is expected to dynamically adjust the hardware as requested at run time.

[lsf37]

An RFC shouldn't be a story of what happened but a description of a desired design and its rationale. Please rephrase as that. I think the idea is good. Not entirely clear if post-initialisation should be part of initialisation or not. (Maybe not, IIRC communication is not supposed to happen during initialisation, so maybe the component init phase is not the right place)

[terryzbai]

it refers to the post-initialisation phase of the whole system, i.e. after the capDL initialiser, rather than the initialisation phase of a PD.

[lsf37]

Does this define a PD? Or is it just a thread? What VSpace would it get?

[terryzbai]

It should be a thread but also wants a small subset of features of PDs. It should has its own VSpace, which will be released after the post-initialiser completes.

[lsf37]

When you say "for centralised resource allocation and configurations", what does that mean exactly? Does the PCIe driver consist of multiple components? Does it have to hand out resources to other parts of the system or does it remain a single central component for anything PCIe related?

[terryzbai]

The PCIe driver aims to allocate memory regions and I/O Ports from the resource window, which is handed off by the ACPI driver. The resource window of each device (including PCIe bus) on hardware is written on the ACPI tables by the firmware. Interrupt routing information of I/O APIC is also formatted in the ACPI tables.

[lsf37]

Should be rephrased a bit, but I understand that this is saying the cnode feature is only available to the post init phases. 👍

[lsf37]

Is it required that this is linear? E.g. pos-initialiser phase and the rest could run interleaved/concurrent. Not sure if that is a good idea, but I think we should have rationale on why the design is this way and what pro/con aspects we have considered. The RFC text will serve as documentation in the future for why things are the way they are, in particular to document what we have thought about and what not. If a new idea comes along we want to know if it is actually new or if it was considered and rejected (and why).

[lsf37]

I do think this needs to be resolved in this discussion. It doesn't have to be a final unchangeable solution, i.e. with more experience we might go back and change it, but we need to decide on one design now and document why we thought it is the way to go.

[lsf37]

This section should define the full syntax and meaning for the new feature, ideally as it will appear in the manual. An "includes" list is not enough.

[lsf37]

The planned layout of the differences should be specified.

[lsf37]

What would be an alternative/tweak to this design that makes a generalisation later easy? I'm not sure what exactly template PDs are, and if they will spark joy, but if you already have something in mind and future change can easily be reduced by more thinking now, then that seems worth doing. (But if template PDs need shared CNodes, then they do break the Microkit design, so maybe it is better if they do not fit).

[lsf37]

In terms of principle of least privilege, it is better if such code runs in an already authority-constrained environment. Then at least it can be verified without needing to preserve invariants about the entire rest of the system (e.g. in the loader about what it has done to kernel code, memory, page tables etc).

So from that perspective, I think the design proposed here is strictly better.

In terms of implementation, doing this before the kernel loads might be the simplest option. But doing everything in privileged mode is always the simplest option, i.e. that doesn't mean we should do it.

[lsf37]

It should of course only pass 1 capability per call, and do that in a loop. I'm not sure there is any substantive difference to the shared CNode feature, apart that it is easier to break the authority link temporally. I.e. after the cap transfer via grant is done, the grant right can be removed (or even the entire endpoint cap), and the components are from then on separate according to authority confinement.

(Edit: I'm not necessarily pushing for this alternative. If shared CNodes are easier or the same, we can just do that, but it's not clear to me that it is in fact easier or better, so we should not just dismiss it)

This reminds me: the RFC does currently not describe what happens to the post-initialisation non-PDs after they are finished. Are they inert? How do we show that? Does the monitor explicitly kill everything that should no longer run? Can/should their resources be reclaimed? (probably not in a static system).

[midnightveil]

(Right, transferCaps only ever does 1 cap, even though seL4_MsgMaxExtraCaps implies one could do more. That's weird).

[lsf37]

(Discussion ongoing in a separate comment thread). If done right, this may actually be not a bad option either.

[terryzbai]

Thanks for the patience and insightful comments. Like many questions you mentioned above, I had already thought about them but didn't get clear answer yet, so just made a very draft-y RFC for more input from the community.

I will try to progress on the remaining issues.