SeL4 Question: Implementation of encrypted file types
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
Hello Marc, On 2024-02-09 20:14, info@wolffgames.com wrote:
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.
Would some of the "other things" be AI? Perchance training it via public mailing lists? No offence, but everything you said made no sense whatsoever and you sound like a deranged AI bot. I'll score it 2 out of 10, but only 1/10 if this was a hand picked message to send. Greetings, Indan
Hello, After some introspection, I sincerely apologise for my rude reply yesterday. I was tired and put off balance by all the discrepancies. I thought the message was a stupid prank by students or something and acted accordingly. Even so, that does not excuse my behaviour. I should have sent a polite private inquiry instead. I told Marc that to make up for it I will answer any technical questions he may have. Sorry for the noise, Indan
Thank you very much Indan, I appreciate the sincere apology. As for technical questions, I've provided a summary of my idea and would love to speak with someone from the dev team about it. I apologize for my amateur wording of everything, but please know I have absolutely zero intent to waste anyone's time and have contacted you because I think there is genuine merit to this idea. Perhaps if we could discuss this in a voice chat I could clarify easier, and clarifying questions could be asked. Please and thank you, Marc On 2024-02-11 02:23, Indan Zupancic wrote:
Hello,
After some introspection, I sincerely apologise for my rude reply yesterday.
I was tired and put off balance by all the discrepancies. I thought the message was a stupid prank by students or something and acted accordingly. Even so, that does not excuse my behaviour. I should have sent a polite private inquiry instead.
I told Marc that to make up for it I will answer any technical questions he may have.
Sorry for the noise,
Indan
On 2/9/24, info@wolffgames.com
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.
participants (3)
-
Andrew Warkentin -
Indan Zupancic -
info＠wolffgames.com