TY - GEN
T1 - Verifying security invariants in expressOS
AU - Edgar, Haohui Mai
AU - Xue, Pek Hui
AU - King, Samuel T.
AU - Madhusudan, P.
PY - 2013
Y1 - 2013
N2 - 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. Categories and Subject Descriptors D.4.6 [Operating Systems]: Security and Protection; D.2.4 [Software Engineering]: Software/ Program Verification General Terms Security, Verification.
AB - 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. Categories and Subject Descriptors D.4.6 [Operating Systems]: Security and Protection; D.2.4 [Software Engineering]: Software/ Program Verification General Terms Security, Verification.
KW - Automatic theorem proving
KW - Microkernel
KW - Mobile security
KW - Programming by contracts
UR - http://www.scopus.com/inward/record.url?scp=84875660204&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84875660204&partnerID=8YFLogxK
U2 - 10.1145/2451116.2451148
DO - 10.1145/2451116.2451148
M3 - Conference contribution
AN - SCOPUS:84875660204
SN - 9781450318709
T3 - International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS
SP - 293
EP - 303
BT - ASPLOS 2013 - 18th International Conference on Architectural Support for Programming Languages and Operating Systems
T2 - 18th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2013
Y2 - 16 March 2013 through 20 March 2013
ER -