On 2/9/24, info@wolffgames.com info@wolffgames.com wrote:
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.
Processors with fully generic microcode are very uncommon (off the top of my head the most recent I can think of are Transmeta's CPUs from the 2000s, and possibly the Russian Elbrus 2000 family), and AFAIK are rather tricky to get decent performance out of.
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.
As a pure microkernel, seL4 knows absolutely nothing about file systems or executable formats (unless you want to count the embedded ELF loader for the root task on x86). The only functionality present in the kernel is multitasking, inter-task messaging, and low-level memory management (this optionally includes support for CPU virtualization extensions).
Transformation of file formats would be done in some kind of user-level server on seL4 or any other pure microkernel. There's no security or performance reason to include this kind of thing in the kernel.
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?
This kind of protection would normally be done with trusted execution extensions (like TrustZone on ARM). There's no need for custom microcode support or somehow trying to run seL4 on a GPU.