research-article

Verifying security invariants in ExpressOS

Authors:

Samuel Talmadge King,

Parthasarathy MadhusudanAuthors Info & Claims

ACM SIGPLAN Notices, Volume 48, Issue 4

Pages 293 - 304

https://doi.org/10.1145/2499368.2451148

Published: 16 March 2013 Publication History

Abstract

Security for applications running on mobile devices is important. In this paper we present ExpressOS, a new OS for enabling high-assurance 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.

References

[1]

J. P. Anderson. Computer security technology planning study. Technical report, HQ Electronic Systems Division (AFSC), Oct. 1972. ESD-TR-73-51.

[2]

J. Andrus, C. Dall, A. Van't Hof, O. Laadan, and J. Nieh. Cells: A virtual mobile smartphone architecture. In Proceedings of the 23rd ACM Symposium on Operating System Principles, Cascais, Portugal, Oct. 2011.

Digital Library

[3]

M. Bellare, R. Canetti, and H. Krawczyk. Keying hash functions for message authentication. In Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, Santa Barbara, CA, Aug. 1996.

Digital Library

[4]

B. N. Bershad, S. Savage, P. Pardyak, E. G. Sirer, M. E. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility safety and performance in the SPIN operating system. In Proceedings of the 15th ACM Symposium on Operating Systems Principles, Copper Mountain, CO, Dec. 1995.

Digital Library

[5]

W. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15:1382--1396, 1989.

Digital Library

[6]

M. Castro, M. Costa, J.-P. Martin, M. Peinado, P. Akritidis, A. Donnelly, P. Barham, and R. Black. Fast byte-granularity software fault isolation. In Proceedings of the 22nd ACM Symposium on Operating System Principles, Big Sky, MT, Oct. 2009.

Digital Library

[7]

B. X. Chen and N. Bilton. Et tu, google? android apps can also secretly copy photos. http://bits.blogs.nytimes.com/2012/03/01/android-photos.

[8]

E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. VCC: A practical system for verifying concurrent C. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, Aug. 2009.

Digital Library

[9]

Common Vulnerabilities and Exposures (CVE). http://cve.mitre.org.

[10]

R. S. Cox, S. D. Gribble, H. M. Levy, and J. G. Hansen. A safety-oriented platform for web applications. In Proceedings of the 27th IEEE Symposium on Security and Privacy, Oakland, CA, May 2006.

Digital Library

[11]

J. Criswell, A. Lenharth, D. Dhurjati, and V. Adve. Secure virtual architecture: a safe execution environment for commodity operating systems. In Proceedings of the 21st ACM Symposium on Operating System Principles, Stevenson, WA, Oct. 2007.

Digital Library

[12]

L. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for Construction and Analysis of Systems, Budapest, Hungary, Mar. 2008.

Digital Library

[13]

W. Enck, P. Gilbert, B.-G. Chun, L. P. Cox, J. Jung, P. McDaniel, and A. N. Sheth. Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. In Proceedings of the 9th Symposium on Operating Systems Design and Implementation, Vancouver, BC, Canada, Oct. 2010.

Digital Library

[14]

R. J. Feiertag and P. G. Neumann. The foundations of a provably secure operating system (PSOS). In Proceedings of the 1979 National Computer Conference, New York City, NY, June 1979.

[15]

M. Golm, M. Felser, C. Wawersich, and J. Kleinöder. The JX operating system. In Proceedings of the USENIX 2002 Annual Technical Conference, Monterey, CA, June 2002.

Digital Library

[16]

M. Hohmuth and H. Tews. The VFiasco approach for a verified operating system. In Proceedings of the 19th European Conference on Object-Oriented Programming, Glasgow, UK, July 2005.

[17]

G. C. Hunt and J. R. Larus. Singularity: rethinking the software stack. ACM SIGOPS Operating Systems Review, 41(2):37--49, Apr. 2007.

Digital Library

[18]

G. Keizer. Google pulls 22 more malicious android apps from market. http://www.computerworld.com/s/article/9222595/Google_pulls_22_more_malicious_Android_apps_from_Market.

[19]

J. J. Kistler and M. Satyanarayanan. Disconnected operation in the Coda file system. ACM Transactions on Computer Systems, 10(1):3--25, Feb. 1992.

Digital Library

[20]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. seL4: formal verification of an OS kernel. In Proceedings of the 22nd ACM Symposium on Operating System Principles, Big Sky, MT, Oct. 2009.

Digital Library

[21]

