Research

overview

In the last two decades, we have witnessed a dramatic increase in the scale of chip designs. Today, we have multi-core system-on-a-chip design with billions of transistors and embedded processors that power everything from cell phones to cars. Recent advances in sciences and engineering have also led to the proliferation of cyber-physical systems. These are systems whose correct operation hinge on some complex interaction and integration of computational processes, physical processes and human activities. Drones, telesurgery robots, self-driving cars, body-sensor networks, smart dust, and building automation systems are all examples of cyber-physical systems. As the quality of our lives now depend on the correct functioning of these devices and systems, it is paramount to ensure that they are safe, reliable and secure.

Current Projects:

A.I. Safety

Artificial Intelligence (A.I.) is on the verge of ubiquity. The rise of AlphaGo and Watson suggests that A.I. might soon replace humans as the decision maker in many applications ranging from driving a car to making medical diagnosis. On the other hand, A.I. systems are also becoming increasing complex, and it is quite daunting that we are going to deploy these systems without a solid understanding of the complexities and their implications: why did the machine pick this decision? why not something else? when does it fail? how can we trust the machine if we don’t fully understand it? The somewhat dismal status quo is that A.I. is often used as the silver bullet or some magic black box in many applications. In this project, we will develop a combination of machine learning and computational proof techniques to (im)prove A.I. safety, explain A.I. decisions, and ultimately make A.I. systems more trustworthy. We are currently focusing on reinforcement learning problems and their applications to robots and human-robot interaction. 

Students: Weichao Zhou, Jiameng Fan, Panagiota Kiourti

Relevant publications:

  • Jiameng Fan and Wenchao LiSafety-Guided Deep Reinforcement Learning via Online Gaussian Process Estimation. International Conference on Learning Representation (ICLR), Workshop on Safe Machine Learning: Specification, Robustness, and Assurance, May 2019 (to appear).
  • Weichao Zhou and Wenchao Li. Safety-Aware Apprenticeship Learning. International Conference on Computer Aided Verification (CAV), July 2018.
  • Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli and Sanjit A. Seshia. Polynomial-Time Verification of PCTL Properties of MDPs with Convex UncertaintiesInternational Conference on Computer Aided Verification (CAV), July 2013. [Longer Tech. Report Version]

Secure Multi-Robot Systems

Recent trends in industrial automation indicate an ever-increasing adoption of autonomous mobile robots in production systems (the Kiva system in Amazon’s warehouses is a prime and large-scale example). In parallel, there is also an accelerating trend in large scale hacking events directed against high-profile companies (Equifax, Target, Walmart, Yahoo, Adobe, etc.) that have resulted in serious security breaches. Until now, these breaches have been limited to data, but it is easy to imagine that similar incidents in the near feature could take advantage of the increasing amount of automation to expand the attack reach to physical damages. It is therefore of critical importance to devise strategies that can preemptively address these threats. In this project, we propose a novel cyber-physical framework that uses planning and physical measurements to improve the security of networks of advanced robots against malicious cyber attacks that can compromise individual robots and sabotage the task of the group.

Student: Kacper Wardega

Relevant publications:

  • Resilience of Multi-Robot Systems to Physical Masquerade Attacks
    Kacper Wardega, Roberto Tron and Wenchao Li
    IEEE Workshop on the Internet of Safe Things (SafeThings), May 2019.
  • Masquerade Attack Detection Through Observation Planning for Multi-Robot Systems
    Kacper Wardega, Roberto Tron and Wenchao Li
    International Conference on Autonomous Agents and Multiagent Systems (AAMAS), May 2019.

Extensibility-Driven Design of Cyber-Physical Systems

extensibility

A longstanding problem in the design of CPSs is the inability and ineffectiveness in coping with software and hardware evolutions over the lifetime of a design or across multiple versions in the same product family. For example, Boeing 777 still uses the discontinued AMD 2950-microprocessor running a MS DOS file system for its Information Management System and Air Data Inertial Reference System. A fundamental reason for this is that small changes in resource usage can cause big and unexpected changes in timing and ultimately affect the functionality of the design. Engineers need to ensure that any changes not only (1) meet the constraints of the embedded platform such as schedulability and power constraints, but also (2) preserve the correctness of functional properties, many of which are affected by the platform changes. Systems that are designed without future changes in mind often incur significant redesign and re-verification cost, and reduced system availability and reliability. In this project, we treat extensibility as a first-class design objective, and aim to develop an extensibility-driven design (EDD) flow where different models and metrics of extensibility are considered jointly with other objectives at design time, further supported by new synthesis and verification tools that can reason about design updates efficiently. This is a collaborative project with Northwestern University, funded by NSF CPS.

Students: Jiameng Fan, Kacper Wardega

Relevant publications:

  • Formal Verification of Weakly-Hard Systems
    Chao Huang, Wenchao Li and Qi Zhu.
    International Conference on Hybrid Systems: Computation and Control (HSCC), April 2019.
  • Exploring Weakly-hard Paradigm for Networked Systems
    Chao Huang, Kacper Wardega, Wenchao Li and Qi Zhu.
    Workshop on Design Automation for CPS and IoT (DESTION), April 2019.
  • Qi Zhu, Hengyi Liang, Licong Zhang, Debayan Roy, Wenchao Li and Samarjit Chakraborty. Extensibility-Driven Automotive In-Vehicle Architecture DesignACM/IEEE Design Automation Conference (DAC), June 2017.
  • Bowen Zheng, Chung-Wei Lin, Hengyi Liang, Shinichi Shiraishi, Wenchao Li and Qi Zhu. Delay-Aware Design, Analysis and Verification of Intelligent Intersection ManagementIEEE International Conference on Smart Computing (SMARTCOMP), May 2017.
  • Sanjit A. Seshia, Shiyan Hu, Wenchao Li and Qi Zhu. Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities. IEEE Transactions on Computer-Aided Design of Circuits and Systems (TCAD), 2017.

