Information Flow Tracking for Side-effectful Libraries
by Alexander Sjösten, Daniel Hedin, and Andrei Sabelfeld.
DOI, short version PDF, full version PDF Prototype Proof
This paper was published and presented at FORTE 2018.
Dynamic information flow control is a promising technique for ensuring
confidentiality and integrity of applications that manipulate sensitive
information. While much progress has been made on increasingly powerful
programming languages ranging from low-level machine languages to high-level
languages for distributed systems, surprisingly little attention has been
devoted to libraries and APIs. The state of the art is largely an
all-or-nothing choice: either a shallow or deep library
modeling approach. Seeking to break out of this restrictive choice, we
formalize a general mechanism that tracks information flow for a language
that includes higher-order functions, structured data types and references.
A key feature of our approach is the model heap, a part of the
memory, where security information is kept to enable the interaction between
the labeled program and the unlabeled library. We provide a
proof-of-concept implementation and report on experiments with a file system
library. The system has been proved correct using Coq.