To Secure a Flow
From Specification to Enforcement of Information Flow Control
Time: Tue 2025-03-11 09.00
Location: Kollegiesalen, Brinellvägen 8, Stockholm
Language: English
Subject area: Computer Science
Doctoral student: Amir M. Ahmadian , Teoretisk datalogi, TCS, Language-Based Security
Opponent: Professor Limin Jia, Carnegie Mellon University, Pittsburgh, PA, US
Supervisor: Associate Professor Musard Balliu, Teoretisk datalogi, TCS; Professor Dilian Gurov, Teoretisk datalogi, TCS
QC 20250214
Abstract
The use of software has become increasingly prevalent, affecting nearly every aspect of our daily lives. In this landscape, ensuring the security of software systems is more critical than ever, as vulnerabilities can lead to significant social and financial consequences. Information flow control is a research area focused on developing methods and techniques to provide strong security guarantees against software attacks and vulnerabilities. Information flow control achieves this by tracking how information flows within a program, ensuring that sensitive data does not reach unauthorized outputs. This process can be challenging as it requires precisely defining the software system's security policy and developing mechanisms to enforce that policy against different types of attackers with varying capabilities.
In this thesis, we examine language-based approaches to enforcing information flow control in software systems, with a focus on defining appropriate security policies, attacker models, and enforcement mechanisms to proactively secure modern software systems. The thesis contributes to the state of the art of information flow security in several directions, both theoretical and practical, by investigating four key research questions: defining non-trivial security policies for real-world scenarios, developing appropriate attacker models, creating mechanisms to enforce information flow security conditions, and applying language-based techniques to real-world programming languages. On the policy specification side, we provide a knowledge-based security framework capable of expressing many variants of dynamic policies as well as the Determinacy Quantale, a new semantic model for expressing disjunctive policies in database-backed programs, focusing on the conflict-of-interest classes. We examine the role of attackers in defining security conditions, specifically two types of active attackers and three types of passive attackers with various degrees of capabilities. Moreover, we investigate enforcement mechanisms, such as security type systems and symbolic execution, developed to statically enforce various information flow security policies. Finally, to demonstrate the applicability of language-based approaches in real-world programs, we implement and evaluate the proposed enforcement mechanisms in the programming languages Java and P4.