M. Lange, S. Liebergeld, A. Lackorzynski, A. Warg, and M. Peter. L4Android: a generic operating system framework for secure smartphones. In Proceedings of the 1st ACM Workshop on Security and Privacy in Smartphones and Mobile devices, Chicago, IL, Oct. 2011.

Digital Library

[22]

K. R. M. Leino. Dafny: an automatic program verifier for functional correctness. In Proceedings of 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Dakar, Senegal, Apr. 2010.

Digital Library

[23]

F. Logozzo. Practical verification for the working programmer with codecontracts and abstract interpretation. In Proceedings of the 12th Conference on Verification, Model Checking and Abstract Interpretation, Austin, TX, Jan. 2011.

Digital Library

[24]

P. Madhusudan, X. Qiu, and A. Stefanescu. Recursive proofs for inductive tree data-structures. In Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Philadelphia, PA, Jan. 2012.

Digital Library

[25]

A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proceedings of the 16th ACM Symposium on Operating System Principles, Saint Malo, France, Oct. 1997.

Digital Library

[26]

T. Perrine, J. Codd, and B. Hardy. An overview of the kernelized secure operating system (KSOS). In Proceedings of the 7th DoD/NBS Computer Security Initiative Conference, Gaithersburg, MD, Sept. 1984.

[27]

X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan. Natural proofs for structure, data, and separation. Unpublished manuscript, 2012.

[28]

J. S. Shapiro, J. M. Smith, and D. J. Farber. EROS: a fast capability system. In Proceedings of the 17th ACM Symposium on Operating System Principles, Charleston, SC, Dec. 1999.

Digital Library

[29]

E. G. Sirer, W. de Bruijn, P. Reynolds, A. Shieh, K. Walsh, D. Williams, and F. B. Schneider. Logical attestation: an authorization architecture for trustworthy computing. In Proceedings of the 23rd ACM Symposium on Operating Systems Principles, Cascais, Portugal, Oct. 2011.

Digital Library

[30]

M. M. Swift, B. N. Bershad, and H. M. Levy. Improving the reliability of commodity operating systems. In Proceedings of the 19th ACM Symposium on Operating Systems Principles, Bolton Landing, NY, Oct. 2003.

Digital Library

[31]

J. Szefer and R. B. Lee. Architectural support for hypervisor-secure virtualization. In Proceedings of 17th International Conference on Architectural Support for Programming Languages and Operating Systems, London, England, UK, Mar. 2012.

Digital Library

[32]

S. Tang, H. Mai, and S. T. King. Trust and protection in the Illinois browser operating system. In Proceedings of the 9th Symposium on Operating Systems Design and Implementation, Vancouver, BC, Canada, Oct. 2010.

Digital Library

[33]

M. Tiwari, J. K. Oberg, X. Li, J. Valamehr, T. Levin, B. Hardekopf, R. Kastner, F. T. Chong, and T. Sherwood. Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security. In Proceedings of 38th International Symposium on Computer Architecture, San Jose, CA, June 2011.

Digital Library

[34]

H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In Proceedings of the 34th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Nice, France, Jan. 2007.

Digital Library

[35]

R. Wahbe, S. Lucco, T. E. Anderson, and S. L. Graham. Efficient software-based fault isolation. In Proceedings of the 14th ACM symposium on Operating Systems Principles, Asheville, NC, Dec. 1993.

Digital Library

[36]

B. J. Walker, R. A. Kemmerer, and G. J. Popek. Specification and verification of the UCLA Unix security kernel. Communications of the ACM, 23(2):118--131, Feb. 1980.

Digital Library

[37]

A. Whitaker, M. Shaw, and S. D. Gribble. Scale and performance in the Denali isolation kernel. In Proceedings of the 5th Symposium on Operating Systems Design and Implementation, Boston, MA, Dec. 2002.

Digital Library

[38]

J. Yang and C. Hawblitzel. Safe to the last instruction: automated verification of a type-safe operating system. In Proceedings of ACM SIGPLAN 2010 Conference on Programming Language Design and Implementation, Toronto, Ontario, Canada, June 2010.

Digital Library

[39]

E. Zadok, I. Badulescu, and A. Shender. Cryptfs: A stackable vnode level encryption file system. Technical report, Columbia University, June 1998. CUCS-021-98.

[40]

N. Zeldovich, S. Boyd-Wickizer, E. Kohler, and D. Mazières. Making information flow explicit in HiStar. In Proceedings of the 7th Symposium on Operating Systems Design and Implementation, Seattle, WA, Nov. 2006.

Digital Library

Cited By

