I'm a community organizer for WASI https://wasi.dev/, a post-POSIX runtime with features that I think make it suitable for SeL4's planned post-POSIX runtime:
* Fast and fine grained SFI via WASM. * Fast IPC and capability oriented security via WASM Reference Types https://github.com/WebAssembly/reference-types/blob/master/proposals/reference-types/Overview.md . * High level interoperability across programming languages via WASI Interface Types https://hacks.mozilla.org/2019/08/webassembly-interface-types/ and shared garbage collection https://github.com/WebAssembly/gc/blob/master/proposals/gc/Overview.md. * Wide range of targets: embedded, TEE, blockchain, browser, server, and (eventually) consumer operating systems.
Industry cooperation is happening through the Bytecode Alliance https://bytecodealliance.org/, with partners like Red Hat ensuring commercial viability [1 https://github.com/bytecodealliance/wasmtime/issues/70#issuecomment-477329267 , 2 https://github.com/bytecodealliance/wasmtime/issues/71#issuecomment-518006644]. Fastly is already using it for their serverless offering https://www.youtube.com/watch?v=QdWaQOgvd-g, which can scale to 20K processes/machine with a 35.4 microsecond cold start time.
However, I believe the project would benefit *greatly* from the SeL4 community's experience architecting high-performance/high-assurance microkernels, IPC, and capability based security models.
SOIL https://soil-initiative.org/ is an academic effort to foster cross-pollination through biweekly seminars https://soil-initiative.org/seminar/. *We are seeking presenters from the SeL4 to better understand your needs and potential areas of collaboration*. Please contact Ross Tate (ross@cs.cornell.edu) if you are interested in presenting and jump on our Zulip Channel https://bytecodealliance.zulipchat.com/ if you have any questions!
Thank you, -Zach Lym