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

Mittwoch, 14. März 2018
13.30 – 15.00 Uhr

Universität Konstanz, A702


Dr. Ruzica Piskac, Yale

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.

Short bio:
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.