David Brumley

Professor of ECE, Affiliated Faculty

CMU Scholars Page

ORCiD

Office 2202 Mehrabian Collaborative Innovation Center

Email dbrumley@cmu.edu

Phone (412) 268-3851

Department
CIT - Electrical and Computer Engineering
Computer Science Department: Affiliated

Research Interests
Formal Methods
Security
Cryptography
Security and Privacy
Systems

Advisees
Seunghyun Lee

CSD Courses Taught

15330 - Spring, 2024

Research Statement

My primary research area is software security techniques that give users guarantees. My research is at the intersection of model checking, formal methods, compilers, and logic, all of which are applied to security problems.  Some of the central techniques that we are developing in order to accomplish our goals include efficient symbolic execution, reasoning about bit-level arithmetic in finite fields, sound decompilation, and decision procedures.  I also work in other areas of computer security, such as network security and applied cryptography. In these areas, we look at efficient protocols, efficient signature schemes, and privacy-preserving cryptography.

Current questions we are working on include can we automatically generate exploits?  Can we automatically develop recognizers for exploits of a particular vulnerability?  What are the limits of reverse engineering?  Can we show that Microsoft implements RSA correctly, and that they aren't stealing our secrets?  Can we show a crypto algorithm doesn't leak secrets via side-channels?  What do we need to change to keep software patches from breaking systems?  How do things change in critical systems, e.g., securing an MRI machine in a hospital? Would you want to be the first to get an MRI after a software update?

In our setting, we typically assume the software in these settings is only available in binary (i.e., executable) form.  Binary code analysis is attractive for several reasons. First, binary-level code analysis allows us to argue about the security of the code that actually executes, not just what was compiled.  Second, everyone has access to the programs they run in binary form, thus binary-only techniques promise to be widely applicable. Finally, a binary program is a program in the most basic and primitive form. If we can reason about security concerns at the binary level, we can faithfully reason about software security problems in any language.

Publications