PhD studentship on language-based provenance security

Do you have a strong background in foundations of computer science, programming languages, or security? Are you interested in applying these foundations to real-world problems to manage trust in intelligence gathering and scientific data?
We are offering a PhD studentship fully funded for three years, including tuition fees (for a student of any nationality) and a stipend of approximately £13,800 per year. The studentship can start in September 2015 or earlier.

The project will be supervised by James Cheney of the School of Informatics at the University of Edinburgh, as part of a project "Foundations of Language-based Provenance Security" funded by the AFOSR European Office of Aerospace Research and Development.

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


Applicants should normally have or expect at least a first class Honours degree, a Masters degree, or equivalent achievement in Computer Science or a related discipline. For more information about the project please see:

http://homepages.inf.ed.ac.uk/jcheney/lbps.html
http://wcms.inf.ed.ac.uk/lfcs/graduate%20study/language-based-provenance-security

Interested applicants should contact James Cheney ([Email Address Removed]) in the first instance to discuss their suitability for either project. The closing date is 12 December 2014. Applications received by this date will receive full consideration for funding; after this date applications will be considered until the position is filled. For detailed application instructions, see:

http://wcms.inf.ed.ac.uk/lfcs/graduate%20study/apply/