PI: Andrei Popescu, University of Sheffield, previously at Middlesex University,  Co-I: Peter Lammich, University of Twente, The Netherlands, previously at The University of Manchester

  • Our society relies increasingly on systems that handle sensitive information by storing it in databases and offering selective access to it.
  • Expressive policies and mechanisms are needed to prevent information leaks while not inhibiting legitimate flows.
  • In this project, we formalise a framework for reasoning about the information flow security of web-based database-backed systems.
  • Our objective is the creation of concepts and tools for specifying and formally proving fine-grained policies, addressing confidentiality needs of real-world systems.

In this project, we design and implement a framework for reasoning about the information flow security of user interactions with relational databases–where the possible interactions are prescribed by input/output reactive programs that query and update the data.

An important characteristic of this framework is that its policy language is extremely flexible, allowing to express not only the absence of certain flows, often captured by variants of non-interference, but also controlled release of information, also known as declassification, in a very fine-grained manner. For example, in an employee database one could be allowed to query the employee salary field, but only collectively, and nothing should be made available beyond the average salary.

As another example, a medical insurance agent should be able to query a medical database for aspects of a patient’s treatment, but only in a manner that does not reveal whether the patient suffers from a terminal illness. Another characteristic of the framework is the support for both fully automatic reasoning when possible and partly interactive reasoning when necessary, using a compositionality infrastructure developed in the proof assistant Isabelle/HOL.

We validate the framework on two case studies of secure-by-design systems: CoCon, a conference management system, and CoSMed, a social media platform.These systems have been previously verified for confidentiality in an ad hoc manner. Using our framework, we further automate and uniformise their verification code base  and helped fix a bug discovered during the running of ITP 2016.

CoCon’s login page before and after ITP 2016

PUBLICATIONS. [1] A. Popescu, P. Lammich, P. Hou. “CoCon: A Conference Management System with Formally Verified Document Confidentiality.”,  Journal of Automated Reasoning 2021. [2] A. Popescu, T. Bauereiss, P. Lammich. ‘Bounded-Deducibility Security. “ (Invited Paper)”. ITP 2021: 3:1-3:20 [3] A paper, reporting on the formalisation of a sizable fragment of the SQL standard in the Isabelle/HOL proof assistant, is under preparation.[4] T. Bauereiss, A. Popescu. “Compositional BD Security”. Arch. Formal Proofs 2021 [5] A. Popescu, P. Lammich, T. Bauereiss. “CoCon: A Confidentiality-Verified Conference Management System”. Arch. Formal Proofs 2021 [6] T. Bauereiss and A. Popescu. “CoSMeDis: A confidentiality-verified distributed social media platform”. Arch. Formal Proofs 2021 [7] T. Bauereiss and A. Popescu. “CoSMed: A confidentiality-verified social media platform”. Arch. Formal Proofs 2021

IMPACT. The guest editorial in the special issue of the Journal of Computer Security (volume 25, Issue 4-5) dedicated to verified information-flow security notes: “The past few years have seen the seeds of information flow security sown in the preceding three decades bear practical fruit. A number of real-world systems with formally verified guarantees of information flow security now exist.” and goes on to cite nine such systems, two of which are the verified web applications CoCon and CoSMed.