Program
Friday, September 28 | |
8:45 – 9:15 Breakfast & Registration | |
9:15 – 9:30 Opening Remarks | |
9:30 – 10:45 Session 1 – Keynote and Industry Talks         (Session chair: Cesare Tinelli) | |
9:30 – 10:30 |
Keynote talk: The goal of program synthesis is to allow programmers to specify the desired computation in intuitive ways without having to write traditional code. The classical synthesis problem is to find a program that meets a correctness specification given as a logical formula. Recent work on synthesis and optimization illustrates many potential benefits of allowing the user to supplement the logical specification with a syntactic template that constrains the space of allowed implementations. The formulation of the syntax-guided synthesis problem (SyGuS) is aimed at standardizing the core computational problem common to these proposals in a logical framework. In this talk, we first describe how a wide range of problems such as automatic synthesis of loop invariants, program optimization, program repair to defend against timing-based attacks, and learning programs from examples can be formalized as SyGuS instances. We then explain the counterexample-guided-inductive-synthesis strategy for solving the SyGuS problem, its different instantiations, and experimental evaluation over benchmarks from a variety of applications. We conclude by discussing how program synthesis and machine learning can play mutually beneficial roles to transform the way we build software. Rajeev Alur is Zisman Family Professor of Computer and Information Science at University of Pennsylvania. He obtained his bachelor's degree in computer science from IIT Kanpur and PhD in computer science from Stanford University. His research is focused on formal methods for system design, and spans theoretical computer science, software verification and synthesis, and cyber-physical systems. He is a Fellow of the AAAS, ACM, and IEEE, an Alfred P. Sloan Faculty Fellow, and a Simons Investigator. He was awarded the inaugural CAV (Computer-Aided Verification) award, ACM/IEEE Logic in Computer Science (LICS) Test-of-Time award and the inaugural ACM SIGLOG Alonzo Church award for his work on timed automata. He is the author of the textbook Principles of Cyber-Physical Systems (MIT Press, 2015), and the lead PI of the NSF Expeditions in Computing center ExCAPE (Expeditions in Computer Augmented Program Engineering). |
10:30 – 10:45 |
Industry talk: |
10:45 – 11:30 Coffee Break | |
11:30 – 12:30 Session 2 – Research Talks         (Session chair: Haniel Barbosa) | |
11:30 – 11:50 |
Automatic Data Structure Repair using Separation Logic
(slides)
Software systems are often shipped and deployed with both known and unknown bugs. On-the-fly program repairs, which handle runtime errors and allow programs to continue successfully, can help software reliability, e.g., by dealing with inconsistent or corrupted data without interrupting the running program. We report on our work-in-progress that repairs data structure using sepa- ration logic. Our technique, inspired by existing works on specification- based repair, takes as input a specification written in a separation logic formula and a concrete data structure that fails that specification, and per- forms on-the-fly repair to make the data conforms with the specification. The use of separation logic allows us to compactly and precisely rep- resent desired properties of data structures and use existing analyses in separation logic to detect and repair bugs in complex data structures. We have developed a prototype, called STARFIX, to repair invalid Java data structures violating given specifications in separation logic. Preliminary results show that tool can efficiently detect and repair inconsistent data structures including lists and trees. |
11:50 – 12:10 |
SymCerts: Practical Symbolic Execution For Exposing Noncompliance in X.509 Certificate Validation Implementations
(slides)
The X.509 Public-Key Infrastructure has long been used in the SSL/TLS protocol to achieve authentication. A recent trend of Internet-of-Things (IoT) systems employing small footprint SSL/TLS libraries for secure communication has further propelled its prominence. The security guarantees provided by X.509 hinge on the assumption that the underlying implementation rigorously scrutinizes X.509 certificate chains, and accepts only the valid ones. Noncompliant implementations of X.509 can potentially lead to attacks and/or interoperability issues. In the literature, black-box fuzzing has been used to find flaws in X.509 validation implementations; fuzzing, however, cannot guarantee coverage and thus severe flaws may remain undetected. To thoroughly analyze X.509 implementations in small footprint SSL/TLS libraries, this paper takes the complementary approach of using symbolic execution. We observe that symbolic execution, a technique proven to be effective in finding software implementation flaws, can also be leveraged to expose noncompliance in X.509 implementations. Directly applying an off-the-shelf symbolic execution engine on SSL/TLS libraries is, however, not practical due to the problem of path explosion. To this end, we propose the use of SymCerts, which are X.509 certificate chains carefully constructed with a mixture of symbolic and concrete values. Utilizing SymCerts and some domain-specific optimizations, we symbolically execute the certificate chain validation code of each library and extract path constraints describing its accepting and rejecting certificate universes. These path constraints help us identify missing checks in different libraries. For exposing subtle but intricate noncompliance with X.509 standard, we cross-validate the constraints extracted from different libraries to find further implementation flaws. Our analysis of 9 small footprint X.509 implementations has uncovered 48 instances of noncompliance. Findings and suggestions provided by us have already been incorporated by developers into newer versions of their libraries. |
12:10 – 12:30 |
Relational Constraint Solving in SMT
(slides)
Relational logic is useful for reasoning about computational problems with relational structures, including high-level system design, architectural configurations of network systems, ontologies, and verification of programs with linked data structures. In this talk, we present a modular extension of an earlier calculus for the theory of finite sets to a theory of finite relations with such operations as transpose, product, join, and transitive closure. We implement this extension as a theory solver of the SMT solver CVC4. Combining this new solver with the finite model finding features of CVC4 enables several compelling use cases, such as Alloy and Web Ontology Language (OWL) models. We provide an initial evaluation of our solver on a number of Alloy and OWL models which shows promising results. |
12:30 – 14:00 Lunch Break (*) | |
14:00 – 14:30 Session 4 – Speed Meeting with Industry         (Session chair: Omar Chowdhury) | |
14:30 – 15:30 Session 3 – Research Talks         (Session chair: Fareed Arif) | |
14:30 – 14:50 |
LTEInspector: A Systematic Approach for Adversarial Testing of 4G LTE
In this work, we investigate the security and privacy of the three critical procedures of the 4G LTE protocol (i.e., attach, detach, and paging), and in the process, uncover potential design flaws of the protocol and unsafe practices employed by the stakeholders. For exposing vulnerabilities, we propose a model-based testing approach LTEInspector which lazily combines a symbolic model checker and a cryptographic protocol verifier in the symbolic attacker model. Using LTEInspector, we have uncovered 10 new attacks along with 9 prior attacks, categorized into three abstract classes (i.e., security, user privacy, and disruption of service), in the three procedures of 4G LTE. Notable among our findings is the authentication relay attack that enables an adversary to spoof the location of a legitimate user to the core network without possessing appropriate credentials. To ensure that the exposed attacks pose real threats and are indeed realizable in practice, we have validated 8 of the 10 new attacks and their accompanying adversarial assumptions through experimentation in a real testbed. |
14:50 – 15:10 |
Embedding Runtime Verification in Space Robotics
(slides)
Robotic systems operating in hazardous or safety-critical environments necessitate strict requirements for fault-detection. They must be able to detect faults and disambiguate between corrective actions, which is a challenge when temporal context is required for disambiguation. Robonaut 2, onboard the International Space Station, exhibits a common fault case with several potential corrective actions that require operator intervention to resolve. Real-time fault disambiguation must be added in the limited remaining resources. By installing a system health monitor on spare FPGA fabric at the actuator, increased sensor level visibility is available for diagnostic reasoning. We extend R2U2, an online runtime verification framework, for this monitoring because it is uniquely suited to fit in this resource constrained environment. We overview the challenges of analyzing the Robonaut command and data bus, and present preliminary work on real-time detection and disambiguation of faults in Robonaut 2's knee joint. |
15:10 – 15:30 |
Compositional Program Analysis using Max-SMT
Recent developments on SMT solvers have become crucial to make program analysis techniques effective in practice. Despite their success, scalability is still an issue when applying these methods to large fragments of code. In order to address this problem, we propose a template-based (also known as constraint-based) approach using Max-SMT solvers. In particular, we present an automated compositional program verification method for safety properties based on conditional inductive invariants. Our bottom-up verification technique synthesizes and propagates preconditions of small program parts as postconditions for preceding parts. The technique has been implemented within the VeryMax tool which currently can check safety, reachability, and termination properties of C++ code. |
15:30 – 16:10 Coffee Break | |
16:10 – 17:30 Session 5 – Research Talks         (Session chair: Andrew Reynolds) | |
16:10 – 16:30 |
Runtime Model Predictive Verification on Embedded Platforms
(slides)
Mission-Time Linear Temporal Logic (\mltl) specifies requirements over the future of an execution trace relative to the current time; it is specialized for describing missions by adding integer time-bounds to the temporal operators of LTL. Runtime verification continuously evaluates whether an MLTL specification $\phi$ is satisfied during the current mission. Due to the future-time nature of the logic, we may not always have sufficient information to determine whether $\phi$ holds at the current time, yet we need to evaluate this as quickly as possible to enable mitigation actions in case of a subsystem failure. To enable early-as-necessary mitigation triggering, we combine runtime verification with a model of the target system to predict future states. We propose the concept of Model Predictive Runtime Verification (MPRV) and design an embedded solution for MPRV with bounded resource generation to enable stream-based, online, real-time verification. Our solution builds on the state-of-art runtime verification tool \textsc{R2U2}. We contribute (1) a formal definition of MPRV; (2) an algorithm for MPRV on embedded platforms with limited resources; and (3) an implementation of MPRV for safety-critical control systems. |
16:30 – 16:50 |
SMT-based Constraint Answer Set Solver EZSMT
(slides)
Constraint answer set programming integrates answer set programming with constraint processing. The EZSMT system is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search, while providing a high-level logic programming interface. |
16:50 – 17:10 |
Projector: an automatic logic program rewriting tool for better performance
(slides)
Answer set programming is a popular constraint programming paradigm that has seen wide use across various industry applications. However, logic programs under answer set semantics often require careful design and nontrivial expertise from a programmer to obtain satisfactory solving times. In order to reduce this burden on a software engineer we propose an automated rewriting technique for non-ground logic programs that we implement in a system PROJECTOR. This technique allows us to split a single logic rule into multiple rules, so that the number of variables present in each new rule is smaller than that of an original one. This often translates into smaller ground programs and better solving times. We conducted rigorous experimental analysis on an answer set programming-based natural language parser called ASPCCG using three encodings representing increased levels of human optimization. Our results show that applying system PROJECTOR to a logic program can improve its performance, even after significant human-performed optimizations. |
17:10 – 17:30 |
A Temporal Logic for Probabilistic Hyperproperties
(slides)
Hyperproperties have shown to be a useful formalism to express and reason about information-flow security. We propose a new temporal logic for probabilistic hyperproperties that express quantitative dependencies among independent executions. The standard temporal logics for probabilistic systems, i.e., PCTL and PCTL* can refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic, HyperPCTL, adds explicit and simultaneous quantification over multiple traces to PCTL. A model checking algorithm for the proposed logic is also introduced for discrete-time Markov chains. |
17:30 – 18:30 Free Time | |
18:30 – 20:00 Dinner (*) |
(*) Lunch and dinner are on your own. Student participants will be encouraged to go to dinner in groups formed by the organizers.
Saturday, September 29 | |
09:00 – 09:30 Breakfast | |
09:30 – 10:30 Session 1 – Research Talks         (Session chair: Fareed Arif) | |
09:30 – 09:50 |
Hierarchical Abstractions for Reachability Analysis of Probabilistic Hybrid Systems
We consider the problem of reachability analysis of probabilistic hybrid systems (PHS) which model discrete, continuous and probabilistic behaviors. The discrete and probabilistic dynamics are captured using finite state Markov decision processes (MDP), and the continuous dynamics are modeled by annotating the states of the MDP with differential equations/inclusions. We focus on linear dynamics and propose a two tier abstraction for computing bounds on the probability of reachability, wherein the first step performs dynamics simplification by applying hybridization such that the resulting dynamics is a polyhedral inclusion and the second step constructs a finite state markov decision process that abstracts the polyhedral inclusion dynamics. This two-tier abstraction is computationally simpler than applying predicate abstraction directly on the linear PHS. We have implemented the abstraction and analysis algorithms in a Python toolbox. Our experimental results demonstrate the feasibility of the approach. |
09:50 – 10:10 |
BioSIMP: A Process for Sampling and Inference in Biological Organisms
(slides)
Years of research in software engineering has given us novel ways to reason about, test, and predict the behavior of complex software systems that contain hundreds of thousands of lines of code. Many of these techniques have been inspired by nature such as genetic algorithms, swarm intelligence, and ant colony optimization. We reverse the direction and present BioSIMP, a process that models, infers invariants, and predicts the behavior of biological organisms to aid in the emerging field of systems biology. It utilizes techniques from testing and modeling of highly-configurable software systems. Like configurable systems, a biological organism’s source code (metabolic model) contains both common and variable elements (reactions) that are executed only under particular configurations (environmental conditions) and these directly impact an organism’s observable behavior. Using both experimental and simulation data we show that BioSIMP can find important environmental factors in two microbial organisms. However, in order to fully reason about the complexity of biological systems and validate simulated models, we will need to extend existing (or create new) software engineering techniques. |
10:10 – 10:30 |
When Human Intuition Fails: Using Formal Methods to Find an Error in the "Proof" of a Multi-Agent Protocol
(slides)
Designing protocols for multi-agent interaction that achieve the desired behavior is a challenging and error-prone process. Proofs of protocol correctness rely on human intuition and require significant effort to develop. Even then, proofs can have mistakes that may go unnoticed after peer review, modeling and simulation, and testing of the resulting system. The potential for errors can be reduced through the use of formal methods, i.e. automated or semi-automated mathematically rigorous tools and techniques for system specification, design, and verification. In this work, we applied a type of formal method called model checking to a previously published decentralized protocol for coordinating a surveillance task across multiple unmanned aerial vehicles. The original publication provides a compelling proof of correctness, along with extensive simulation results to support it. However, our analysis found an error in one of the lemmas used in the proof. In this presentation, we provide an overview of the protocol, the original "proof" of correctness, the model checking approach we used to analyze the protocol, the counterexample returned by the model checker, and the insight this counterexample provides into why the original lemma was incorrect. We also discuss how the formal modeling process revealed that certain aspects of the protocol were underspecified, and what future efforts would be needed to fully verify it with formal methods. |
10:30 – 11:10 Coffee Break | |
11:10 – 12:20 Session 2 – Research Talks         (Session chair: Daniel Larraz) | |
11:10 – 11:30 |
Runtime Fault Detection in Programmed Molecular Systems
Chemical reaction networks (CRNs) are an important paradigm for molecular computation and process control in the emerging field of DNA nanotechnology. We present a formally verified molecular "watchdog timer" CRN module that monitors a regular "heartbeat" signal and raises an alarm if that signal is absent. We specify our system requirements in continuous stochastic logic (CSL), a variation of CTL that allows for transition probabilities, probabilistic quantifiers, and continuous-time durations. Our CSL specification is a tree-structured goal diagram, with model-checked leaf nodes and the full specification at the root. We use the Isabelle/HOL theorem proving environment to verify our goal diagram: i.e., to prove that the leaf nodes imply the complete specification. We have generated a small set of general CSL lemmas with accompanying mathematical proofs; with these foundational lemmas as input axioms, we use Isabelle to verify each node of the goal diagram tree. This is joint work with Samuel J. Ellis, Titus H. Klinge, James I. Lathrop, Jack H. Lutz, Robyn R. Lutz, Andrew S. Miner. |
11:30 – 11:40 |
EvoAlloy: Evolutionary analysis of Alloy specifications
(slides)
Formal methods use mathematical notations and logical reasoning to precisely define a program’s specifications, from which we can instantiate valid instances of a system. With these techniques, we can perform a multitude of tasks to check system dependability. Despite the existence of many automated tools including ones considered lightweight, they still lack a strong adoption in practice. At the crux of this problem, is scalability and applicability to large real-world applications. In this paper, we show how to relax the completeness guarantee without much loss, since soundness is maintained. We have extended a popular lightweight analysis, Alloy, with a genetic algorithm. Our new tool, EvoAlloy, works at the level of finite relations generated by Kodkod and evolves the chromosomes based on the failed constraints. In a feasibility study, we demonstrate that we can ndfi solutions to a set of specifications beyond the scope where traditional Alloy fails. While small specifications take longer with EvoAlloy, the scalability means we can handle larger specifications. Our future vision is that when specifications are small we can maintain both soundness and completeness, but when this fails, EvoAlloy can switch to its genetic algorithm. |
11:40 – 12:00 |
Generating System-Agnostic Runtime Verification Benchmarks from MLTL Formulas
(slides)
As the complexity of autonomous systems increases, Runtime Verification (RV) has increasingly become a critical component in safety-critical domains. Ensuring the correctness of these components necessitates realistic system benchmarks, an area of research that continues to be lacking. To support this need, we propose a technique for system-agnostic benchmark generation via SAT and SMT. We first propose the ""naive approach”, using a direct encoding to Boolean SAT, for generating system traces over propositional variables. We then present promising nascent work on a satisfiability and trace-generation framework, integrating techniques for evaluating conflicts over temporal logic formulas with existing SMT solvers. |
12:00 – 12:20 |
Combining data-driven and symbolic reasoning for Invariant Synthesis in SMT
(slides)
In program verification one often relies on the derivation of invariants for satisfying safety specifications. They constrain the set of reachable program states and can be used to show that no error state can be reached. Classic techniques for invariant generation rely on interpolation/IC3, but recently data-driven and program synthesis approaches have been able to compete with the state-of-the-art. In this talk we report our work-in-progress on a new framework for invariant synthesis in SMT. We combine decision tree learning with symbolic reasoning to reduce the dependence on heuristics, in a framework combining counter-example guided inductive synthesis (CEGIS) and divide-and-conquer techniques. Our preliminary results show that our approach is competitive with the state-of-the-art in invariant synthesis. |
12:20 – 12:30 Concluding Remarks |