Synthesis Techniques for Security

The problem of implementing a secure program is an ideal problem
domain for formal methods. Even a small error in the logic of a
program can drastically weaken the security guarantees that it
provides. Existing work on applying formal methods to security has
focused primarily on applying verification techniques to determine if
an existing program satisfies a desired security guarantee. In this
talk, I propose that many problems in secure programming can instead
be addressed by synthesizing a provably-secure program automatically.
We review some work on automatically instrumenting programs that
satisfy security properties expressible as safety properties and on a
general framework for designing program synthesizers. I will then describe
a potential line of work on automatically synthesizing programs that
simultaneously satisfy security and functionality.
Somesh Jha received his B.Tech from Indian Institute of
Technology, New Delhi in Electrical Engineering. He received his
Ph.D. in Computer Science from Carnegie Mellon University in
1996. Currently, Somesh Jha is the Sheldon Lubar Professor in the
Computer Sciences Department at the University of Wisconsin (Madison),
which he joined in 2000. His work focuses on analysis of security
protocols, survivability analysis, intrusion detection, formal methods
for security, and analyzing malicious code. Recently, he has also
worked on privacy-preserving protocols. Somesh Jha has published over
150 articles in highly-refereed conferences and prominent journals. He
has won numerous best-paper awards. Somesh also received the NSF
career award in 2005 and became an ACM fellow in 2017.