  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.

Logic in Computer Science;Cryptography and Security