Rigorous formal methods can be essential for substantial improvements of security. By modeling computer systems and adversaries, formal methods can be used to prove that a system is immune to entire classes of attacks (provided the assumptions of the models are satisfied).

In this talk, I will share some of my recent experience in building secure and pragmatic systems with formal methods. I will present Co-Inflow: an extension of Java with coarse-grained dynamic information-flow control (IFC). By careful design choices and defaults, a programmer typically needs to add very few annotations to a Java program to convert it to a Co-Inflow program with relatively good precision. Additional annotations can improve precision. Co-Inflow achieves this tradeoff between precision and annotation burden by instantiating and specializing recent advances in coarse-grained IFC for a Java-like setting. The essence of Co-Inflow is captured in a middle-weight imperative calculus, and it is proven to provide a termination-insensitive noninterference security guarantee. All proofs are mechanized with the Coq proof assistant. A prototype of Co-Inflow is developed and used to evaluate the precision, usability, and potential performance.

I will also briefly discuss other recent projects on formal analysis of the security of cyber-physical systems, and my planned future work for advancing formal methods toward building computer systems with guarantees of safety, security, and performance.

Jian Xiang is a postdoctoral researcher in the computer science department at Harvard University. His research applies formal method techniques to analyze and enforce the safety and security of computer systems. His current work focuses on language-based security and the security of cyber-physical systems. His broad interests span the areas of security analysis, programming languages, formal methods, and software engineering. His work has appeared in top security venues such as IEEE S&P and field-specific venues such as HSCC. He obtained his Ph.D. in computer science from the University of Virginia, advised by John Knight.