Reliably Secure Software Systems (RS3) –
DFG Priority Programme 1496

Security in Web-based Workflow Management Systems

Application Scenario & Motivation

The Web contains a variety of complex applications with workflows processing sensitive data both on the server and in the browser, e.g., Amazon, Facebook, EasyChair, or HealthVault. These systems often deal with confidential information like credit card details, medical and health-related data, location information, and sensitive documents. In order to prevent unintended information disclosure, the flows of confidential information to the different users and services have to be carefully controlled, both in the presence of malicious attackers and of programming errors that could lead to information leaks.

Our goal is a methodology to verify end-to-end information flow security properties of web-based workflow systems. This methodology encompasses both the server components of web-based systems as well as the client-side components in the web browser.

Our primary case study for the methodology is CoCon, a verified and usable system for organizing the peer-review process of scientific conferences, similar to EasyChair. Such a conference management system has complex confidentiality requirements, e.g. "authors learn nothing about their paper's reviewer assignment beyond the number of reviewers, and only in the notification phase."

Approach

The security of the web-based workflow system has to be ensured both on the server side and on the client side. For example, in the case of CoCon, on the server side we have to ensure that the server code keeps reviews secret from the authors of other papers. On the client side, we have to protect against untrusted JavaScript code running in the browser, which may leak reviewer names to untrusted web locations.

The guarantee on the server side implementation is obtained by a formal proof in the theorem prover Isabelle. The formal specification is written as a program in a functional programming language, and the code extraction feature of Isabelle generates executable Scala code, wrapped into a REST API. We verify that, by interacting with this API, users of the system cannot learn more about confidential information than what we specify.

The client side implementation of CoCon in the JavaScript web framework AngularJS is secured at runtime in the web browser. The web pages coming from the server carry security policy information, declaring, for example, that text entered into a review form by the user may only flow to the review API of the system. A monitor running in the browser enforces this policy. This ensures that confidential information like reviews is protected and does not flow to untrusted sinks. The soundness of the enforcement has been formally proved wrt. an abstract model of JavaScript execution, event handling, and DOM manipulation. [1, 2]

Beyond our particular case study CoCon, we envision our techniques to become the basis of a reusable methodology for secure web-based workflow management systems: verifying the server-side core of the system with the help of the interactive and automatic proof techniques we developed, then generating executable server-side code, and complementing this with monitoring of untrusted code on the client side.

Solution

The main tangible product of this reference scenario is the web-based conference management system CoCon, a real-world, usable system with complex security requirements. It offers features comparable to existing systems such as EasyChair, e.g. providing convenient means for discussions within the program committee. The user interface is built upon state-of-the-art technologies for web applications, e.g. web frameworks for dynamic UI generation.

The web-based UI can be seen in the following screenshot or by trying the online demo system.

The security requirements on the server side are ensured by verifying several confidentiality properties, such as: "program committee members learn nothing about the updates to a paper's content beyond the final version, and only after the submission phase." We have designed a parameterized security notion called Bounded Deducibility (BD) security to capture such properties: its parameters specify what an attacker can observe about the system and which information is (potentially) confidential, a declassification bound ("beyond" which information should not flow), and a declassification trigger ("unless" which information should not flow) — the last two expressed as arbitrary formulas in higher-order logic (HOL). More details of the formalization can be found in [3]. For CoCon, we have verified these properties with the interactive theorem prover Isabelle. Improving the automation of proofs, e.g. by integrating model checking techniques [4], is ongoing work.

Besides the server-side code, a web application typically consists of JavaScript code running in the browser. For CoCon, the user interface is rendered dynamically on the client side using the AngularJS framework. This third-party code is untrusted and could leak data, either maliciously or through a programming error. For example, on the left-hand side of the following screenshot, a piece of JavaScript code running in the browser of a reviewer has leaked confidential reviews by posting them as public news item, which can be seen by every user.

Hence, we complement the server-side verification with an information flow control (IFC) mechanism for browsers on the client side, implemented for Safari/Webkit. With a suitable client-side policy, this mechanism ensures that untrusted JavaScript code, in particular the UI web framework, cannot compromise the security guarantees of the server application. The IFC-enabled browser, display on the right-hand side of the screenshot, prevents the leak due to a policy that labels reviews as confidential and news items as public. This gives us an end-to-end security guarantee for CoCon, covering both server and client.

Highlights

  • CoCon, a conference management system with both verified security and practical usability — in fact, it has been used in production for the Isabelle workshop 2014, the TABLEAUX conference 2015, and the ITP conference 2016.

  • An integration of techniques for formal verification on the server-side, generation of server code corresponding to the verified formal specification, and run-time monitoring of untrusted client-side code for end-to-end security guarantees.

Publications

[1] Information flow control in WebKit's JavaScript bytecode. A. Bichhawat, V. Rajani, D. Garg, and C. Hammer. In Principles of Security and Trust 2014.
[2] Information Flow Control for Event Handling and the DOM in Web Browsers. V. Rajani, A. Bichhawat, D. Garg, and C. Hammer. In Computer Security Foundations Symposium 2015.
[3] A Conference Management System with Verified Document Confidentiality. S. Kanav, P. Lammich, and A. Popescu. In Computer Aided verification 2014.
[4] Temporal logics for hyperproperties. M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. Sanchez. In Principles of Security and Trust 2014.