Background
David builds programming languages and analysis tools which help programmers build reliable software. In particular, these languages and tools are designed for security-sensitive settings, and when applied, result in systems that are immune to large classes of defects. David leverages state-of-the-art approaches, including program analysis, type checking, mechanized verification, differential privacy, and secure multiparty computation.
David considers a strong adversary when securing systems: the well-intended developer who accidentally misused security-relevant technology, such as cryptography or differential privacy. To combat this adversary, David co-designs programming languages in concert with tools to combat these defects, while also maintaining a usable, general-purpose programming environment for the developer.
At Galois, David will continue to develop programming languages and analysis tools for computer security and data privacy, as well as discover new application domains for formal methods more broadly. Fun fact: The name “Galois” appears four times in the titles of David’s publication history as of September 2020. Read more about David at david.darais.com.
David received his BS from the University of Utah, MS from Harvard University, Ph.D. from the University of Maryland, and was previously an Assistant Professor at the University of Vermont before joining Galois.