Research Projects

 

Symbolic Execution Engine for Haskell

G2 is a symbolic execution engine for Haskell, a non-strict, functional programming language.  Symbolic execution is a technique that runs a program with symbolic variables as inputs, and gives output in terms of expressions and constraints involving those symbolic variables.  By using SMT solvers to solve the constraints, G2 can find concrete inputs to Haskell programs that satisfy assumptions or violate assertions.

G2 has been applied to generate concrete and counterfactual counterexamples for errors from the LiquidHaskell modular verification tool.  Concrete counterexamples identify actual errors in the users code, while counterfactual counterexamples identify output specifications that must be strengthened to enable verification.

People involved in the project:

William T. Hallahan

Recent Publications:

William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala and Ruzica Piskac.

Lazy counterfactual symbolic execution.

In Proceedings of the 40th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA,
June 22-26, 2019., 2019.

[ bib | DOI | http ]

William T. Hallahan, Anton Xue and Ruzica Piskac.

G2Q: Haskell constraint solving.

In Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell. 2019.

[ bib | DOI | http ]

 

Privacy Preserving Formal Methods

The use of formal methods for program analysis and verification is one of the most effective techniques computer science has for establishing the correctness of our systems. The goal of our privacy preserving formal methods (PPFM) project is to develop methods for mutually distrustful parties to evaluate correctness while maintaining secrecy of objects such as algorithms, programs, protocols, specifications, and constraints rendered as logical formulae. Our work combines cryptography, especially secure multiparty computation (MPC), with formal methods to develop efficient and secure protocols for private verification.  

 

One component of the project is privacy preserving model checking (PPMC). Model checking is a powerful technique for verifying programs meet specifications written in modal logics. Our work on PPMC has
potential to allow auditors and regulators -- such as Apple and Google in their roles as app store maintainers -- to verify programs without the developer needing to expose their valuable software. Another component of PPFM is privacy preserving satisfiability solving (PPSat). Boolean satisfiability is an essential problem in verification, and in computer science more generally. Our work allows multiple parties to check a conjunction of logical formulae. An example application is to allow two network routers to coordinate traffic while maintaining privacy of their configurations.

 

Reactive systems that operate in environments with complex data, such as mobile apps or embedded controllers with many sensors, are difficult to synthesize.  Synthesis tools usually fail for such systems because the state space resulting from the discretization of the data is too large.  

 

In this project, we have introduced Temporal Stream Logic (TSL), a new temporal logic that separates control and data. TSL provides an attractive trade-off for synthesis. On the one hand, synthesis from TSL, unlike synthesis from standard temporal logics, is undecidable in general. On the other hand, however, synthesis from TSL is scalable, because it is independent of the complexity of the handled data. Some of the application domains to which we have successfully used TSL for synthesis include:

- a music player Android app

- a controller for an autonomous vehicle in the Open Race Car Simulator (TORCS)

- a hardware implementation of a kitchen timer

 

Mark Santolucito, William T. Hallahan, and Ruzica Piskac.

Live programming by example.

In Extended Abstracts of the 2019 CHI Conference on Human
Factors in Computing Systems, CHI 2019, Glasgow, Scotland, UK, May 04-09,
2019., 2019.

[ bib | DOI | http ]

Verifications for Configuration Files

Modern verification technologies inherently depend on the availability of formal specifications, yet they are extremely labor intensive to create and maintain. This is especially the case for configuration files, which rarely have any documentation, even in written English form. Configurations are the values of system parameter settings; Incorrect configurations often lead to system misbehaviours such as exceptions, error code return, crashing or even core dump. 

We have developed ConfigV, which is the first tool that can automatically detect complex errors involving multiple variables, and learn over a training set of partially incorrect configuration files. Since configuration files lack helpful semantic information to infer types, we use a probabilistic inference method to learn likely types for keywords based on their values from the training set. We combined this new type of information with a generalization of association rule learning that handles not just association rules, but arbitrary, typed predicates. We evaluated ConfigV by verifying public configuration files on GitHub, and we showed that ConfigV can successfully detect configuration errors in these files. 

People involved in the project:

Mark Santolucito, Jialu Zhang

Recent Publications:

Mark Santolucito, Ennan Zhai, Rahul Dhodapkar, Aaron Shim, and Ruzica Piskac.

Synthesizing configuration file specifications with association rule

learning.

PACMPL, 1(OOPSLA):64:1--64:20, 2017.

[ bib | DOI | http ]