Re: MirageOS and my recent involvement

[Thomas Gazagnaire <thomas@xxxxxxxxxxxxxx>]

Dear Hannes,

> I have some exciting MirageOS related news that I find worth sharing, and 
> hope to engage discussions by doing so. Maybe it is also worth to restart 
> weekly / biweekly MirageOS meetings (as in the old days) -- what do you think?

I think that’s a great idea to restart bi-weekly MirageOS meetings. There are 
many projects that are going on, it would be great to sync more regularly. 
Should we start early January?

> Some repositories in the mirage organization are suffering from bitrot, 
> and/or lack of cleanups or reviews (such as the ocaml-solo5 PR waiting since 
> a long time for proper reviews that would enable to use OCaml 5) -- my 
> personal experience with OCaml 5 from a resource perspective is not very 
> good, that's why I don't really care about that too much (and am happy that 
> 4.14 is under long-term support).

Do you have some reproducible case for the OCaml5 resource usage? 5.1.1 is 
shipping with a few improvements and it would be great to see if that fixes 
what you have observed.

> ## uTCP
> 
> Since August I've motivated myself to work a bit more on uTCP, a TCP/IP stack 
> that originated from Netsem, a formal model in HOL4.
> 
> […]

As we already have discussed offline, I’m quite excited by seeing progress on 
that new implementation as having a robust, verified and extendable TCP stack 
is super important. I’m also curious to compare the performance with the 
previous stack.

> ## NetHSM
> 
> The first (to my knowledge) commercial product using MirageOS (and Muen) is 
> now for sale; it is a "Hardware Security Module", so something you can store 
> your private keys which hopefully never get extracted. With the robur team 
> (namely Steffi and Martin) I was involved in the early days (doing system 
> design and implementation) [though I've not followed changes in later years]. 
> See their announcement at 
> https://www.nitrokey.com/news/2023/after-8-years-development-nethsm-10-available-first-open-source-hardware-security-module

That’s indeed probably the first commercial projects to use Solo5. However, 
that’s not the only one using the library part of the "library operating 
systems" approach. For instance, the network stack (mirage-tcpip (UDP/TCP), 
charrrua (NTP/DNS), cohttp) is used widely (dozen of millions of users) to 
translate all the container raw traffic into host syscalls in Docker for 
Desktop since 2016 :-) As you pointed out in your blog, the stack mostly handle 
well-formed traffic (that has been generated by the Linux kernel) but it’s 
pretty solid and flexible. Happy to see if we can swap it with uTCP when this 
is ready.

Best,
Thomas