Abstract
Even though their architecture relies on robust security principles, it is well-known that poor programming practices may expose browser extensions to serious security flaws, leading to privilege escalations by untrusted web pages or compromised extension components. We propose a formal security analysis of browser extensions in terms of a fine-grained characterization of the privileges that an active opponent may escalate through the message passing interface and we discuss to which extent current programming practices take this threat into account. Our theory builds on a formal language that embodies the essential features of JavaScript, together with few additional constructs dealing with the security aspects specific to the browser extension architecture. We then present a flow logic specification estimating the safety of browser extensions modelled in our language against the threats of privilege escalation and we prove its soundness. Finally, we show the feasibility of our approach by means of Chen, a prototype static analyser for Google Chrome extensions based on our flow logic specification.
Chapter PDF
Similar content being viewed by others
Keywords
- Message Passing Interface
- Android Application
- Abstract Memory
- USENIX Security Symposium
- Abstract Environment
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abadi, M.: Secrecy by typing in security protocols. J. ACM 46, 749–786 (1999)
Akhawe, D., Saxena, P., Song, D.: Privilege separation in HTML5 applications. In: USENIX Security Symposium, pp. 429–444 (2012)
Bandhakavi, S., Tiku, N., Pittman, W., King, S.T., Madhusudan, P., Winslett, M.: Vetting browser extensions for security vulnerabilities with VEX. Communications of the ACM 54(9), 91–99 (2011)
Barth, A., Porter Felt, A., Saxena, P., Boodman, A.: Protecting browsers from extension vulnerabilities. In: NDSS (2010)
Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Static validation of security protocols. Journal of Computer Security 13(3), 347–390 (2005)
Bugliesi, M., Calzavara, S., Focardi, R., Khan, W.: Automatic and robust client-side protection for cookie-based sessions. In: Jürjens, J., Piessens, F., Bielova, N. (eds.) ESSoS. LNCS, vol. 8364, pp. 161–178. Springer, Heidelberg (2014)
Bugliesi, M., Calzavara, S., Focardi, R., Khan, W., Tempesta, M.: Provably sound browser-based enforcement of web session integrity. In: CSF, pp. 366–380 (2014)
Bugliesi, M., Calzavara, S., Spanò, A.: Lintent: Towards security type-checking of android applications. In: Beyer, D., Boreale, M. (eds.) FORTE 2013 and FMOODS 2013. LNCS, vol. 7892, pp. 289–304. Springer, Heidelberg (2013)
Calzavara, S., Bugliesi, M., Crafa, S., Steffinlongo, E.: Fine-grained detection of privilege escalation attacks on browser extensions (full version), http://www.dais.unive.it/textasciitildecalzavara/papers/esop15-full.pdf
Carlini, N., Porter Felt, A., Wagner, D.: An evaluation of the Google Chrome extension security architecture. In: USENIX Security Symposium, pp. 97–111 (2012)
Costantini, G., Ferrara, P., Cortesi, A.: Static analysis of string values. In: ICFEM, pp. 505–521 (2011)
Davi, L., Dmitrienko, A., Sadeghi, A.-R., Winandy, M.: Privilege escalation attacks on android. In: Burmester, M., Tsudik, G., Magliveras, S., Ilić, I. (eds.) ISC 2010. LNCS, vol. 6531, pp. 346–360. Springer, Heidelberg (2011)
Dhawan, M., Ganapathy, V.: Analyzing information flow in JavaScript-based browser extensions. In: ACSAC, pp. 382–391 (2009)
Fragkaki, E., Bauer, L., Jia, L., Swasey, D.: Modeling and enhancing Android’s permission system. In: ESORICS, pp. 1–18 (2012)
Guha, A., Fredrikson, M., Livshits, B., Swamy, N.: Verified security for browser extensions. In: 32nd IEEE Symposium on Security and Privacy, pp. 115–130 (2011)
Guha, A., Saftoiu, C., Krishnamurthi, S.: The essence of javaScript. In: D’Hondt, T. (ed.) ECOOP 2010. LNCS, vol. 6183, pp. 126–150. Springer, Heidelberg (2010)
Guha, A., Saftoiu, C., Krishnamurthi, S.: Typing local control and state using flow analysis. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 256–275. Springer, Heidelberg (2011)
Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for javaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238–255. Springer, Heidelberg (2009)
Jensen, S.H., Møller, A., Thiemann, P.: Interprocedural analysis with lazy propagation. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 320–339. Springer, Heidelberg (2010)
Karim, R., Dhawan, M., Ganapathy, V., Shan, C.-c.: An analysis of the mozilla jetpack extension framework. In: Noble, J. (ed.) ECOOP 2012. LNCS, vol. 7313, pp. 333–355. Springer, Heidelberg (2012)
Liu, L., Zhang, X., Yan, G., Chen, S.: Chrome extensions: Threat analysis and countermeasures. In: NDSS (2012)
Maffeis, S., Mitchell, J.C., Taly, A.: An operational semantics for JavaScript. In: APLAS, pp. 307–325 (2008)
Maffeis, S., Taly, A.: Language-based isolation of untrusted JavaScript. In: CSF, pp. 77–91 (2009)
Nielson, F., Nielson, H.R.: Flow logic and operational semantics. Electronic Notes on Theoretical Computer Science 10, 150–169 (1997)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of program analysis. Springer (1999)
Nielson, H.R., Nielson, F., Pilegaard, H.: Flow logic for process calculi. ACM Computing Surveys 44(1), 1–39 (2012)
Politz, J.G., Carroll, M.J., Lerner, B.S., Pombrio, J., Krishnamurthi, S.: A tested semantics for getters, setters, and eval in javascript. In: DLS, pp. 1–16 (2012)
Politz, J.G., Eliopoulos, S.A., Guha, A., Krishnamurthi, S.: Adsafety: Type-based verification of JavaScript sandboxing. In: USENIX Security Symposium (2011)
Porter Felt, A., Wang, H.J., Moshchuk, A., Hanna, S., Chin, E.: Permission re-delegation: Attacks and defenses. In: USENIX Security Symposium (2011)
Roesner, F., Kohno, T., Wetherall, D.: Detecting and defending against third-party tracking on the web. In: NSDI, pp. 155–168 (2012)
Saltzer, J.H., Schroeder, M.D.: The protection of information in computer systems. Proceedings of the IEEE 63(9), 1278–1308 (1975)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Calzavara, S., Bugliesi, M., Crafa, S., Steffinlongo, E. (2015). Fine-Grained Detection of Privilege Escalation Attacks on Browser Extensions. In: Vitek, J. (eds) Programming Languages and Systems. ESOP 2015. Lecture Notes in Computer Science(), vol 9032. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46669-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-662-46669-8_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46668-1
Online ISBN: 978-3-662-46669-8
eBook Packages: Computer ScienceComputer Science (R0)