Dissertation Defense - William Hallahan

Event time: 
Wednesday, March 9, 2022 - 4:00pm
Location: 
Zoom Presentation See map
Event description: 

Dissertation Defense
William Hallahan

Title: Automated Approaches for Program Verification and Repair

Advisor: Ruzica Piskac

Other committee members:
Zhong Shao
Abhishek Bhattacharjee
Nate Foster (Cornell University)

Abstract:

Formal methods techniques such as verification, analysis, and synthesis allow programmers to prove properties of their programs, or automatically derive programs from specifications. This dissertation presents automated analysis and synthesis techniques to ease the debugging of modular verification systems, allow easy access to constraint solvers from functional code, and to reduce the burden of network administrators writing and analyzing firewalls.

We describe the design and implementation of a symbolic execution engine, G2, for non-strict functional languages such as Haskell. We then extended G2 to assist with modular verification. Modular verifiers allow programmers to write and prove specifications of their code. When a modular verifier fails to verify a program, it could be because of an actual bug in the program, but it could also be because a specification somewhere in the program is too weak. We present a technique, counterfactual symbolic execution, to aid in the debugging of both types of modular verification failures, by finding counterexample or counterexample-like explanations of the failure. Further, a counterexample-guided inductive synthesis (CEGIS) loop based technique is introduced to fully automate modular verification, by using found counterexamples to automatically infer needed function specifications. The counterfactual symbolic execution and automated specification inference techniques are evaluated on existing LiquidHaskell errors and programs.

In addition to leveraging G2 to explain modular verification errors, we built a library, G2Q, which makes it easy for Haskell programmers to call G2 to solve constraint problem written in Haskell. G2Q uses symbolic execution to unroll recursive function definitions, and guarantees that the use of G2Q constraints will preserve type correctness.

Finally, we describe techniques to ease analysis and repair of firewalls. Firewalls are widely deployed to manage network security. However, firewall systems provide only a primitive interface, in which the specification is given as an ordered list of rules. This makes it hard to manually track and maintain the behavior of a firewall. We introduce a formal semantics for iptables firewall rules via a translation to first-order logic with uninterpreted functions and linear integer arithmetic, which allows encoding of firewalls into a decidable logic. We then describe techniques to automate the analysis and repair of firewalls using SMT solvers, based on user provided specifications of the desired behavior. We evaluate this approach with real world case studies collected from StackOverflow users.