Before joining Galois, David Darais was an Assistant Professor of Computer Science at the University of Vermont. David’s research focuses on tools for achieving reliable software in critical, security-sensitive, and privacy-sensitive systems. Software errors are costly in these systems, such as incorrect or corrupted output, or privacy violations of sensitive data. David’s research considers a strong adversary in deploying these systems: the intern who wrote the buggy software and misused security-relevant technology, such as cryptography or differential privacy. To combat this adversary, David designs new programming languages which enforce that security and privacy enabling technologies are used properly, while also supporting expressive, general-purpose programming. David applies a wide range of technical approaches, ranging from automated, lightweight verification systems integrated and co-designed with programming languages, to full mechanized verification of software through embedding in proof assistants. David received his BS from the University of Utah, MS from Harvard University, and Ph.D. from the University of Maryland.
At Galois, David will continue to develop usable programming language techniques for secure computation and differentially private algorithms, as well as general applications of 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.