FP /

ReasoningAboutInformationFlowInAWebBrowser

Reasoning about Information Flow in a Web Browser

Todays feature-packed web browsers exhibit more and more subtle security errors, for example, when HTML code containing JavaScript can be injected in page from another server, which allows sensitive information (such as passwords) to be sent to an attacker. Many of these bugs are in the actual security policies of web browsers, rather than in a faulty implementation. In this project, you will develop a method and an implementation, which we can use to specify security policies of web browsers, and check that private information is safe from security attacks.

Background: Intro.FP, Datastructures, First-order logic; (preferably) AFP, Program Verification. Number of people: 1. Contact person: Koen