Verifying Security Invariants in ExpressOS

Provided by: Association for Computing Machinery
Topic: Hardware
Format: PDF
Security for applications running on mobile devices is important. In this paper, the authors present ExpressOS, a new OS for enabling high-assurance applications to run on commodity mobile devices securely. Their main contributions are a new OS architecture and their use of formal methods for proving key security invariants about their implementation. In their use of formal methods, they focus solely on proving that their OS implements their security invariants correctly, rather than striving for full functional correctness, requiring significantly less verification effort while still proving the security relevant aspects of their system. They built ExpressOS, analyzed its security, and tested its performance. Their evaluation shows that the performance of ExpressOS is comparable to an Android-based system.

Find By Topic