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 modeled 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 analyzer for Google Chrome extensions based on our flow logic specification.

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.

Fine-grained Detection of Privilege Escalation Attacks on Browser Extensions

CALZAVARA, STEFANO;BUGLIESI, Michele;Steffinlongo, Enrico
2015-01-01

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.
2015
ESOP 2015
File in questo prodotto:
File Dimensione Formato  
esop15.pdf

non disponibili

Descrizione: Articolo principale
Tipologia: Documento in Post-print
Licenza: Accesso chiuso-personale
Dimensione 429.46 kB
Formato Adobe PDF
429.46 kB Adobe PDF   Visualizza/Apri
Calzavara2015_Chapter_Fine-GrainedDetectionOfPrivile.pdf

accesso aperto

Tipologia: Versione dell'editore
Licenza: Accesso chiuso-personale
Dimensione 405.07 kB
Formato Adobe PDF
405.07 kB Adobe PDF Visualizza/Apri

I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/10278/3655341
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 11
social impact