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).
2. 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.cc
[3]
https://github.com/genodelabs/genode/blob/master/repos/os/recipes/raw/test-init/test-init.config
3. 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
--
Dr.-Ing. Norman Feske
Genode Labs
https://www.genode-labs.com · https://genode.org
Genode Labs GmbH · Amtsgericht Dresden · HRB 28424 · Sitz Dresden
Geschäftsführer: Dr.-Ing. Norman Feske, Christian Helmuth
_______________________________________________
users mailing list -- users@lists.genode.org
To unsubscribe send an email to users-le...@lists.genode.org
Archived at
https://lists.genode.org/mailman3/hyperkitty/list/users@lists.genode.org/message/FLP66FX6SQ7AJV3273FQJVRXMRZDAZ5Y/
