Dependency-Based Information Flow Analysis with Declassification in a Program Logic
This work addresses the challenge of ensuring secure information flow with fine-grained declassification for software security, representing an incremental improvement in program logic methods.
The paper tackles the problem of analyzing secure information flows in programs with declassification policies by introducing a deductive approach that tracks dependencies to maintain precision without comparing independent runs, and it demonstrates applicability to object-oriented programs through an explicit heap model.
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.