ABOUT THIS PROJECT
Many of our OSes are built on less than assured architectures and may contain a bloated codebase that is good for hiding backdoors and software bugs. These bugs and backdoors can be kept undiscovered in a huge codebase (> 50K LOCs) and are very tedious and difficult to attempt a proper code review or to map the code logic to rigorous mathematical equations for proofing the code's trustworthiness, security and resilience to faults.
In this project, the Genode Framework has been explicitly chosen to be used as the basic building block to due to it's flexibility in integrating many well known Open Source microkernels into it's array of supported build combinations. It also offers a trusted GUI interface called the Nitpicker that would allow users to securely interact with multiple instances (called as "scenarios" in Genode's terminology). This project would host a blog that would include first hand experiences in using the Genode Framework and sample commands learnt from first hand experiences while attempting to build a usable trusted microkernel booting a common OS to simulate a real world scenario.
The starting build option would be using a 32 bit Intel architecture build as it's CPU core, the Fiasco.OC microkernel and the L4Linux as the real world OS instance (scenario) sitting above the microkernel. We will attempt to simulate a scenario on a QEMU environment before gradually increasing it's complexity to the point where the trusted system could be booted off a bare metal 32 bit Intel chip with loaded application scenarios that allows a user to readily interact with the environment.
By following the instructions and suggestions in this research and/or to use the resources provided in this research, you hereby agree that you are using the information and resources at your own risk and ASKG.INFO nor the researchers, publishers or committers are to be held liable in any circumstances that may arise from such usage.