Ruzica Piskac Wins Facebook Award For Firewall Proposal

For her work on developing a firewall that repairs itself, Ruzica Piskac, assistant professor of computer science, has received a research award from Facebook.

Ruzica Piskac won a Facebook Communications & Networking award for the proposal “Automated Repair and Verification of Firewalls.” In addition to $50,000, Piskac has been invited to visit the Facebook headquarters.

Typically, firewalls manage your computer’s traffic, deciding what comes in and goes out, according to a set of rules from its administrators. Because of its central role in networks, small changes to the firewall can have a very big effect – especially in increasingly large and complex networks. Companies such as Amazon and Facebook can suffer huge financial losses from even brief outages caused by these changes.

The team of researchers, which also included Ph.D. student William Hallahan and postdoctoral researcher Ennan Zhai, developed FireMason, the first tool that can not only detect errors in firewall behaviors, but also automatically repair the firewall. Once a computer’s administrator observes problems in a firewall, he or she can provide input/output examples that comply with what they want the firewall to do. Based on the examples given, FireMason automatically synthesizes new rules for the existing firewall.

“It takes examples that the user provides and FireMason automatically synthesizes the repair,” Piskac said. “That means our program creates for you a new firewall which is as close as possible to the original firewall and, in addition, behaves according to your specifications."

One of the main challenges in firewall repair and verification is that adding a new rule might fix the current problem, but entirely break the firewall’s behavior in areas that the user might not have considered. To ensure the correctness of the repair, Piskac and her team translated the firewall into the formal mathematical language of first-order logic. From there, they could use tools known as satisfiability modulo theories (SMT) solvers that can automatically prove the correctness of various types of formulas.