A Language For Information Flow:

Dynamic Tracking in Multiple Interdependent Dimensions

Avraham Shinnar, Marco Pistoia, and Anindya Banerjee.

Abstract

This paper presents λ_I, a language for dynamic tracking of information flow across multiple, interdependent dimensions of information. Typical dimensions of interest are integrity and confidentiality. λ_I supports arbitrary domain-specific policies that can be developed independently. λ_I treats information-flow metadata as a first-class entity and tracks information flow on the metadata itself (integrity on integrity, integrity on confidentiality, etc.). This paper also defines IMPOLITE, a novel class of information-flow policies for λ_I. Unlike many systems, which only allow for absolute-security relations, IMPOLITE can model more realistic security policies based on relative-security relations. IMPOLITE demonstrates how policies on interdependent dimensions of information can be simultaneously enforced within λ_I's unified framework.

Tech Report

The paper is currently available as an IBM Tech Report.

Citation

Bibtex Citation (Tech Report)

@techreport{shinnar:lambdaif,
  author = "Avraham Shinnar, Marco Pistoia, and Anindya Banerjee",
  title = "A Language for Information Flow: Dynamic Tracking in Multiple Interdependent Dimensions",
  institution = "IBM Research",
  number = "RC24541",
  month = apr,
  year = 2008
}

IBM Research Link

It is IBM Research Technical Report RC24541.

Random Info

I did this work while I was a Summer Intern at IBM Research (Hawthorne) during the Summer of 2007. I was working with Marco Pistoia at IBM, and Anindya Banerjee, from Kansas State University, who was on sabbatical at IBM for the summer. We started with their previous work Beyond Stack Inspection: A Unified Access-Control and Information-Flow Security Mode. We initially planned on implementing both a static and dynamic analysis for Java security based on this work. However, I was curious about some of the formalism, and we started working on it a bit. "A bit" wound up begin quite a bit, and we then generalized things quite a bit, and spent the summer frantically proving theorems about the language.