Hello Zachary,
thank you for sharing your work. Even though I'm not a Nix user myself, I can appreciate the work that went into nixpkgs-genode and the comprehensive documentation.
In my cursory research, I came across at least one past attempt at porting the Genode build system to Nix and vice versa (see [c]), as well as a mailing list discussion from almost a decade ago.
We originally got aware of Nix while working on Genode's 'ports' tool for the integration of 3rd-party code with Genode's build system [1].
[1] https://github.com/genodelabs/genode/issues/1082#issuecomment-36732457
The content-addressed directory names in contrib/ are inspired by it. Nix came up again a few years later when we started working on package management as a prerequisite for creating Sculpt OS. Nix was appealing for its feature to roll the system back/forward to any installed state and for the ability to use different package versions side by side. I remember Emery approaching the integration of Genode and Nix from several angles. But the complexity of those experiments went way over my head. Eventually, Christian and me went back to the drawing board and designed the simple depot structure we use today. Similar to Nix, it supports roll back/forward and the installation of different package versions side by side. But it forgoes the content addressing by using manually managed versions (i.e., release dates).
- Is anyone working on a build and/or runtime abstraction for system
composition?
Sculpt OS synthesizes the system composition of the runtime subsystem dynamically using C++ code. The sculpt manager merely consumes and produces XML. Here, the pkg/runtime files provide an abstraction that matches the needs of Sculpt (e.g., abstraction from the used kernel, file system, hardware devices etc.). Goa works on the same level of abstraction.
In similar spirit, there are quite a few test scenarios that follow the approach of using plain C++ for this purpose. Very little code [2] can create the suitable abstraction for executing a comprehensive test plan like [3].
[2] https://github.com/genodelabs/genode/blob/master/repos/os/src/test/init/main... [3] https://github.com/genodelabs/genode/blob/master/repos/os/recipes/raw/test-i...
- Is there any ongoing or planned work toward formal verification of
Genode components (e.g., core, init, etc.)?
The seL4 developers articulated Genode's use of C++ as a show stopper years ago.
Earlier this year, I got in touch with the company TrustInSoft, which offers (proprietary) static analysis tools for C++. Their analyzer is presumably able to prove the absence of memory-safety issues and other classes of vulnerabilities. Proofs of higher-level properties can in principle be pursued by using annotations similar to Ada/SPARK. The tools support C++20, which is the version used by Genode.
Personally, I find the prospect of analyzing Genode's code using these tools quite intriguing. Even though this idea remains intangible at this time, as a preparatory step into this direction, I'm currently striving to simplify and strengthen the code base of the base framework. E.g., removing Genode's dependency from the C++ support library [4].
[4] https://github.com/genodelabs/genode/issues/5245
Cheers Norman