ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Wed 15 Apr 2015 17:00 - 17:30 at Skeel - Session 6 Chair(s): Helmut Seidl

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. In this paper 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.

Wed 15 Apr

16:30 - 18:00: ESOP - Session 6 at Skeel
Chair(s): Helmut SeidlTechnische Universität München
esop-2015-papers16:30 - 17:00
Arlen CoxUniversity of Colorado Boulder, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Xavier RivalINRIA/CNRS/ENS Paris
esop-2015-papers17:00 - 17:30
Stefano CalzavaraUniversità Ca' Foscari Venezia, Michele BugliesiUniversità Ca' Foscari Venezia, Silvia CrafaUniversity of Padova, Enrico SteffinlongoUniversità Ca' Foscari Venezia
esop-2015-papers17:30 - 18:00
Michael EmmiIMDEA Software Institute, Pierre GantyIMDEA Software Institute, Rupak MajumdarMPI-SWS, Fernando Rosa-VelardoUniversidad Complutense de Madrid