Securing Interactive Programs


In the last two decades, research in language-based information-flow
security has enabled practical tools, such as JSFlow, Paragon, LIO,
Jif, FlowCaml, and SPARK Examiner, for writing information-flow secure
software. These tools enforce a termination-insensitive notion of
noninterference, which, for batch-job programs, permits one bit to
leak through varied termination behavior. However, the notion is
progress-insensitive, since, for programs with intermediate outputs
(commonplace in languages like JavaScript), there is no bound on leaks
through how far a program progresses in producing output.

In this talk, we will survey my thesis on information-flow security of
interactive programs, e.g. programs which are reactive, event-driven,
and which pass messages. We present a language-independent framework
for reasoning about security of such programs, which generalizes
previous work in this area by not assuming an infinite supply of
ever-available input (an assumption which disregards certain attacks
we will present), and by distinguishing between confidentiality levels
of message presence and message content. We show a hybrid enforcement
mechanism combining a static enforcement of progress-insensitive
noninterference with dynamic output buffering which tightly regulates
leaks through progress. We then show how to disallows leaks through
progress altogether statically, yielding an enforcement of progress-
sensitive noninterference. An even stronger property, timing-sensitive
noninterference, can be enforced by secure multi-execution (SME): a
dynamic black-box mechanism which modifies (modestly) the semantics of
any program to that of a secure program. We show how to declassify
information in SME and how to modify semantics less at the cost of
timing sensitivity. Finally, towards end-to-end security, we give a
sneak preview into our ongoing work on compositional reasoning for
interactive programs.