Modular Monitor Extensions for Information Flow Security in JavaScript

摘要: Client-side JavaScript programs often interact with the web page into which they are included, as well browser itself, through APIs such DOM API, XMLHttpRequest and W3C Geolocation API. Precise reasoning about security must therefore take API invocation account. However, continuous emergence of new APIs, heterogeneity their forms features, renders behavior a moving target that is particularly hard to capture. To tackle this problem, we propose methodology for modularly extending sound information flow monitors generic Hence, verify whether an extended monitor complies proposed noninterference property requires only prove satisfies predefined set conditions. In order illustrate practicality our methodology, show how monitor-inlining compiler can account arbitrary without changing code or proofs original compiler. We provide implementation extension handling fragment Core Level 1 Furthermore, supports addition extensions at runtime.