On 2/9/24, i...@wolffgames.com <i...@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. _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
