On 23 Jan 2020, at 12:08, Andrew Warkentin mailto:andreww591@gmail.com> wrote: Speaking of unreleased code, the fact that there is any makes me worried that I may have to fork seL4 someday just because of the rather closed development process, which is a mismatch for the fully open, copyright-assignment-free development process (akin to that of the Linux kernel) that UX/RT will have. UX/RT is meant to be an OS for the real world and not yet another systems research project that is completely ignored outside academia. Therefore I am going to do everything I can to give it the best chance at real-world success, which includes a development model with as few barriers to contributing as possible. The experiments Gerwin refers to predate the open-sourcing of seL4. However, there is always going to be some in-house experimental code, especially student work, that never makes it out. We’re doing our best to make things more open, but we have very limited resources, resulting at times in a divergence between intent and reality. The forthcoming seL4 Foundation should help. Forking is a very bad idea. If you modify the kernel, you’re breaking verification, and it’s no longer seL4. And it will be one job of the Foundation to ensure that only things that *are* seL4 are called seL4. Gernot

On 23 Jan 2020, at 13:08, Demi M. Obenour wrote:

Would you be willing to accept PRs that include the corresponding changes to the proofs, or which don’t affect verification?

PRs that don’t affect verification will be accepted subject to standard quality control (and availability of a CLA). These are not frequent, but happen. Typically they are platform ports. One of the things we’d like to set up is a way for developers to check this for themselves, which should certainly help contributions. Not sure when this will be ready. The same applies, in principle, to PRs that come with proof updates. We haven’t seen one of these yet. The bar will be higher if the change affects kernel semantics (even if accompanied by proof), as we need to ensure that the design stays clean and principled. Gernot

On 23 Jan 2020, at 14:02, Heiser, Gernot (Data61, Kensington NSW) wrote:

On 23 Jan 2020, at 13:08, Demi M. Obenour mailto:demiobenour@gmail.com> wrote:

...

Would you be willing to accept PRs that include the corresponding changes to the proofs, or which don’t affect verification?

PRs that don’t affect verification will be accepted subject to standard quality control (and availability of a CLA). These are not frequent, but happen. Typically they are platform ports.

Because CLA sounds scary: Currently we still have the CLA process, but we’re hoping to move to something simpler and less legalistic in the future: a Developer Certificate of Origin [see e.g. https://julien.ponge.org/blog/developer-certificate-of-origin-versus-contrib... https://julien.ponge.org/blog/developer-certificate-of-origin-versus-contrib...].This is exactly the process that Linux uses for contributions. Cheers, Gerwin

Hi Andrew! I warn and apologize that this message is long; however I think there is a misconception at work here and I'd like to clear it up. At 2020-01-22T21:22:41-0700, Andrew Warkentin wrote:

On 1/22/20, Heiser, Gernot (Data61, Kensington NSW) wrote:

...

However, there is always going to be some in-house experimental code, especially student work, that never makes it out.

That's exactly the kind of thing that I think might be a problem for UX/RT because it means that the development process isn't truly community-based.

No, that's not what that means. Every FLOSS license, every Free Software license[1] permits private development. Experimental code is just that, and happens all the time in both professional and personal development environments. We all write toy programs or slapdash implementations to develop and verify our understanding of the systems we're creating or interfacing with. Or, frequently, to discover the undefined behavior of the C compiler we're using. :P Student projects are a case of this written large. Not everybody wants the code they write in their novice years to be unleashed upon the world. In the case of UNSW's AOS (Advanced Operating Systems) course[2], which is seL4-based, the students are discouraged from sharing their solutions to the project milestones because doing so would frustrate the educational objective of the course. That is, the course directors would have to redevelop it every term and that would make them unhappy; also, you'd eventually run out of well-understood operating system concepts with which to easily evaluate their solutions. Fortunately, since the AOS course builds _on top of_ instead of altering the seL4 kernel, this does create a GNU GPL section 7 problem[3]. 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. I'm not entirely comfortable citing my own reputation in the FLOSS community, but I have a public record as a strident FLOSS activist, particularly in the area of copyleft. You can find my fingerprints on the LaTeX Project Public License v1.3 per Frank Mittelbach, find me sparring with Richard Stallman over Invariant Sections and Cover Texts in the GNU FDL, find me exhorting David Dawes of the XFree86 Project not to slap a GPL-incompatible license over all of its (a decision he took anyway and which swiftly led to XFree86's death). I strove with "Gabucino" of the MPlayer project and Jörg Schilling of cdrtools to resolve GNU GPL incompatibilities within their codebases; the former attempt was ultimately successful while the latter was not. My most famous windmill-tilt was at Red Hat Software, Inc., for obfuscating the form of source distribution they used for the Linux kernel, presumably so as to impose an effort-tax on Oracle's Enterprise Linux efforts[4]. This last earned me (what I interpreted as) praise from Bradley M. Kuhn, who said I'm an even more strict interpreter of the GNU GPL than he is[5]. I also did FLOSS license-compliance work for several years professionally, in-house at Cisco.

UX/RT won't have any such thing as "in-house code" (except for code that hasn't yet been committed). All development will be public (except security fixes under temporary embargoes).

That is almost isomorphic (so, "cospectral"?) to what Trustworthy Systems does. Its developers push to internally-hosted Git repositories, upon which various continuous integration tests are run. If and only if the changed repos pass all the tests are the affected repositories then mirrored out to publicly hosted sites. This is quality control, and when the master branches of internal and external repos get out of sync it is a problem that the developers regard as urgent to fix.

I want UX/RT to be as easy as possible to contribute to, and that should include contributing to the kernel (which be much less necessary in general with a microkernel OS, but for stuff like platform support it will still be necessary).

Yes, and that is an objective shared by Trustworthy Systems.

Even just having a copyright-assignment-equivalent CLA would very likely scare off a lot of companies (and some individuals) from contributing. Things are already difficult enough in the industry at large for alternative OSes, and I don't want excessive barriers to contribution to be the thing that keeps UX/RT from succeeding.

That's true. Since the FSF (usually) requires copyright assignment as well, I can hardly cast stones at Trustworthy Systems for requiring this. I think CLAs come down to cases. Trustworthy Systems is part of Data61, which is in turn part of Australia's CSIRO. If you're American, that's sort of like the National Science Foundation. In organizations like these, a great deal of concern about liability exists. Such firms are regarded as having deep pockets (even when they don't), and so they attract civil suits in the hope of extracting a monetary settlement or judgment (the former is preferred, because the latter requires more billable hours in proving claims). However, I've gathered from encountering you on mailing lists over the past few years (no stalking, we simply seem to have similar interests :) ), that you're a lone developer working on a personal project. If you tried to impose a CLA on people I think you'd meet with a lot of resistance. And any contributor who valued their contribution would be pathologically selfless to assign copyright with no strings attached.

I really don't want to fork it unless I have to (and if I did I would rename my fork of course). I just know that my priorities for UX/RT (a general-purpose "better Linux than Linux" OS for production use) seem to be rather different from the those of the seL4 developers (research on static deeply embedded systems), and the development process isn't fully open, and that could possibly lead to differences requiring a fork in the future.

I think that if and when you can come to seL4 engineers at Trustworthy Systems with concrete use cases and measurable problems, they'll be happy to gnaw on the problem with you. It pays to remember that much of the staff are academics. Solving problems in microkernel performance and scalability, or showing how something once thought to be only achievable in a kernel can be done efficiently in user space, leads to conference papers and journal articles. They like that. I look forward to the continued development of UX/RT. Regards, Branden [1] https://www.gnu.org/philosophy/free-sw.html [2] https://www.cse.unsw.edu.au/~cs9242/current/ [3] https://www.gnu.org/licenses/old-licenses/gpl-2.0.en.html [4] https://lwn.net/Articles/432012/ [5] personal communication at DebConf 17 in Montréal, Canada

On 1/23/20, G. Branden Robinson wrote:

No, that's not what that means. Every FLOSS license, every Free Software license[1] permits private development.

Yes, I'm well aware that FOSS licenses permit private development by definition, and don't plan to release anything in UX/RT under a license that requires publication of changes (most of the first-party servers and commands will be under GPL2, and most libraries will be under MIT, BSD, or Apache licenses; anything derived from third party code will fully retain its original license).

Experimental code is just that, and happens all the time in both professional and personal development environments. We all write toy programs or slapdash implementations to develop and verify our understanding of the systems we're creating or interfacing with. Or, frequently, to discover the undefined behavior of the C compiler we're using. :P

Student projects are a case of this written large. Not everybody wants the code they write in their novice years to be unleashed upon the world. In the case of UNSW's AOS (Advanced Operating Systems) course[2], which is seL4-based, the students are discouraged from sharing their solutions to the project milestones because doing so would frustrate the educational objective of the course. That is, the course directors would have to redevelop it every term and that would make them unhappy; also, you'd eventually run out of well-understood operating system concepts with which to easily evaluate their solutions. Fortunately, since the AOS course builds _on top of_ instead of altering the seL4 kernel, this does create a GNU GPL section 7 problem[3].

That kind of thing is understandable.

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.

That is good to hear. I was worried that there was quite a bit of development going on behind closed doors.

However, I've gathered from encountering you on mailing lists over the past few years (no stalking, we simply seem to have similar interests :) ), that you're a lone developer working on a personal project. If you tried to impose a CLA on people I think you'd meet with a lot of resistance. And any contributor who valued their contribution would be pathologically selfless to assign copyright with no strings attached.

Yeah, it would be pretty much suicidal as an individual developer to impose a CLA on third-party contributions.

I think that if and when you can come to seL4 engineers at Trustworthy Systems with concrete use cases and measurable problems, they'll be happy to gnaw on the problem with you. It pays to remember that much of the staff are academics. Solving problems in microkernel performance and scalability, or showing how something once thought to be only achievable in a kernel can be done efficiently in user space, leads to conference papers and journal articles. They like that.

Yes, it's still quite early. Getting to real userspace is my only real priority at the moment, and I'm trying to avoid premature optimization. I probably won't bother to optimize all that much until it's capable of self-hosting. Once it's mature, I would like to see UX/RT become popular as a platform for research on OS subsystems and components, even though I'm intending it to be a production system and not a research system as such. I'd like to be able to incorporate such research into the mainline when it's reasonably possible. On 1/23/20, Klein, Gerwin (Data61, Kensington NSW) wrote:

Because CLA sounds scary: Currently we still have the CLA process, but we’re hoping to move to something simpler and less legalistic in the future: a Developer Certificate of Origin [see e.g. https://julien.ponge.org/blog/developer-certificate-of-origin-versus-contrib... https://julien.ponge.org/blog/developer-certificate-of-origin-versus-contrib...].This is exactly the process that Linux uses for contributions.

That sounds good. I'm planning to have a Linux-style DCO for UX/RT contributions once it's more established and there are other people contributing.

As an alternative to seL4_Untyped_RetypeAtOffset, would it maybe be possible to add an seL4_Untyped_Merge invocation that would take two adjacent untyped objects and a third slot for a destination and merge them into a single untyped, revoking the original two untypeds, and an seL4_Untyped_Replace invocation that would be similar to seL4_Untyped_Retype except that it would revoke the original untyped (failing if called on an initial untyped object). These would allow almost comparable optimizations to seL4_Untyped_RetypeAtOffset (although some "filler" untyped objects for free blocks would still have to be created). Could these be implemented without a searchable CDT? Would they be any easier to verify?

On 26 Jan 2020, at 12:55, Andrew Warkentin wrote:

Actually, it would probably be better to make seL4_Untyped_Replace take a parent untyped capability and a child capability (of any type) of that untyped to revoke and replace. That would allow replacing an object any number of times.

Still not quite sure I understand correctly what seL4_Untyped_Replace would do. The description above sounds like the following: - c_u: a cap to an untyped - c_o: a cap to an object retyped from that untyped, i.e. c_u is the direct parent of c_o - you want a retype operation that is equivalent to: - revoke c_o - delete c_o. There is now a hole in somewhere in the space covered by c_u. - retype a new object of equal or smaller size into the space made available by that hole If I got that right, then this operation could be a bit harder to verify than the merge operation, but probably not much. We’d probably eliminate the revoke again and put that in user space, but you’d still be left with reasoning about a potentially long-running delete, followed by a retype. The retype would be justified by knowing that we have just reclaimed that area of memory and the only other authority to it is the untyped and its parents. This is a bit different to the reasoning we have so far for knowing that an area of memory is unused (and also not pointed to by any other kernel objects). The usual reasoning goes from invariants about untypeds without children, which wouldn’t quite fit here. The proof here could probably still re-use most of that reasoning, but it would need a bit more digging to be sure it doesn’t blow out into a long project. To be able to make use of the result of that free-space reasoning, the end of the delete would have to be atomic with the beginning of the retype, otherwise the authorising untyped could disappear during the call. That should be reasonably easy inside the kernel. In terms of kernel design, this one is harder to justify to the minimality principle, because you could achieve the same effect with the additional untyped cap that I think you were mentioning before, i.e. between c_u and c_o, have a cap c_u2 of the size that is needed for c_o, and revoke/retype that one (which also neatly covers what could go wrong if the authorising cap disappears, e.g. because some overlord server revoked everything — the kernel would catch that at invocation time of the in-between untyped). Given the size of most objects, one untyped cap per object sounds like not too bad of an overhead, but of course this also means managing the relationship between these untypeds and the object caps. Cheers, Gerwin

On 28 Jan 2020, at 14:56, Andrew Warkentin wrote:

On 1/27/20, Klein, Gerwin (Data61, Kensington NSW) wrote:

...

Thinking through confidentiality, integrity, availability, and capDL theorems this also sounds fine, if you present both untyped caps, you are not gaining more authority by merging them. capDL can probably not express the operation (it doesn’t have the information wether two untypeds are adjacent) but doesn’t really need to, since you wouldn’t run it in system initialisation.

capDL limitations won't be an issue for UX/RT since it won't use capDL at all (the only user code in common with CAmkES will be libsel4, with the other low-level code being Rust-based and derived from feL4 and Robigalia). Kernel capabilities will just be treated as a supervisor implementation detail and not exposed to applications at all (only the root server and the low-level system library will deal with kernel objects directly). File descriptors and mapping descriptors (identifying a specific mapping of a file) will be the only true capabilities that normal user programs see (they will be wrappers for groups of kernel capabilities). There will also be process file permissions that will be capability-like in that they can be transferred securely between processes, but unlike true capabilities will not serve as identifiers. These will be the main security mechanism, since they will be more compatible with Unix software than a pure capability model.

I wouldn't think that they'd be an issue for CAmkES either since it probably wouldn't ever need to merge any untyped objects. Not sure about Genode, but AFAIK it uses its own XML-based capability definition language everywhere rather than using capDL, and it treats untyped objects as an implementation detail much like UX/RT.

Yes, I think capDL will not be a problem. The non-expressiveness would take the form of non-determinism, i.e. when you call the merge operation, the capDL state would non-deterministically fail or perform the operation, you just can’t predict which one it does. This means you only have to deal with it if you use capDL and if you use that operation in capDL, for which I can’t see a real use case. System description and system initialisation would still work as before.

...

Still not quite sure I understand correctly what seL4_Untyped_Replace would do. The description above sounds like the following:

- c_u: a cap to an untyped - c_o: a cap to an object retyped from that untyped, i.e. c_u is the direct parent of c_o - you want a retype operation that is equivalent to: - revoke c_o - delete c_o. There is now a hole in somewhere in the space covered by c_u. - retype a new object of equal or smaller size into the space made available by that hole

Yes, that's exactly what I meant.

Got it.

...

In terms of kernel design, this one is harder to justify to the minimality principle, because you could achieve the same effect with the additional untyped cap that I think you were mentioning before, i.e. between c_u and c_o, have a cap c_u2 of the size that is needed for c_o, and revoke/retype that one (which also neatly covers what could go wrong if the authorising cap disappears, e.g. because some overlord server revoked everything — the kernel would catch that at invocation time of the in-between untyped).

UX/RT won't have to deal with issues relating to revocation of the parent untyped, since only the root server will deal with untyped objects and it will only ever use one copy of each untyped capability, although that could be a problem for other OSes with a more recursive architecture.

This one is slightly different to the expressiveness for capDL. For expressiveness the context/use case matters, but the atomicity here is a case of security/correctness, which would have to work in all contexts. I.e. it would probably be fine in UX/RT by design, but if the feature could be abused elsewhere to break the security of the kernel, we could not include it. This specific one is not really such a big issue, though, it could be enforced easily in the kernel, it just caught my attention because the security reasoning is a bit more subtle there than usual.

...

Given the size of most objects, one untyped cap per object sounds like not too bad of an overhead, but of course this also means managing the relationship between these untypeds and the object caps.

It's still more overhead than the Linux kernel's buddy allocator, which uses bitmaps to track free blocks, rather than having to use some kind of associative array. I know that some use of associative arrays is probably unavoidable (at least with the allocator design I'm using), but it would be nice to have as few capabilities as possible so as much as possible can be tracked with bitmaps.

In this I should really defer to the kernel design experts, since I'm more the verification side. Compared to the searchable CDT it would certainly be a much simpler operation, and maybe the trade-off for performance (memory overhead, speed, and complexity) is worth it. It would basically be the properly implemented replacement of the Recycle operation the API used to have in the very beginning, but that we had to drop because it had too many surprising corner cases to be actually useful (it allowed you to reset an object to a neutral state -- the idea was that it would be as if it had been deleted and retyped, but that wasn’t really the case in the end). Cheers, Gerwin

I’m happy to help with the process and description. I’m offline for the rest of the week, but should be able to spend some time on it next week. Cheers, Gerwin On 29 Jan 2020, at 19:38, Heiser, Gernot (Data61, Kensington NSW) mailto:Gernot.Heiser@data61.csiro.au> wrote: Hi Andrew, Something along the lines of what you are proposing might make sense and might be doable at reasonable cost. I propose you use our (so far heavily under-utilised) RfC process https://docs.sel4.systems/RfcProcess.html for the proposal. Please provide a detailed motivation, including convincing use cases, and a detailed description of the proposed functionality and how it interacts with existing functionality. Gernot On 28 Jan 2020, at 15:26, Andrew Warkentin mailto:andreww591@gmail.com> wrote: On 1/27/20, Klein, Gerwin (Data61, Kensington NSW) mailto:Gerwin.Klein@data61.csiro.au> wrote: Thinking through confidentiality, integrity, availability, and capDL theorems this also sounds fine, if you present both untyped caps, you are not gaining more authority by merging them. capDL can probably not express the operation (it doesn’t have the information wether two untypeds are adjacent) but doesn’t really need to, since you wouldn’t run it in system initialisation. capDL limitations won't be an issue for UX/RT since it won't use capDL at all (the only user code in common with CAmkES will be libsel4, with the other low-level code being Rust-based and derived from feL4 and Robigalia). Kernel capabilities will just be treated as a supervisor implementation detail and not exposed to applications at all (only the root server and the low-level system library will deal with kernel objects directly). File descriptors and mapping descriptors (identifying a specific mapping of a file) will be the only true capabilities that normal user programs see (they will be wrappers for groups of kernel capabilities). There will also be process file permissions that will be capability-like in that they can be transferred securely between processes, but unlike true capabilities will not serve as identifiers. These will be the main security mechanism, since they will be more compatible with Unix software than a pure capability model. I wouldn't think that they'd be an issue for CAmkES either since it probably wouldn't ever need to merge any untyped objects. Not sure about Genode, but AFAIK it uses its own XML-based capability definition language everywhere rather than using capDL, and it treats untyped objects as an implementation detail much like UX/RT. In total probably 6-8 weeks of verification work. You likely would want to tweak the operation such that user space does the revocation in a separate syscall to avoid reasoning about preemption in the new operation. Yes, requiring the user process to revoke the capability first would probably actually make more sense. On 1/27/20, Klein, Gerwin (Data61, Kensington NSW) mailto:Gerwin.Klein@data61.csiro.au> wrote: Still not quite sure I understand correctly what seL4_Untyped_Replace would do. The description above sounds like the following: - c_u: a cap to an untyped - c_o: a cap to an object retyped from that untyped, i.e. c_u is the direct parent of c_o - you want a retype operation that is equivalent to: - revoke c_o - delete c_o. There is now a hole in somewhere in the space covered by c_u. - retype a new object of equal or smaller size into the space made available by that hole Yes, that's exactly what I meant. In terms of kernel design, this one is harder to justify to the minimality principle, because you could achieve the same effect with the additional untyped cap that I think you were mentioning before, i.e. between c_u and c_o, have a cap c_u2 of the size that is needed for c_o, and revoke/retype that one (which also neatly covers what could go wrong if the authorising cap disappears, e.g. because some overlord server revoked everything — the kernel would catch that at invocation time of the in-between untyped). UX/RT won't have to deal with issues relating to revocation of the parent untyped, since only the root server will deal with untyped objects and it will only ever use one copy of each untyped capability, although that could be a problem for other OSes with a more recursive architecture. Given the size of most objects, one untyped cap per object sounds like not too bad of an overhead, but of course this also means managing the relationship between these untypeds and the object caps. It's still more overhead than the Linux kernel's buddy allocator, which uses bitmaps to track free blocks, rather than having to use some kind of associative array. I know that some use of associative arrays is probably unavoidable (at least with the allocator design I'm using), but it would be nice to have as few capabilities as possible so as much as possible can be tracked with bitmaps. _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel