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.
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.
Orna Grumberg: Compositional model checking for multi-properties (recording)
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.
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.
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 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.
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 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.
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 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.
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.
Monday, October 18, 2021; all times are in PDT (UTC-7).
|7:15||Tachio Terauchi (recording; slides)|
|Constraint-based relational verification|
|8:00||Orna Grumberg (recording)|
|Compositional model checking for multi-properties|
|9:00||Bernd Finkbeiner (recording)|
|Probabilistic Hyperproperties of Markov Decision Processes|
|9:45||Sanjit A. Seshia (recording; slides)|
|Formal Specification for Machine Learning Systems|
|10:45||Jyotirmoy V. Deshmukh (recording; slides)|
|Trust-aware Control for Multi-Agent Systems: a future arena for hyperproperties?|
|11:30||Borzoo Bonakdarpour (recording; slides)|
|Controller Synthesis for Hyperproperties|
|12:30||Panel discussion (recording)|
Please register via the ATVA registration site. Note that workshop-only registration is free.
Recordings of the HYPER 2021 talks and panel discussion are available on YouTube.