BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:STANDARD
DTSTART:20171105T020000
RDATE:20171105T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20180130T230152Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20180202T120000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20180202T110000
DTSTAMP;VALUE=DATE-TIME:20180130T230152Z
LAST-MODIFIED;VALUE=DATE-TIME:20180130T230152Z
UID:http://calagator.org/events/1250473189
DESCRIPTION:Title: New Applications of Software Synthesis: Firewall Repai
 r and Verification of Configuration Files&#13\;\n&#13\;\nAbstract:&#13\;
 \nIn this talk we present a systematic effort that can automatically rep
 air firewalls\, using the programming by example approach. Firewalls are
  widely employed to manage and control enterprise networks. Because ente
 rprise-scale firewalls contain hundreds or thousands of policies\, ensur
 ing the correctness of firewalls – whether the policies in the firewalls
  meet the specifications of their administrators – is an important but c
 hallenging problem. In our approach\, after an administrator observes un
 desired behavior in a firewall\, she may provide input/output examples t
 hat comply with the intended behavior. Based on the given examples\, we 
 automatically synthesize new firewall rules for the existing firewall. T
 his new firewall correctly handles packets specified by the examples\, w
 hile maintaining the rest of the behavior of the original firewall.&#13\
 ;\n&#13\;\nWe also show\, using verification for configuration files\, h
 ow to learn specification when the given examples is actually a set of c
 onfiguration files. Software failures resulting from configuration error
 s have become commonplace as modern software systems grow increasingly l
 arge and more complex. The lack of language constructs in configuration 
 files\, such as types and grammars\, has directed the focus of a configu
 ration file verification towards building post-failure error diagnosis t
 ools.  In this talk we describe a framework which analyzes data sets of 
 correct configuration files and derives rules for building a language mo
 del from the given data set. The resulting language model can be used to
  verify new configuration files and detect errors in them.&#13\;\n&#13\;
 \nBio:&#13\;\nRuzica Piskac is an assistant professor (tenure-track) at 
 Yale\, Computer Science Department. Her research interests span the area
 s 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. Ruzic
 a has received a NSF CAREER award for her proposal\, “Synthesis in a Liv
 e Programming Environment”.  She proposed the concept of cooperative pro
 gramming which combines a live programming environment and the programmi
 ng by example paradigm.\n\nTags: verification\, software\, computer scie
 nce\n\nImported from: http://calagator.org/events/1250473189
URL:https://galois.com/blog/2018/01/new-applications-software-synthesis-f
 irewall-repair-verification-configuration-files/
SUMMARY:Galois Tech Talk: New Applications of Software Synthesis: Firewal
 l Repair and Verification of Configuration Files (Ruzica Piskac)
LOCATION:Galois Inc: 421 Sw 6th Ave Ste 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR