Alexander Senier

With 2.5 billions of active users Android is the most widely deployed mobile operating system in the world. Its vast complexity paired with a monolithic architecture regularly result in severe security issues like the infamous Stagefright bug. In this presentation we talk about an ongoing research project which aims at running Android applications on top of the component-based Genode OS framework and secure them using formally verified components. We discuss how Android applications interact, how well this matches the semantics of Genode and what it takes to support unmodified Android apps.

Google tracks you even with location service disabled. Your smartphone can be taken over remotely via WiFi. Opening media files remains an (unpredictable risk)[https://en.wikipedia.org/wiki/Stagefright_(bug)]. Despite all the effort put into mitigation techniques we don't seem to make good progress with the privacy and security of our mobile devices.

We present our vision of Componolit, an open-source platform for trustworthy mobile devices. Based on the Genode OS framework, the component-based system will provide strict isolation between apps, services and drivers. The platform will enable users to run arbitrary unmodified Android apps without giving up control of their devices. This is realized by trustworthy policy objects implemented and formally proven in the SPARK language.