Principles of Programing Seminar
— 4:30pm
Location:
In Person and Virtual - ET
-
Gates Hillman 7101 and Zoom
Speaker:
WILLARD RAFNSSON
,
Assistant Professor
IT University of Copenhagen (ITU)
https://www.willardthor.com/
Information-Flow Control That Scales
Information-flow control (IFC) is the act of tracking the flow of information through a program, to ensure that it handles information securely. IFC is the basis of many methods to protect confidentiality and integrity of data, and IFC research is part of computer security foundations (CSF) research, which involves developing mathematical models of problems and methods in computer security, to put technical solutions to security and privacy problems on solid ground.
In this talk, we give a brief history and overview of IFC research as a whole. We highlight the main challenges in IFC, and explain how these challenges are important to PL and FM research in general.
We then present our past and ongoing research towards one of the main open challenges in IFC: making enforcements scale. State-of-the-art IFC enforcements do not scale to large programs, because they do not facilitate compositional reasoning; they enforce properties that are not preserved under composition. How one facilitates compositional reasoning is not well understood in state-of-the-art. We motivate how this involves a careful balance in the choice of systems, attackers, and combinators. We then present a theory for compositional reasoning that strikes this balance. It is a domain-specific language (DSL) for composing asynchronously communicating processes in many practical ways, including ways that introduce state and ways to suspend and resume processes (for implementing schedulers). We prove under which conditions a combinator preserve timing-sensitive noninterference, for each combinator in our language. We do this by desugaring our DSL to a core set of combinators. We demonstrate that our theory makes it straightforward 1) to prove, through compositional reasoning, that complex systems are free of external timing channels, and 2) to identify sub-components that cause information leakage.
We close by briefly summarizing ongoing research in this directions: 1) adding probabilities to the above theory, and 2) articulating the different nuances in different styles of noninterference definitions.
—
Willard Rafnsson is an Assistant Professor at the IT University of Copenhagen (ITU). His research is at the intersection of programming languages (PL), formal methods (FM), and security. He has published foundational results on information-flow control, and published on privacy and on vulnerability scanning. His research agenda is to help developers write secure software. He worked as a Postdoc at Max Planck Institute for Software Systems (MPI-SWS), hosted by Deepak Garg, and at Carnegie Mellon University (CMU) CyLab, hosted by Limin Jia and Lujo Bauer. He completed his PhD at Chalmers University of Technology in the security lab, supervised by Andrei Sabelfeld, and a MSc at Aalborg University (AAU), supervised by Hans Hüttel.
Faculty Host: Stephanie Balzer In Person and Zoom Participation. See announcement.Event Website:
http://www.cs.cmu.edu/Groups/pop/
For More Information:
ahornick@andrew.cmu.edu