ExpressOS

ExpressOS is a high assurance OS architecture that enforces high level security invariants to improve the security of mobile application, where the enforcement has been formally verified.

ExpressOS is able to run non-trivial, unmodified Android application like web browsers. Thanks to its novel architecture, and automatic verification techiques including Dafny and code contracts, the verification effort on security invariants is low enough to be pragmatically feasible.

The ASPLOS'13 paper contains more technical information of the design and implementaiton of ExpressOS.

This repository holds the kernel of ExpressOS. The project also holds the instructions of building and using ExpressOS.

The source code is under the UIUC BSD open source license.

This research was funded in part by AFOSR MURI grant FA9550-09-01-0539, ONR grant N000141210552, NSF grant CCF-1018182, and supported by Intel through the ISTC for Secure Computing.