Language-based provenance security

Provenance means metadata/trace information about a computation. Many scientific disciplines are increasingly data-driven and require support for provenance to make it possible to safely share and reuse raw data or processed results. There are many intriguing interactions between provenance and classical problems in programming languages and security. This includes language-based security (information flow), incremental or bidirectional computation, and software engineering (program slicing) for provenance-tracking. A number of projects in this area are possible, including:

• Enriching and extending formal models of provenance from simple programming languages or database query languages to handle features such as concurrency, references, side-effects, notions of location, time, or boundaries of control
• Analysing existing proposals for provenance security mechanisms, and identify shortcomings or generalisations leading to a richer understanding of policies and correct mechanisms for provenance
• Developing efficient techniques for integrating provenance-tracking techniques into programming languages or other frameworks
• Formalising and verify provenance techniques in mechanised proof systems or dependently-typed languages such as Coq, Agda or Isabelle/HOL
  

This project would be suitable for a student with some background in programming languages, semantics, or security, and interest in applications to system configuration and other industrially-relevant problems.

Potential Supervisors:

James Cheney

For more information see our recent publications here.