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...
Best regards, Marc
Marc Wolff Email: info@wolffgames.com Phone: 530.210.4811