[Colloq] Talk - Willard Thor Rafnsson - End-to-End Information-Flow Security for Interactive Systems - Monday, September 22nd, 9:45am, 166 WVH

[Biron, Jessica]

Speaker: Willard Thor Rafnsson 

Title: End-to-End Information-Flow Security for Interactive Systems

Monday, September 22nd
9:45am - 10:45am
166 WVH

Abstract: 

We provide means to achieve end-to-end information-flow security in 
interactive systems. The elusiveness of this problem stems from the 
fact that interaction patterns, primitives, synchronous communication 
and nondeterminism combine in ways where seemingly innocuous systems 
compromise security in unexpected ways under interaction.
 
We study what it means for systems to preserve confidentiality in a 
nondeterministic interactive setting. We focus on two properties:
progress-sensitive noninterference (PSNI), requiring that observable 
behavior is invariant to confidential input, and progress-insensitive 
noninterference (PINI), permitting confidential input to impede the 
ability of a system to make progress on its observable output. The 
latter is a popular target of information-flow security enforcement 
mechanisms, e.g. JSFlow, Jif, and sequential LIO. To identify the 
essence of interactive systems security, we explore classes of attacks 
in this setting, and find previous work ignores e.g. attacks powered 
by varied input presence -- a high-bandwidth channel in our setting.

To address this, we devise a new, preservation-based, formalization of 
noninterference, which guarantees secure systems interact securely.
Our formalization is thereby compositional; we prove this for a core 
of combinators, and derive a rich language of security-preserving 
combinators from it. While both PSNI and PINI are preserved under 
arbitrary wirings, PINI relies fundamentally on the lack of scheduling 
fairness to guarantee security of interactions. This makes PINI unfit 
for autonomous interactive systems security.
 
To facilitate building secure systems in parts, we advance secure 
multi-execution (SME): a combinator which repairs insecurities. SME 
thus makes any interactive system, secure or not, readily pluggable 
into a secure composed system. We prove soundness for all fair 
schedulers, and redesign SME to enforce PSNI, obtaining a more 
semantics-preserving combinator. We give a language-independent model 
for information release in SME. For scenarios where semantics must be 
preserved, we present type-based enforcements of PSNI and PINI.