Informal Methods for Large Code, Formal Methods for Small Code

Thursday, October 11, 2018 -
4:00pm to 5:00pm
2310 CS

Speaker Name: 

Tristan Ravitch

Speaker Institution: 

Galois, Inc.




Galois uses a wide variety of program-analysis techniques across our projects. In this talk, I will describe some work we have done at opposite ends of the automated-program-reasoning spectrum. First, I will describe work we have done on information-flow analysis in Android applications with the aim of identifying colluding applications, with a focus on the trade-offs required for large-scale analysis. Second, I will describe work we have done to formally verify parts of s2n, which is an open-source implementation of TLS. This work was much more focused on smaller pieces of code, but provides significantly stronger guarantees.