Information flow monitoring as abstract interpretation for relational logic

Andrey Chudnov, George Kuan, David A. Naumann

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

16 Scopus citations

Abstract

A number of systems have been developed for dynamic information flow control (IFC). In such systems, the security policy is expressed by labeling input and output channels, it is enforced by tracking and checking labels on data. Systems have been proven to enforce some form of noninterference (NI), formalized as a property of two runs of the program. In practice, NI is too strong and it is desirable to enforce some relaxation of NI that allows downgrading under constraints that have been classified as 'what', 'where', 'who', or 'when' policies. To encompass a broad range of policies, relational logic has been proposed as a means to specify and statically enforce policy. This paper shows how relational logic policies can be dynamically checked. To do so, we provide a new account of monitoring, in which the monitor state is viewed as an abstract interpretation of sets of pairs of program runs.

Original languageEnglish
Title of host publicationProceedings - 2014 IEEE 27th Computer Security Foundations Symposium, CSF 2014
Pages48-62
Number of pages15
ISBN (Electronic)9781479942909
DOIs
StatePublished - 13 Nov 2014
Event27th IEEE Computer Security Foundations Symposium, CSF 2014 - Vienna, Austria
Duration: 19 Jul 201422 Jul 2014

Publication series

NameProceedings of the Computer Security Foundations Workshop
Volume2014-January
ISSN (Print)1063-6900

Conference

Conference27th IEEE Computer Security Foundations Symposium, CSF 2014
Country/TerritoryAustria
CityVienna
Period19/07/1422/07/14

Keywords

  • Abstract interpretation
  • Declassification
  • Endorsement
  • Information flow
  • Relational logic
  • Run-time monitoring

Fingerprint

Dive into the research topics of 'Information flow monitoring as abstract interpretation for relational logic'. Together they form a unique fingerprint.

Cite this