Towards Program Synthesis for Security

  • Markus N. Rabe  | University of California, Berkeley

Many of the major security problems are caused by small programming errors, which could be avoided by automating menial programming tasks through program synthesis. However, program synthesis is still limited to a few lines of code at a time. In this talk, I will discuss fundamental problems that limit the scalability of existing program synthesis algorithms and suggest a new algorithmic principle to overcome these problems. For the sake of simplicity, we formulate the algorithm for quantified Boolean formulas (QBFs). It already significantly improves over the state of the art in QBF solving and I will report on some initial, promising experiments on applying the algorithm to program synthesis. The last part of the talk will focus on quantitative synthesis problems. While often believed to be even harder than regular synthesis problems, I will show that quantitative synthesis can, in fact, be simpler. By exploiting approximate model counting via universal hashing, we can synthesize approximately optimal solutions with a polynomial number of SAT queries. The algorithm not only establishes a complexity result but also proved useful in two case studies on quantitative information flow and on approximate program synthesis.

Series: Microsoft Research Talks