New Applications of Software Synthesis: Firewall Repair and Verification of Configuration Files

  • Date Friday, February 02, 2018  Time 11:00 AM
  • Speaker Dr. Ruzica Piskac
  • Location Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

    This talk will also be live streamed on our YouTube channel


In this talk we present a systematic effort that can automatically repair firewalls, using the programming by example approach. Firewalls are widely employed to manage and control enterprise networks. Because enterprise-scale firewalls contain hundreds or thousands of policies, ensuring the correctness of firewalls – whether the policies in the firewalls meet the specifications of their administrators – is an important but challenging problem. In our approach, after an administrator observes undesired behavior in a firewall, she may provide input/output examples that comply with the intended behavior. Based on the given examples, we automatically synthesize new firewall rules for the existing firewall. This new firewall correctly handles packets specified by the examples, while maintaining the rest of the behavior of the original firewall.

We also show, using verification for configuration files, how to learn specification when the given examples is actually a set of configuration files. Software failures resulting from configuration errors have become commonplace as modern software systems grow increasingly large and more complex. The lack of language constructs in configuration files, such as types and grammars, has directed the focus of a configuration file verification towards building post-failure error diagnosis tools. In this talk we describe a framework which analyzes data sets of correct configuration files and derives rules for building a language model from the given data set. The resulting language model can be used to verify new configuration files and detect errors in them.


Ruzica Piskac is an assistant professor (tenure-track) at Yale, Computer Science Department. Her research interests span the areas of programming languages, software verification, automated reasoning, and code synthesis. A common thread in Ruzica’s research is improving software reliability and trustworthiness using formal techniques. Ruzica has received a NSF CAREER award for her proposal, “Synthesis in a Live Programming Environment”. She proposed the concept of cooperative programming which combines a live programming environment and the programming by example paradigm.