In this talk, I will first provide an overview of language-based approaches to information flow security. The goal is to prevent secret information from being leaked to the attackers. This can be achieved by labeling sensitive data using a security label, e.g., secret, and ensuring that information does not flow from data labeled secret to attacker-observable events (e.g., writes to a memory location that the attacker has access to). There are static approaches that allow programmers to label data using information flow types. There, the compiler checks the security of the program at compile time. There are also dynamic approaches, where a runtime monitor tracks movement of secret data and stops the execution or takes remedial actions (e.g., returns a dummy value when an attack tries to read secret variables) to enforce security policies. In the end, I will show how to connect the two approaches via gradual information flow types.

Dr. Jia is an Associate Research Professor in the ECE Department at Carnegie Mellon University. Dr. Jia received her PhD in Computer Science from Princeton University. She received her BE in Computer Science and Engineering from the University of Science and Technology in China. Dr. Jia’s research interests are in formal aspects of software security, in particular, applying formal logic to constructing software systems with known security guarantees.