Temporal and Spatial Nonlocalness in Information Flow Security


Content-dependent information flow policies have received much
attention in the recent decade. We direct our attention from
dependency on current content to dependency on future content,
observing that the latter (temporally nonlocal) dependency is
natural in a class of scenarios, avoiding unnecessary
declassifications and other fluctuations in the flow policies
to be enforced. 

Our future-dependent flow policies use so called ``prophetic
variables'' to refer to the final values of program variables.
A prophetic variable remains constant in each specific
execution, preventing policies from being inadvertently
weakened due to concurrent interference. For present-dependent
flow policies, such (spatially nonlocal) interference is
nontrivial and addressed recently using rely-guarantee
reasoning.

In this talk, I present previous work on using prophetic
variables to define and enforce future-dependent security,
ongoing work on lifting rely-guarantee-style reasoning for
modularizing distributed system security, and potential future
directions in rely-guarantee-style reasoning for secure
information flow.