Hello Genodians,
I have spent the last few months familiarizing myself with the base API and creating some sample projects. While I am relatively new to Genode, I had a few ideas during my initial exploration for areas to which I might contribute.
[1] When I was just starting out, my biggest challenge was the build system. While going through some of the basic examples / demos, I developed a rather simplistic Nix wrapper around the Genode build system (see [a]). Despite its simplicity, it greatly sped up my development time. For those that aren't familiar, Nix is a language for creating reproducible builds (see [b]). I was able to get several of my co-workers spun up on my projects in a single command. Since Nix has a docker image, creating development container images for those that did not already have Nix was trivial. I think there is a lot of potential here for decreasing the barrier to entry for playing with Genode demo scenarios, and generally making Genode builds more reproducible.
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 (see [d]). Has anyone continued these efforts? If no one is currently working on this, would it be something that others would be interested in using? I have my own ideas for how I would implement this, but I would like to get input from more experienced members of the community.
[2] I also want to ask about system composition abstractions. XML ROMs make sense as a runtime representation since they are easy to parse, but they make it difficult to write complex system configurations by hand. Are there any current efforts to create build and/or runtime abstractions for system composition? From my naive perspective, this also seems like a wonderful place to introduce a high-level package manager to create and deploy modular subsystems (if one doesn't already exist). I also wonder if there are any opportunities here for formal modelling and analysis of a configuration.
[3] Finally, I want to ask about any previous or planned work to formally verify the correctness of important Genode components (e.g, core, init) and the Genode API. Are there any challenges that make this infeasible? There are several follow-up questions I would have before going in this direction, but I would once again like to get input before adding my thoughts.
To summarize: 1. Has anyone been working on porting Genode to Nix (or vice versa)? 2. Is anyone working on a build and/or runtime abstraction for system composition? 3. Is there any ongoing or planned work toward formal verification of Genode components (e.g., core, init, etc.)?
I look forward to hearing everyone's thoughts!
Best, Zachary Zollers
[a] https://github.com/zgzollers/nixpkgs-genode [b] https://nixos.org/ [c] https://discourse.nixos.org/t/genodepkgs-extending-nixpkgs-nixos-to-genode/8... [d] https://lists.genode.org/mailman3/hyperkitty/list/users@lists.genode.org/mes...
Hi Zachary,
I have spent the last few months familiarizing myself with the base API and creating some sample projects. While I am relatively new to Genode, I had a few ideas during my initial exploration for areas to which I might contribute.
"First contact" is an interesting time, rich in impressions and creative suggestions indeed, as (I think) Norman has noted in the past, noting the need to encourage well-thought feedback from "fresh eyes".
Genode demo scenarios, and generally making Genode builds more reproducible.
Newbie-level question about the reproducible build concept: is it about making sure people using different build platforms/OS will still end up creating byte-for-byte identical binaries (so long as they build from the exact same source of course), so that one may "trust" a binary build just by comparing it with an upstream one ? Or is it about something else entirely ?
- Is anyone working on a build and/or runtime abstraction for system
composition?
I've seen several opinions on this between both extremes (change nothing/overhaul-all). I took the middle road with my perforce jam/mr build system that could be described as just "reducing the boilerplate a little", or maybe as "refactoring xml config creation a bit".. It's very spepcific to my project so might not serve as inspiration much or at all for other projects... Even on the (hypothetical) day when I'll finally clean it up and make it decent-looking *g*.
That jam-based system does work wonders for me in several ways, but I still find myself inefficient sometimes when dealing with routing sessions and such, so I'll keep an eye out watching for possible developments in the future, coming from genodians or the Genode team. To be honest, difficulties I face are due more to my brain being slow to 'grok' some thing, or simply making the same mistakes over and over again :-). But, imagining that later on something comes up that is useful both to newbies learning the ropes, *and* supposed experienced devs like me who are still slow on the intake (several years in), then why not ! This might not be a high priority item for the community currently, but sometimes a breakthrough is made even on things that were believed to be "not low hanging fruit/not worth the time" :-)
- Is there any ongoing or planned work toward formal verification of Genode
components (e.g., core, init, etc.)?
I seem to remember the Genode team experimenting with the Spark language a few years back, for one specific component, which would have allowed (IIRC) formal correctness checking of that component, and (if the concept worked well) could have been extended to others, but eventually abandoning that venue and sticking with C++. www.genodians.org should have it.
Also remember breathing a sigh of relief for selfish purposes (I have to build the toolchain from scratch, and building GCC is a lot of work already, without adding more on top) but feeling guilt about that sentiment *g*
Cedric
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
-
Norman Feske -
ttcoder＠netcourrier.com -
Zachary Zollers