A Core Calculus for Provenance

Umut A. Acar, Amal Ahmed, James Cheney, Roly Perera

Research output: Chapter in Book/Report/Conference proceedingConference contribution


Provenance is an increasing concern due to the revolution in sharing and processing scientific data on the Web and in other computer systems. It is proposed that many computer systems will need to become provenance-aware in order to provide satisfactory accountability, reproducibility, and trust for scientific or other high-value data. To date, there is not a consensus concerning appropriate formal models or security properties for provenance. In previous work, we introduced a formal framework for provenance security and proposed formal definitions of properties called disclosure and obfuscation

This paper develops a core calculus for provenance in programming languages. Whereas previous models of provenance have focused on special-purpose languages such as workflows and database queries, we consider a higher-order, functional language with sums, products, and recursive types and functions. We explore the ramifications of using traces based on operational derivations for the purpose of comparing other forms of provenance.We design a rich class of provenance views over traces. Finally, we prove relationships among provenance views and develop some solutions to the disclosure and obfuscation problems.
Original languageEnglish
Title of host publicationPrinciples of Security and Trust
Subtitle of host publicationFirst International Conference, POST 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012, Proceedings
EditorsPierpaolo Degano, JoshuaD. Guttman
PublisherSpringer-Verlag GmbH
Number of pages20
ISBN (Electronic)978-3-642-28641-4
ISBN (Print)978-3-642-28640-7
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'A Core Calculus for Provenance'. Together they form a unique fingerprint.

Cite this