Since Branden explicitly invoked me:
On 23 Jan 2020, at 19:56, G. Branden Robinson g.branden.robinson@gmail.com wrote:
If you're thinking of skunkworks-style projects, or secret modules that get released only to paying customers, then Gernot can answer with certainty but I can tell you that I've neither seen nor heard of any such thing in the year I've worked at the Trustworthy Systems Group; that proprietary work product is opposed to the mission of the lab as I understand it; and that such a thing is not congruent with the workplace culture and opinions of staff.
What Branden says is totally correct, including the cultural part.
I can categorically say that there are no privately-distributed kernel versions (at least not by us, and if someone else does it tey are breaking the law). What goes out is public. The GPL on seL4 applies to us as well.
This doesn’t stop us from having internal experimental versions, mostly student work, which is kept in-house for the reasons Branden outlined. But also because if we create a public branch with experimental features, this is bound to create an expectation out there that whatever we’re experimenting with will eventually make it into mainline. There are cases that are too speculative for this.
Things are a bit less strict for userland code and tools. These are mostly under BSD licenses, so we could have special versions. We do not normally do this, and even under contract will normally only produce code that is destined for release (where the release may have to go through an external approval process, but we're trying to avoid that too).
Sometimes there are projects where we work with an external partner on enabling real-world use, our string of DARPA projects are examples. In such cases we strive to work only on components that are of general use and will (eventually) be publicly released, and leave the project/customer-specific code to the partners as much as possible, so we can release everything *we* produce. There are rare exceptions where we need to keep something we write a private deliverable owned by the customer. These cases are rare, almost always are code that is of little value to someone else, or a special case of a more general solution we’ll re-implement (and release) concurrently or soon after.
These qualifications, “eventually” and the “rare exceptions” may not satisfy all purists, but they come down to a judgement of what is overall best for the community. If we can get funding for developing some significant pieces of code that will be beneficial to the community, and the price is that we end up writing an extra 5% that is kept by the customer, then we will probably go for it. This is always a case-by-case decision, and in the rare cases where this happened, we were quite satisfied that the decision was in the best interest of the seL4 ecosystem.
When someone approaches us for a project, we make this position clear early on, and sometimes the conversation ends there, but this is rare.
Bottom line is that we aren’t a body shop, we’re about making seL4 ubiquitous.
Gernot