Abstract
Current web browsers are complex, have enormous trusted computing bases, and provide attackers with easy access to computer systems. This makes web browser security a difficult issue that increases in importance as more and more applications move to the web. Our approach for this challenge is to design and build a correct-by-construction web browser, called IBOS, that consists of multiple concurrent components, with a small required trusted computing base. We give a formal specification of the design of this secure-by-construction web browser in rewriting logic. We use formal verification of that specification to prove the desired security properties of the IBOS design, including the address bar correctness and the same-origin policy.
This work was done while the first author was at the University of Illinois.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Akhawe, D., Barth, A., Lam, P.E., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: Proceedings of the 2010, 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pp. 290–304. IEEE Computer Society, Washington, DC (2010)
Barth, A., Jackson, C., Reis, C., The Google Chrome Team: The security architecture of the chromium browser (2008), http://crypto.stanford.edu/websec/chromium/chromium-security-architecture.pdf
Chen, S., Meseguer, J., Sasse, R., Wang, H.J., Wang, Y.-M.: A systematic approach to uncover security flaws in GUI logic. In: IEEE Symposium on Security and Privacy, pp. 71–85. IEEE Computer Society (2007)
Chen, S., Ross, D., Wang, Y.-M.: An analysis of browser domain-isolation bugs and a light-weight transparent defense mechanism. In: Ning, P., di Vimercati, S.D.C., Syverson, P.F. (eds.) ACM Conference on Computer and Communications Security, pp. 2–11. ACM (2007)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Google Inc. Chromium OS (2010), http://www.chromium.org/chromium-os
Grier, C., Tang, S., King, S.T.: Secure web browsing with the OP web browser. In: Proceedings of the 2008 IEEE Symposium on Security and Privacy, pp. 402–416 (May 2008)
Heiser, G., Ryzhyk, L., Von Tessin, M., Budzynowski, A.: What if you could actually trust your kernel? In: Proceedings of the 13th USENIX Conference on Hot Topics in Operating Systems, HotOS 2013, pp. 27–27. USENIX Association, Berkeley (2011)
Klein, G., Andronick, J., Elphinstone, K., Heiser, G., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an operating-system kernel. Commun. ACM 53(6), 107–115 (2010)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Moshchuk, A., Bragin, T., Gribble, S.D., Levy, H.M.: A crawler-based study of spyware on the web. In: Proceedings of the 2006 Network and Distributed System Security Symposium (NDSS) (February 2006)
Provos, N., Mavrommatis, P., Rajab, M.A., Monrose, F.: All your iFRAMEs point to us. In: Proceedings of the 17th Usenix Security Symposium, pp. 1–15 (July 2008)
Provos, N., McNamee, D., Mavrommatis, P., Wang, K., Modadugu, N.: The ghost in the browser: Analysis of Web-based malware. In: Proceedings of the 2007 Workshop on Hot Topics in Understanding Botnets (HotBots) (April 2007)
Rosu, G., Stefanescu, A.: Matching logic: a new program verification approach. In: Taylor, R.N., Gall, H., Medvidovic, N. (eds.) ICSE, pp. 868–871. ACM (2011)
Sasse, R.: Security Models in Rewriting Logic for Cryptographic Protocols and Browsers. PhD thesis, University of Illinois at Urbana-Champaign (July 2012), Current Draft available at http://hdl.handle.net/2142/34373
Symantec. Symantec internet security threat report (2011), http://www.symantec.com/business/threatreport
Tang, S., Mai, H., King, S.T.: Trust and protection in the illinois browser operating system. In: Arpaci-Dusseau, R.H., Chen, B. (eds.) OSDI, pp. 17–32. USENIX Association (2010)
TeReSe (ed.): Term Rewriting Systems. Cambridge University Press (2003)
Wang, H.J., Grier, C., Moshchuk, A., King, S.T., Choudhury, P., Venter, H.: The multi-principal OS construction of the Gazelle web browser. In: Proceedings of the 2009 USENIX Security Symposium (August 2009)
Wang, Y.-M., Beck, D., Jiang, X., Roussev, R., Verbowski, C., Chen, S., King, S.: Automated Web Patrol with Strider HoneyMonkeys: Finding Web sites that exploit browser vulnerabilities. In: Proceedings of the 2006 Network and Distributed System Security Symposium (NDSS) (February 2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sasse, R., King, S.T., Meseguer, J., Tang, S. (2013). IBOS: A Correct-By-Construction Modular Browser. In: Păsăreanu, C.S., Salaün, G. (eds) Formal Aspects of Component Software. FACS 2012. Lecture Notes in Computer Science, vol 7684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35861-6_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-35861-6_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35860-9
Online ISBN: 978-3-642-35861-6
eBook Packages: Computer ScienceComputer Science (R0)