Future-dependent Flow Policies with Prophetic Variables

Ximeng Li, Flemming Nielson, Hanne Riis Nielson

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


Content-dependency often plays an important role in the information flow security of real world IT systems. Content dependency gives rise to informative policies and permissive static enforcement, and sometimes avoids the need for downgrading. We develop a static type system to soundly enforce future-dependent flow policies- policies that can depend on not only the current values of variables, but also their final values. The final values are referred to using what we call prophetic variables, just as the initial values can be referenced using logical variables in Hoare logic. We develop and enforce a notion of future-dependent security for open systems, in the spirit of "non-deducibility on strategies". We also illustrate our approach in scenarios where future-dependency has advantages over present-dependency and avoids mixtures of upgradings and downgradings.
Original languageEnglish
Title of host publicationProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security
PublisherAssociation for Computing Machinery
Publication date2016
ISBN (Print)978-1-4503-4574-3
Publication statusPublished - 2016
Event2016 ACM Workshop on Programming Languages and Analysis for Security - Vienna, Austria
Duration: 24 Oct 201624 Oct 2016


Conference2016 ACM Workshop on Programming Languages and Analysis for Security


Dive into the research topics of 'Future-dependent Flow Policies with Prophetic Variables'. Together they form a unique fingerprint.

Cite this