When one beyond-mainstream technology is not enough: Combining program verification with component-based architectures
Fuzzing. Bug bounties. ASLR. Code reviews. Despite the immense efforts put into improving the robustness of our software and the security of our systems, we don’t seem to make good progress here. Have a look at a recent update to your favorite smartphone OS. Every single month, dozens of flaws get fixed. But even more are still lurking in the code bases. Many of them allow for total system compromise. What is the reason that the situation does not seem to improve?
We argue that it’s the due to lacking approaches at the architecture level as well as the implementation level. Consequently, the problem has to be addressed at those two levels: Firstly, our systems need to be structured such that most complexity is in untrusted components which cannot affect system security. Secondly, for the much smaller trusted portions we need to establish formal correctness arguments.
In this talk, we present our approach to building trustworthy mobile OS. We combine the novel system architecture of the Genode OS framework with the SPARK technology for high-reliability applications.
This session is held on