Balancing Security-Privacy and Functionality in Software Synthesis

The problem of implementing a secure program is an ideal problem
domain for formal methods. In this talk, I will be using security as a
term that encompasses traditional security concepts and also privacy.
Even a small error in the logic of a program can drastically weaken
the security and privacy 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. However, the challenge is to synthesize
correct software from the outset. However, the key issue here is to
balance security and functionality (a secure software that does
nothing is easy to synthesize. Just do nothing.)

In this work, I will describe some of the projects that I have worked on
that balance the two competing requirements (i.e., security-privacy
and functionality). I will then describe some interesting open
problems along these lines.
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 Grace Wahba 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 and adversarial machine
learning. Somesh Jha has published over 150 articles in
highly-refereed conferences and prominent journals. He has also won
numerous best-paper awards. Somesh also received the NSF career award
in 2005 and became an ACM fellow and IEEE fellow in 2017.