On 11/18/20 10:44 PM, Gernot Heiser wrote:
Dear seL4 Community,
Those who attended today’s closing session at the seL4 Summit have heard about this, for the rest I’m pleased to announce that we have an RFC out for the seL4 Core Platform, a minimal seL4-based OS for embedded/cyberphysical/IoT applications, see https://sel4.atlassian.net/browse/RFC-5
Feedback welcome.
Gernot
I hope it is okay for me to respond here, as opposed to on JIRA, but if you prefer the latter, just let me know and I will comment there. The design document appears to be well-written, and gives a good explanation of what the seL4 Core Platform is. That said, there are two ways I believe it could be improved. The first is an explanation for why the restrictions stated are acceptable. For instance, it is clear that the targeted systems are static. Why is dynamism not required? Is it because these systems are created with a single purpose in mind, and so do not need the level of extensibility that a dynamic system offers? The second is the ability to forcibly reset a protection domain to its initial state. For instance, a printer might have a PostScript interpreter and a PDF rasterizer. Both of these have been major sources of vulnerabilities in the past, and are of such complexity that reimplementation may not be viable. Instead, the untrusted rendering code can run in its own protection domain. After a print job has been processed, the renderer is forcibly reset, preventing any attack from harming other jobs. This feature can also be used to recover from a crash of an individual component, without having to reboot the entire system. Sincerely, Demi