Keynote Speakers

Title: Self-Certifying and Secure Compilation
Kedar Namjoshi, Bell Labs, Nokia

Abstract: An optimizing compiler improves the performance of a program by modifying its instructions, control flow, and data representations. How can one be sure that such changes are implemented correctly? Testing is difficult, as it requires producing programs as test data. A mechanized correctness proof is infeasible for a production compiler such as GCC or LLVM. This talk explores a third alternative, self-certification, where a compiler generates a proof of correctness with each compilation run. As the compiler is untrusted, generated proofs have to be independently validated by automated methods. I will lay out the theoretical basis behind this technique, discuss why proof generation and proof checking are feasible in practice, and sketch our implementation for the LLVM compiler.

A compiler transformation may be correct and yet be insecure. The possibility of an information leak being silently introduced during compilation is troubling, as such leaks can be hard to detect. I will present a notion of secure compilation, show that some commonly applied optimizations can be insecure, and describe how they may be secured.

The end goal is fully verified and secure compilation: throughout the talk, I will highlight important implementation challenges and intriguing open questions.

Speaker Bio
Kedar Namjoshi is a member of technical staff at Bell Laboratories. He received his Ph.D. degree from the University of Texas at Austin (with E. Allen Emerson) and the B.Tech. degree from the Indian Institute of Technology, Madras, both in the computing sciences. His research interests include program semantics, logics and verification, model checking, static program analysis, distributed computing, and programming methodology.
Kedar's research explores the interplay between the deductive and algorithmic approaches to verification. Contributions include decision procedures for parameterized model checking via cutoff theorems, algorithms and tools for compositional verification, abstraction methods for branching-time logics, the theory and applications of well-founded bisimulation, and the development of localized symmetry reduction. Current research is on self-certifying compilation, network verification, and the synthesis of fault-tolerant and secure programs. This research has been supported in part by grants from the NSF and DARPA.