Hi Nick,
then the own custom software components need not be licensed under GPL and need not make their code available; even if the underlying operating system used is licensed under the GPL, applications running on it are not considered derivative works.'
So in our case, we don't have an issue with GPL. Phew! :)
Your conclusion does actually not apply to Genode. The Linux kernel has an explicit clause at the top of its COPYING file that exempts user-level programs on top of Linux from being considered "derived work":
https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.git/tree/COPYING...
Genode has no such exemption clause. Such a clause would actually not make much sense because in Genode, most traditional in-kernel functionalities are separate programs. If we defined a license boundary around each program (as the Linux kernel does), this would correspond to defining a license boundary around each Linux kernel module. This would obviously undermine the spirit of the GPL.
The Genode framework is, for the most part, a collection of libraries, against which programs are linked when running on the platform. Because those libraries and interfaces are GPL software, programs using those libraries have to comply with the terms of the GPL. Put simply: Genode is Free Software. Software that is based on Genode should be Free Software, too.
If you intend to facilitate Genode to build a non-free software stack, commercial licensing should be investigated. This way, proprietary software built on top of Genode helps indirectly to bring Free Software forward by funding its development.
Best regards Norman