Verifying security invariants in expressoS

Haohui Mai, Edgar Pek, Hui Xue, Samuel T. King, P. Madhusudan

Research output: Contribution to journalArticlepeer-review


Security for applications running on mobile devices is important. In this paper we present ExpressOS, a new OS for enabling highassurance applications to run on commodity mobile devices securely. Our main contributions are a new OS architecture and our use of formal methods for proving key security invariants about our implementation. In our use of formal methods, we focus solely on proving that our OS implements our security invariants correctly, rather than striving for full functional correctness, requiring significantly less verification effort while still proving the security relevant aspects of our system. We built ExpressOS, analyzed its security, and tested its performance. Our evaluation shows that the performance of ExpressOS is comparable to an Android-based system. In one test, we ran the same web browser on ExpressOS and on an Android-based system, and found that ExpressOS adds 16% overhead on average to the page load latency time for nine popular web sites.

Original languageEnglish (US)
Pages (from-to)293-303
Number of pages11
JournalACM SIGPLAN Notices
Issue number4
StatePublished - Apr 2013


  • Automatic theorem proving
  • Microkernel
  • Mobile security
  • Programming by contracts

ASJC Scopus subject areas

  • Computer Science(all)


Dive into the research topics of 'Verifying security invariants in expressoS'. Together they form a unique fingerprint.

Cite this