Derakhshan FZhang ZVasudevan AJia L(2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00021
Haque ID’Souza DHabeeb PKundu ABabu G(2020)Verification of a Generative Separation KernelAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_17(305-322)Online publication date: 12-Oct-2020
https://doi.org/10.1007/978-3-030-59152-6_17
Shin JKim JHonoré WVanzetto HRadhakrishnan SBalakrishnan MShao Z(2019)WormSpaceProceedings of the ACM Symposium on Cloud Computing10.1145/3357223.3362739(299-311)Online publication date: 20-Nov-2019
https://dl.acm.org/doi/10.1145/3357223.3362739
Show More Cited By

Index Terms

Verifying security invariants in ExpressOS

Recommendations

Verifying security invariants in ExpressOS
ASPLOS '13: Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems

Security for applications running on mobile devices is important. In this paper we present ExpressOS, a new OS for enabling high-assurance applications to run on commodity mobile devices securely. Our main contributions are a new OS architecture and our ...
Verifying security invariants in ExpressOS
ASPLOS '13

Security for applications running on mobile devices is important. In this paper we present ExpressOS, a new OS for enabling high-assurance applications to run on commodity mobile devices securely. Our main contributions are a new OS architecture and our ...
Understanding the relationship between quality and security: a large-scale analysis of Android applications
SEAD '18: Proceedings of the 1st International Workshop on Security Awareness from Design to Deployment

Android applications (apps) are not immune to the problems which also plague conventional software including security vulnerabilities, quality defects, permission misuse, and numerous other issues. Many developers even intentionally create vulnerable or ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 48, Issue 4

ASPLOS '13

April 2013

540 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2499368

Issue’s Table of Contents

ASPLOS '13: Proceedings of the eighteenth international conference on Architectural support for programming languages and operating systems
March 2013
574 pages
ISBN:9781450318709
DOI:10.1145/2451116
General Chair:
Vivek Sarkar
Rice University, USA
,
Program Chair:
Rastislav Bodik
University of California, Berkeley, USA

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 March 2013

Published in SIGPLAN Volume 48, Issue 4

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

35
Total Citations
View Citations
616
Total Downloads

Downloads (Last 12 months)35
Downloads (Last 6 weeks)7

Reflects downloads up to 27 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Derakhshan FZhang ZVasudevan AJia L(2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00021
Haque ID’Souza DHabeeb PKundu ABabu G(2020)Verification of a Generative Separation KernelAutomated Technology for Verification and Analysis10.1007/978-3-030-59152-6_17(305-322)Online publication date: 12-Oct-2020
https://doi.org/10.1007/978-3-030-59152-6_17
Shin JKim JHonoré WVanzetto HRadhakrishnan SBalakrishnan MShao Z(2019)WormSpaceProceedings of the ACM Symposium on Cloud Computing10.1145/3357223.3362739(299-311)Online publication date: 20-Nov-2019
https://dl.acm.org/doi/10.1145/3357223.3362739
Neider DGarg PMadhusudan PSaha SPark D(2018)Invariant Synthesis for Incomplete Verification EnginesTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-319-89960-2_13(232-250)Online publication date: 12-Apr-2018
https://doi.org/10.1007/978-3-319-89960-2_13
Wang XChen DSun YWang XYao S(2014)Security Control for TVOSApplied Mechanics and Materials10.4028/www.scientific.net/AMM.643.136643(136-141)Online publication date: Sep-2014
https://doi.org/10.4028/www.scientific.net/AMM.643.136
Garg PLöding CMadhusudan PNeider D(2013)Learning Universally Quantified Invariants of Linear Data StructuresComputer Aided Verification10.1007/978-3-642-39799-8_57(813-829)Online publication date: 2013
https://doi.org/10.1007/978-3-642-39799-8_57
Garg PMadhusudan PParlato G(2013)Quantified Data Automata on Skinny Trees: An Abstract Domain for ListsStatic Analysis10.1007/978-3-642-38856-9_11(172-193)Online publication date: 2013
https://doi.org/10.1007/978-3-642-38856-9_11
Wu XTian DKim C(2023)Building GPU TEEs using CPU Secure Enclaves with GEVisorProceedings of the 2023 ACM Symposium on Cloud Computing10.1145/3620678.3624659(249-264)Online publication date: 30-Oct-2023
https://dl.acm.org/doi/10.1145/3620678.3624659
Zhou YGibson SCai SWinchell MParno BMeng WJensen CCremers CKirda E(2023)Galápagos: Developing Verified Low Level Cryptography on Heterogeneous HardwaresProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3616603(2113-2127)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3616603
Derakhshan FZhang ZVasudevan AJia L(2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00021
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents