Workshop on Hyperproperties: Advances in Theory and Practice
18 October 2021 @ ATVA 2021
The study of hyperproperties has recently gained a great deal of attention in the formal methods, security, and cyber-physical systems communities. The goal of HYPER 2021 is to foster the exchange of ideas on the topic of hyperproperties between researchers from these diverse communities and to present and discuss recent advances in logical formalisms for specifying hyperproperties, algorithmic methodologies for the verification, synthesis, and runtime verification of hyperproperties, as well as applications related to both the fields of security and cyber-physical systems.
Invited Speakers
Tachio Terauchi: Constraint-based relational verification (recording; slides)
Waseda University, Japan
Tachio Terauchi is a professor in the Department of Computer Science and Engineering at Waseda University. He received his M.S. and Ph.D. from University of California Berkeley in 2004 and 2006, and B.S. from Columbia University in 2000, all in computer science. Before joining Waseda, he was a professor at JAIST from 2014 to 2017, an associate professor at Nagoya University from 2011 to 2014, and an assistant professor at Tohoku University from 2007 to 2011. Terauchi is interested in techniques for building reliable computational systems. His work draws from, and contributes to the areas of programming languages, program analysis, program verification, program synthesis, type systems, mathematical logic, automated deduction, and security.
Constraint-based relational verification
In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (CHCs) empower a wide range of verification techniques and tools, they lack the ability to express hyperproperties beyond k-safety such as generalized non-interference and co-termination. This talk describes a novel and fully automated constraint-based approach to relational verification. We first introduce a new class of predicate Constraint Satisfaction Problems called pfwCSP where constraints are represented as clauses modulo first-order theories over predicate variables of three kinds: ordinary, well-founded, or functional. This generalization over CHCs permits arbitrary (i.e., possibly non-Horn) clauses, well-foundedness constraints, functionality constraints, and is capable of expressing these relational verification problems. Our approach enables us to express and automatically verify problem instances that require non-trivial (i.e., non-sequential and non-lock-step) self-composition by automatically inferring appropriate schedulers (or alignment) that dictate when and which program copies move. To solve problems in this new language, we present a constraint solving method for pfwCSP based on stratified CounterExample-Guided Inductive Synthesis (CEGIS) of ordinary, well-founded, and functional predicates. We have implemented the proposed framework and obtained promising results on diverse relational verification problems that are beyond the scope of the previous verification frameworks.
This is a joint work with Hiroshi Unno (University of Tsukuba) and Eric Koskinen (Stevens Institute of Technology).
Orna Grumberg: Compositional model checking for multi-properties (recording)
Technion, Israel
Orna Grumberg is a Professor in the Computer Science Department at the Technion. She is a member of the Academia Europaea and an ACM fellow. She holds a Ph.D. from the Computer Science Department at the Technion, and an Honorary Doctorate from the Technical University of Munich.
Grumberg serves on the steering committee of the main conference on model checking - Computer-aided Verification (CAV). She serves on numerous program committees of leading conferences and on the editorial boards of two of the main journals in her field.
Grumberg is the co-author of the highly cited book "Model Checking", which is a main reference in the field of Formal Verification. Her work is published in leading conferences and is widely cited. Her work on counterexample-guided abstraction refinement (CEGAR) has won the CAV award.
Compositional model checking for multi-properties
Hyperproperties lift conventional trace properties in a way that describes how a system behaves in its entirety, and not just based on its individual traces. We generalize this notion to multi-properties, which describe the behavior of not just a single system, but of a set of systems, which we call a multi-model. We demonstrate the usefulness of our setting with practical examples. We show that model-checking multi-properties is equivalent to model-checking hyperproperties. However, our framework has the immediate advantage of being compositional.
We introduce sound and complete compositional proof rules for model-checking multi-properties, based on over- and under-approximations of the systems in the multi-model. We then describe methods of computing such approximations. The first is abstraction-refinement based, in which a coarse initial abstraction is continuously refined using counterexamples, until a suitable approximation is found. The second, tailored for models with finite traces, finds suitable approximations via the L* learning algorithm. Our methods can produce much smaller models than the original ones, and can therefore be used for accelerating model-checking for both multi-properties and hyperproperties.
This is a joint work with Ohad Goudsmid and Sarai Sheinvald.
Bernd Finkbeiner: Probabilistic Hyperproperties of Markov Decision Processes (recording)
CISPA Helmholtz Center for Information Security, Germany
Bernd Finkbeiner is a faculty member at the CISPA Helmholtz Center for Information Security and a professor for computer science at Saarland University. He obtained his Ph.D. in 2003 from Stanford University. Since 2003, he leads the Reactive Systems Group, which became part of CISPA in 2020. His research focus is the development of reliable guarantees for the safety and security of computer systems, including specification, program synthesis and repair, and static and dynamic verification.
Probabilistic Hyperproperties of Markov Decision Processes
Hyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as robotics and planning. While the model checking problem for PHL is in general undecidable, we provide methods both for proving and for refuting formulas from a fragment of the logic. The fragment includes many probabilistic hyperproperties of interest.
Sanjit A. Seshia: Formal Specification for Machine Learning Systems (recording; slides)
University of California, Berkeley, USA
Sanjit A. Seshia is a Professor in the Department of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He received an M.S. and Ph.D. in Computer Science from Carnegie Mellon University, and a B.Tech. in Computer Science and Engineering from the Indian Institute of Technology, Bombay. His research interests are in formal methods for dependable and secure computing, with a current focus on the areas of cyber-physical systems, computer security, machine learning, and robotics. He has made pioneering contributions to the areas of satisfiability modulo theories (SMT), SMT-based verification, and inductive program synthesis. He is co-author of a widely-used textbook on embedded, cyber-physical systems and has led the development of technologies for cyber-physical systems education based on formal methods. His awards and honors include a Presidential Early Career Award for Scientists and Engineers (PECASE), an Alfred P. Sloan Research Fellowship, the Frederick Emmons Terman Award for contributions to electrical engineering and computer science education, the Donald O. Pederson Best Paper Award for the IEEE Transactions on CAD, and the IEEE Technical Committee on Cyber-Physical Systems (TCCPS) Mid-Career Award. He is a Fellow of the ACM and the IEEE.
Formal Specification for Machine Learning Systems
The verification of machine learning (ML) components and systems is a topic of much interest.
In this talk, I will survey the landscape of specification of ML components and systems,
including properties such as robustness, fairness, and semantic invariance. Some of these
specifications are hyperproperties. I will discuss the many flavors that some of these properties
come in, a few techniques for verifying them, and directions for future research.
Jyotirmoy V. Deshmukh: Trust-aware Control for Multi-Agent Systems: a future arena for hyperproperties? (recording; slides)
University of Southern California, USA
Jyotirmoy V. Deshmukh is an assistant professor in the Department of Computer Science at the University of Southern California in Los Angeles, USA. Before joining USC, Jyo worked as a Principal Research Engineer in Toyota R&D. He received his Ph.D. degree from the University of Texas at Austin and was a post-doctoral fellow at the University of Pennsylvania. Dr. Deshmukh's research interest is in the broad area of analysis, design, security and trustworthiness, and synthesis of cyber-physical systems, including those that use machine learning and AI-based components.
Trust-aware Control for Multi-Agent Systems: a future arena for hyperproperties?
Autonomous multi-agent systems often operate in uncertain environments. The safety and performance of such systems is often dependent on their ability to coordinate the actions of individual agents. Many algorithms either optimistically view all participating agents as fully trustworthy, or provide theoretical limits under which the system can achieve fault tolerance (under pessimistic assumptions of agent failure). Many real world systems in contrast consist of agents who demonstrate behavior trends, i.e. certain agents are more likely to demonstrate reliable behavior, while other agents are demonstrably unreliable. Untrustworthiness of agents can be both due to benign failures in agents, malicious agents, or sporadic and adverse environment conditions. What are the precise and quantitative notions of trust we can introduce in such agents (and their environments)? How can we quantify the trustworthiness of individual agents using only observations of their behaviors? Furthermore, can we use trustworthiness to regulate system behavior to achieve better safety or performance guarantees? In this talk, we give tentative answers to these questions by introducing a notion of trust (inspired by an epistemic logic), a method to quantify trustworthiness, and trust-aware control methods. We observe that our notion of trustworthiness is a hyperproperty (in a statistical sense). We will formulate some open questions on exploring the connection between hyperproperties and our notion of trust, and the related verification and synthesis problems for achieving trustworthy multi-agent systems.
Borzoo Bonakdarpour: Controller Synthesis for Hyperproperties (recording; slides)
Michigan State University, USA
Borzoo Bonakdarpour is currently an Associate Professor of Computer Science
at Michigan State University. His research interests include formal methods and its
application in computer security, distributed systems, and cyber-physical systems.
He has published more than 90 articles and papers in top journals and conferences.
His work in these areas have received multiple best paper awards from highly
prestigious conferences, including, SRDS'17, SSS'14, and SIES'10. He chaired the
Technical Program Committee of the SRDS'20, SSS'16, and RV'14 conferences.
Controller Synthesis for Hyperproperties
This talk will discuss the problem of controller synthesis for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple execution traces. Hyperproperties can elegantly express information-flow policies like noninterference and observational determinism. The controller synthesis problem is to automatically design a controller for a plant that ensures satisfaction of a given specification in the presence of the environment or adversarial actions. The controller synthesis problem is decidable for HyperLTL specifications and finite-state plants and I will provide a rigorous complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general graphs.
Program
Monday, October 18, 2021; all times are in PDT (UTC-7).
