Greetings SeL4 Development,
My name is Marc Wolff, currently located in Portland, Oregon, USA.
I'm CEO of Leyline Nexus, an R&D team primarily for game development,
but also some other things.
I have an implementation question for the SeL4 microkernel, and I was
hoping you could point me in the right direction. Unfortunately I'm not
a computer scientist and my knowledge is both self-taught and currently
very limited. Right now we're focused on tabletop games, but our next
development target is video games and hardware development.
I see based on what I can understand from the whitesheet that SeL4 can
hypervise, but I'm wondering about an idea to fully secure it on the
hardware side, essentially solving one its primarily vulnerabilities.
The basic idea starts with a modified risc-based CPU architecture on an
FPGA (since x86 is compromised) for testing. This includes a
microcode-embedded SeL4 mk with an added feature for encrypting a NEW
SYSTEM of FILE TYPES.
Here, all files types become a system-specific encrypted file type which
presents a virtual (more common) file type externally for readability,
e.g. ".doc" or ".exe". I suppose this would be at -0 privilage, since
it happens in microcode and the processs would not be accessible through
ASM instructions, except through dedicated query ports and flag
registers. The result is that the system comes up with its own hidden
and encrypted name, for example, for the .exe file type. I guess it
could do this for any arbitrary file name, so long as its source code
could be validated by the hyperviser (possibly modified?; it would have
to do this both at runtime when executing code and when compiling).
When compiling files, if the microkernel discovers exploits in the code
(invalid requests, etc.), then it can simply compile it as the standard
file type that could run on other systems (.exe) but not on this system
- since this system only reads its own encrypted file types. If there's
an existing standard output for invalid programs in SeL4 then this could
modify that or be added to it for certain cases.
I suppose this would entirely depend on the quality of encryption, save
for reverse-engineering through decapping or something, but it seems
like a potential solution for fully separating virtual memory from
runtime execution. I definitely DO NOT know what I'm talking about, but
from my perspective this seemed like a great way to implement copyright
protection on game hardware SOC's. Maybe on the FPGA you could even do
a sub-GPU within a microkernel core that was dedicated to encrypting?
Maybe someone has already thought of all this before?
If yes, we'd be very interested to know - as it could save us a lot of
time and headaches...