Verification of Web-based Systems (VOWS)

In this project, we are concerned with the verification of information-flow security of web applications, more precisely, with confidentiality properties: users of a web-based system should not be able to *infer*, let alone access, some designated sensitive information.

For example, consider a system that stores information about medical patients and offers selective web-based access to individuals and companies. A life insurance company agent should not be given direct access to sensitive information such as a registered patient suffering from cancer. However, ideally the system should also prevent propagation of sensitive information: if it is known that certain discounts are offered mainly to patients suffering from cancer, then the agent can infer that sensitive information if they can access the list of available discounts for that patient.

A proof assistant is an environment for building mathematical models of reality, in particular, of software systems, and mechanically verifying properties about them. A web framework is an environment for writing web applications. The behaviour of a web application can be regarded as an input/output (I/O) automaton: a user interacts with the web application by submitting input (e.g., through the fields of the web forms); in response, the application changes its internal state and outputs a new web page. The I/O automaton model captures the essential information flow through a web application.

We build an infrastructure for verifying the information flow of web applications in a proof assistant. To this end, we design and implement a tool for the automatic translation of web applications written in a web framework into mathematical models in a proof assistant, namely I/O automata. Moreover, in the proof assistant, we formalize a framework for the verification of information-flow security for I/O automata, addressing aspects such as proof automation and compositionality. To validate this entire mechanism, translation plus verification of web applications, we perform a major case study: a confidentiality-verified social media platform.

Our major case study, a confidentiality-verified social media platform, helps a UK charity organization, Caritas Anchor House, establish a secure global humanitarian network. This organization is building an online social media platform aimed at connecting people for matching concrete needs and possibilities for help. The platform will host thousands of users and will manage a large amount of data, including delicate information, e.g., involving troubled children. It is important that such information be handled with care, obeying confidentiality and non-disclosure rules. We bring crucial technical support for this goal, by offering strong confidentiality guarantees for the software running the platform.

Besides the aforementioned immediate impact, we have good reasons to hope for a medium term technological benefit for the economy and the society in general. The functional mechanisms of our society rely increasingly on web-based systems: from banking, to online shopping, to searching for information, to social networking, even to voting. It is important, but currently far from guaranteed, that these systems satisfy privacy properties in order to comply with regulations and ensure the safety and comfort of their users. Public interest and awareness concerning confidentiality aspects is also in rapid growth. For example, a recent survey indicates that most of the users quitting a popular online social platform such as Facebook invoke privacy concerns. Our work is timely with respect to these growing need and growing interest, as it addresses the problem at its core: To guarantee reliable web-based systems, we need an infrastructure to produce machine-checked proofs of their reliability (which can also act as formal certificates addressing public concerns).