Dependency-Based Information Flow Analysis with Declassification in a Program Logic

TL;DR

This paper introduces a deductive method for analyzing secure information flows in programs, supporting fine-grained policies with declassification, by tracking dependencies explicitly to enhance precision without requiring multiple program executions.

Contribution

It presents a novel deductive approach that explicitly tracks dependencies for information flow analysis, accommodating declassification and object-oriented features.

Findings

High-precision analysis of information flow with declassification

Applicability to object-oriented programs through explicit heap modeling

Avoids the need for comparing multiple program runs

Abstract

We present a deductive approach for the analysis of secure information flows with support for fine-grained policies that include declassifications in the form of delimited information release. By explicitly tracking the dependencies of program locations as a computation history, we maintain high precision, while avoiding the need for comparing independent program runs. By considering an explicit heap model, we argue that the proposed analysis can straightforwardly be applied on object-oriented programs.