Verification and Synthesis of Human-in-the-Loop Controllers

extensibility

This project is motivated by the emergence of automated driver-assistance systems and smart factories where human operators and industrial robots work together for the manufacturing and delivery of goods. A common theme in these settings is the deployment of control systems in safety-critical settings that involve the interaction of autonomous controllers with human operators. The correctness of such systems depends not only on the autonomous controller, but also on the actions of the human operator. Our previous work has provided a formalism for human-in-the-loop controllers, and explored automata-theoretic techniques for synthesizing provably safe controllers from high-level temporal logic specifications. In this project, we will build on these results and investigate novel verification and synthesis techniques for richer models (e.g., hybrid and probabilistic) and more complex modes of interactions.

Students: Jiameng Fan

Relevant publications:

  • Sanjit A. Seshia, Shiyan Hu, Wenchao Li and Qi Zhu. Design Automation of Cyber-Physical Systems: Challenges, Advances, and Opportunities. IEEE Transactions on Computer-Aided Design of Circuits and Systems (TCAD), September 2017.
  • Wenchao Li, Dorsa Sadigh, S. Shankar Sastry and Sanjit A. Seshia. Synthesis for Human-in-the-Loop Control Systems. International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), April 2014.
  • Dorsa Sadigh, Katherine Driggs-Campbell, Alberto Puggelli, Wenchao Li, Victor Shia, Ruzena Bajcsy, Alberto Sangiovanni-Vincentelli, S. Shankar Sastry and Sanjit A. Seshia. Data-Driven Probabilistic Modeling and Verification of Human Driver BehaviorAAAI Symposium on Modeling in Human Machine Systems: Challenges for Formal Verification, March 2014.

Dynamic Adaptive Embedded Software (DyAdEm)

adapt

Adaptivity is a fundamental requirement of embedded systems. These systems often face changes in computing platforms, resources available, physical environments, operator skills, and functional and performance requirements. This project aims to develop the principles and tools for designing adaptive embedded software. Specifically , we propose an integrative framework that can (1) learn about what and how much has changed (e.g., through runtime monitoring), (2) use language-based approaches (e.g., program transformation, program synthesis) to automatically adapt the system to these changes, and (3) regulate the adaptation through verification or an assurance case so that changing the system does not result in violation of safety requirements which can cause catastrophic failures. We will explore both online and offline approaches to these three problems. This is a collaborative project with SRI International, UC Berkeley, Honeywell Research Labs, funded under the DARPA BRASS program.

Student: Weichao Zhou, Jiameng Fan

Relevant publications:

  • Weichao Zhou and Wenchao Li. Safety-Aware Apprenticeship Learning. International Conference on Computer Aided Verification (CAV), July 2018.

Past Projects:

Programmer’s Assistant Synthesizing Code via Abstraction & Logical Inference (PASCALI)

PASCALI aims to offer a comprehensive range of capabilities for extracting, indexing, and applying semantic information from large code bases to support both individual programmers and software development teams in the task of constructing reliable, robust, and efficient software. In particular, we focus on developing techniques that can effectively and efficiently identify similar program fragments across software projects in a large code base. This is a collaborative project with SRI International, University of Waterloo, MIT, and University of Washington, funded under the DARPA MUSE program.

Student: Xiaoyue Wang

Relevant publications:

  • Wenchao Li, Hassen Saidi, Huascar Sanchez, Martin Schaf, and Pascal Schweitzer. Detecting Similar Programs via the Weisfeiler-Leman Graph KernelInternational Conference on Software Reuse (ICSR), June 2016.

Hardware Trojan Detection

Our earlier work on applying formal methods to reverse engineer circuit netlists helped pioneer the field of algorithmic reverse engineering of circuits. Our method can systematically derive a high-level description of a gate-level netlist and scales to a system-on-a-chip design with half a million gates. In addition, the reverse engineered description can help human analysts in navigating the sea of gates and identifying the extraneous and malicious circuitries (i.e. hardware Trojans).

Student: Yaqin Huang

Relevant publications:

  • Wenchao Li. Formal Methods for Reverse Engineering Gate-Level Netlists. Master Report, University of California, Berkeley. [Tech. Report Link]
  • Pramod Subramanyan, Nestan Tsiskaridze, Wenchao Li, Adria Gascon, Wei Yang Tan, Ashish Tiwari, Natarajan Shankar, Sanjit A. Seshia and Sharad Malik. Reverse Engineering Digital Circuits Using Structural and Functional AnalysesIEEE Transactions on Emerging Topics in Computing: Special Issue on Nanoscale Architectures for Hardware Security, Trust and Reliability (TETC), December 2013.
  • Wenchao Li, Adria Gascon, Pramod Subramanyan, Wei Yang Tan, Ashish Tiwari, Sharad Malik, Natarajan Shankar, Sanjit A. Seshia. WordRev: Finding Word-Level Structures in a Sea of Bit-Level GatesIEEE International Symposium on Hardware-Oriented Security and Trust (HOST), June 2013.
  • Wenchao Li, Zach Wasson and Sanjit A. Seshia. Reverse Engineering Circuits Using Behavioral Pattern MiningIEEE International Symposium on Hardware-Oriented Security and Trust (HOST), June 2012.