Haohui Mai
Skip Abstract Section
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.
- J. P. Anderson. Computer security technology planning study. Technical report, HQ Electronic Systems Division (AFSC), Oct. 1972. ESD-TR-73-51.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- W. Bevier. Kit: A study in operating system verification. IEEE Transactions on Software Engineering, 15:1382--1396, 1989. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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. Google ScholarDigital Library
- Common Vulnerabilities and Exposures (CVE). http://cve.mitre.org.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.Google Scholar
- G. C. Hunt and J. R. Larus. Singularity: rethinking the software stack. ACM SIGOPS Operating Systems Review, 41(2):37--49, Apr. 2007. Google ScholarDigital Library
- 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.Google Scholar
- J. J. Kistler and M. Satyanarayanan. Disconnected operation in the Coda file system. ACM Transactions on Computer Systems, 10(1):3--25, Feb. 1992. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- X. Qiu, P. Garg, A. Stefanescu, and P. Madhusudan. Natural proofs for structure, data, and separation. Unpublished manuscript, 2012.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- E. Zadok, I. Badulescu, and A. Shender. Cryptfs: A stackable vnode level encryption file system. Technical report, Columbia University, June 1998. CUCS-021-98.Google Scholar
- 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. Google ScholarDigital Library
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 systemsSecurity 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 '13Security 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 ...
Taint flow analysis to improve Android application security
The current generation, adults and children of all ages, have come to know and love the smartphone. Everywhere you look, a majority of people will have a smartphone in hand. The entirety of one's life is on his or her device - contacts, pictures, ...
Comments