On 23 Jun 2022, at 05:13, Isaac Beckett <isaactbeckett@gmail.commailto:isaactbeckett@gmail.com> wrote:

Hello, in your answer about camkes VMs, you mentioned a collaboration with DARPA on their SMACCM/HACMS project.

While seL4 is undoubtedly a good choice for mixed criticality systems like avionics on a UAV, I’m somewhat frustrated to hear y’all had done a contract for DARPA considering what they *use* those drones to do.

Is there somewhere I can read more in detail about this and other military-adjacent contracts?

In terms of technical content: https://trustworthy.systems/projects/TS/SMACCM/

We (the people who worked on these projects from the TS side) had the policy to accept and look for funding for work that is open source, including from defence. (In fact without that DARPA funding, it's unlikely that seL4 would be available open source now or have a community around it). We're not US citizens so can't work on US classified projects, which was a reasonable barrier for what kind of use we directly supported. (I'm using past tense here, because the community is now much larger and more diverse, and I don't know what other groups and companies do)

Of course all open source software can indirectly support anything. Pretty sure militaries around the world use a lot more Linux, BSD, networking stacks, encryption stacks, etc than they use seL4.

Personally, even for weapons systems, and even though I do not intend to work on any myself, I'd rather people have a dangerous weapons system that works as intended than one that has software bugs and uncontrolled behaviour. I'm not going to build such a system, but I'm fine accepting funding for work that makes everyone more able to build safer or more secure systems.

Cheers, Gerwin