Reimplement? Reuse? Both! — trustworthy systems with Genode and SPARK
Alexander Senier - Componolit
Formal verification is key to trustworthy systems. Especially when used for sensitive or critical applications. However, no matter which technology is used, the verification effort usually exceeds the costs for the actual implementation considerably. Hence, the verification of complex subsystems like device drivers, file systems or media codecs often is prohibitively expensive.
To improve on that situation for systems with confidentiality and integrity requirements, we realize component-based architectures based on the Genode OS framework. While we can reuse a lot of existing code, verified SPARK components maintain guarantees by wrapping, validating, sanitizing or resetting untrusted components. We present the different strategies and showcase their application to complex communication protocols using the example of the Componolit baseband filter. This SPARK component enables safe reuse of complex untrusted software by validating the interaction between Android and a radio communication processor.
About Alexander Senier
Alexander Senier is the founder and CEO of Componolit, a startup developing an open-source OS to run unmodified Android apps as well as critical IoT applications in a trustworthy environment. Since he started programming 25 years ago, he is in search of tools and technologies for creating better software. Consequently, he is interested in formal verification, microkernels and open-source software which he has used extensively in the past to build high-security systems.