2018-05-23: Information-Flow Control for Concurrent Programs with Declassification

Abstract

Software systems handle a lot sensitive data that must be kept confidential. Such systems are often interactive with complex input-output behavior and handle data with different security levels, necessitating a way to prevent information leakage in complex, untrusted programs. However, existing information-flow control properties, such as noninterference are often too strict for real-world software, due to a lack of support for declassification. Security verification becomes even more challenging in the presence of concurrency and shared memory, which typically requires functional correctness guarantees to soundly reason about interaction between threads.

We present a novel security condition for interactive concurrent programs with shared memory and, to our knowledge, the first compositional approach allowing fine-grained reasoning with declassification support in a shared-memory concurrent setting.

Our declassification policies allow expressing both under what circumstances declassification is allowed as well as limiting exactly what part of secret information can be revealed. To that end, we adapt an existing notion for non-interactive programs, delimited release, to our setting and show a sound embedding into our framework.

We provide a security type system allowing for compositional verification by decoupling functional correctness from security reasoning. The type system leverages standard assertions about functional correctness to support intricate features such as declassification policies and value-dependent declassification, while keeping the type system simple. We show that correctness assertions that can be discharged using existing off-the-shelf verification techniques (such as Owicki-Gries and Rely-Guarantee reasoning). We show how to use our system to establish security of two case studies: a router connecting networks of different security levels and a declassification scheme with user interaction, as often seen in multi-level security operating systems (such as QubesOS).

All results are formalized in Isabelle/HOL.

About Daniel Schoepe

Daniel Schoepe got a Bachelor's degree from TU Darmstadt, working on formalizing information-flow security proofs in Isabelle with Heiko Mantel, and a Master's degree from Chalmers on information-flow security of functional programs with database interaction supervised by Andrei Sabelfeld. He is currently pursuing a Ph.D. at Chalmers in the same area, also supervised by Andrei Sabelfeld.