Run-time Monitoring and Formal Analysis of Information Flows in Chromium

摘要: Web browsers are a key enabler of wide range online services, from shopping and email to banking health services. Because these services frequently involve handling sensitive data, web browser security policies mechanisms has been implemented or proposed mitigate the dangers posed by malicious code sites. This paper describes an approach for specifying enforcing flexible information-flow on Chromium browser. Complementing efforts that focus enforcement JavaScript, our focuses existing encompasses broad features, pages scripts DOM elements, events, persistent state, extensions. In approach, which is coarse-grained, light-weight implementation taint tracking, entities in annotated with labels specify policy track information flows. We develop detailed formal model we prove noninterference. also corresponding prototype system built top Chromium. demonstrate, experimentally confirm, can enforce many policies, as well practically useful beyond those enforceable standard browsers.