Security of Cyber-Physical Systems
by P. R. Kumar (Texas A&M University)
CPS Test Beds
The Internet of Everything and Industry 4.0 revolutions
by Ram D. Sriram (US National Institute of Standards and Technology – NIST)
The Internet, which has spanned several networks in a wide variety of domains, is having a significant impact on every aspect of our lives. These networks are currently being extended to have significant sensing capabilities, with the evolution of the Internet of Things (IoT). With additional control we are entering the era of cyber-physical systems (CPS). In the near future the networks will go beyond physically linked computers to include multimodal-information from biological, cognitive, semantic, and social networks. This paradigm shift will involve symbiotic networks of people (social networks), smart devices, and smart phones or mobile personal computing and communication devices that will form smart net-centric systems and societies (SNSS), which is also known as Internet of Everything in the U.S. and Industry 4.0 in Europe. These devices – and the network – will be constantly sensing, monitoring, interpreting, and controlling the environment. In this talk, I will provide a unified framework for Internet of Things, cyber-physical systems, and smart networked systems and societies, along with a brief introduction to Industry 4.0. I will discuss the various research issues and representative projects at NIST.
Category theory for CPS
by Eswaran Subramanian (Carnegie Mellon University and US National Institute of Standards and Technology – NIST)
The study of cyber physical systems (CPS) requires consideration of two distinct types of composition problems. First we must integrate existing approaches for analyzing physical dynamics and computational behavior (not to mention probability). This is essentially definitional for CPS. Second, most CPS are designed to interact via network processes, and this forces us to consider systems-of-systems composition, where one CPS (a car) is both a composed system in its own right (from engine, brakes, etc.) and a component of a larger system (traffic flow). We will motivate these two types of composition with examples from medicine, smart cities and the industrial internet.
We will argue that category theory (CT), a branch of abstract mathematics, provides the means to address both of these concerns. CT has played a unifying role in mathematics, providing a common language for studying other structures such as state charts and dynamical systems. This provides a common context in which the different methods required for CPS can interact. At the level of systems, CT provides a detailed specification for building compositional systems and analyses. Above all, CT has the potential to provide a rigorous and systematic foundation for engineering of CPS.
Federated experiment design using the Universal CPS Environment for Federation (UCEF)
by Thomas Roth (US National Institute of Standards and Technology – NIST)
The U.S. National Institute of Standards and Technology (NIST), in partnership with the Institute for Software Integrated Systems at Vanderbilt University, has developed an open-source tool to expedite the design and implementation of cyber-physical systems (CPS) experiments. This tool, called the Universal CPS Environment for Federation (UCEF), integrates diverse programming languages and software simulators into a common graphical modeling environment using the IEEE 1516 High Level Architecture (HLA) standard.
UCEF readily enables the co-simulation of heterogeneous hardware and software resources over large geographical distances for multiple CPS domains. This presentation will introduce the UCEF architecture and outline the capabilities of its current alpha release.
Control and Optimization for Smart Grids
Virtual energy storage for solar and wind power with distributed coordination of smart devices
by Prabir Barooah (University of Florida)
As we move away from fossil fuels toward renewable energy sources such as solar and wind, inexpensive energy storage technologies are required. This is so since renewable energy sources, such as solar and wind, are intermittent. An alternative to batteries – which are quite expensive – is “smart loads”, such as air conditioners equipped with computation and communication capability. With appropriate software, the power consumption of air conditioning – and many other loads – can be varied around a baseline. This variation is analogous to the charging and discharging of a battery. Loads equipped with such intelligence have the potential to provide a vast and inexpensive source of energy storage.
Two principal challenges in creating a reliable virtual battery from millions of consumer loads include (1) maintaining consumers’ Quality of Service (QoS) within strict bounds, and (2) coordinating the actions of loads with minimal communication to ensure accurate reference tracking by the aggregate. This talk describes our work in addressing these two challenges. Key ideas that underpin the proposed methodology include spectral decomposition for QoS-abiding resource classification, communication-free distributed control that exploits physical-signaling for coordination, and randomized control for reducing combinatorial problems to convex ones.
Anupama Kowli (IIT Bombay)
Analytics opportunities in the energy sector
by Vijay Arya (IBM India Research Labs)
The energy sector is on the cusp of a digital transformation. Utilities worldwide are undertaking advanced metering and smart grid initiatives to improve energy efficiency, reduce carbon footprint, and integrate distributed energy resources while improving the overall efficiency and reliability of the power system. This poses a number of interesting analytics and optimization challenges.
This presentation will provide a glimpse of real industry problems and solution covering different areas of the energy sector including distribution networks, renewable energy, demand response, unit commitment, storage, and microgrids.
CPS Security and Anomaly Detection
On the resilience of cyber-physical systems
by Bruno Sinopoli (Carnegie Mellon University)
Recent advances in sensing, communication and computing allow cost effective deployment in the physical world of large-scale networks of sensors and actuators, enabling fine grain monitoring and control of a multitude of physical systems and infrastructures. Such systems, called cyber-physical, lie at the intersection of control, communication and computing. The close interplay among these fields renders independent design of the control, communication, and computing subsystems a risky approach, as separation of concerns does not constitute a realistic assumption in real world scenarios. It is therefore imperative to derive new models and methodologies to allow analysis and design of robust and secure cyber-physical systems (CPS). In this talk I will present an overview of recent research on the topic and discuss future directions.
Anomaly detection for securing critical infrastructure using big data analytics
by Amir Averbuch (Tel Aviv University)
Cyber security for protecting critical infrastructure, which consists of energy, transportation, financial institutions, telecommunications corporations, are all examples for the need to have anomaly detection that operates on high dimensional big data to find new and unseen types of threats and disturbances including advanced persistent threats (APTs). Several factors make anomaly detection in High Dimensional Big Data (HDBD) a challenging task: learning HDBD distributions, the boundary between normal and abnormal behavior is sometimes vague, many scenarios exhibit data that evolve in time which means that what is currently considered as a normal behavior might be abnormal in future and vice versa and there is a need to employ many different domain experts. This may cause high false alarms rate.
In this talk, we focus on describing an automatic and unsupervised anomaly detection methods that do not necessitate domain expertise, signatures, rules, patterns or features semantics understanding and propose several new methodologies for anomaly detection for protecting critical infrastructures that are data driven based methods. Anomalies can be originated from either a cyber-attack/threat or operational malfunction, or both. We will show that cyber threat and operational malfunction are converging into a single detection paradigm.
Cyber security of cyber-physical critical infrastructures: A case for a schizoid design approach
by Sandeep Shukla (IIT Kanpur)
In the past, the design of cyber-physical systems (CPS) required a model based engineering approach – a design methodology consisting of physics based mathematical modeling of the physical system, and a control theoretic modeling of the control system put together in a formal or semi-formal framework. The designers would start from an abstract model, and refine it down to an implementation model in several steps, either formally or informally. The implementation model is then validated for functional correctness, and satisfaction of performance, real-time schedulability goals. Functional Safety, robustness to input assumptions, reliability under fault assumptions, and resilience to unknown adversities were considered as important design goals for safety-critical CPS.
With the increased use of networked distributed control of large and geographically distributed critical infrastructures such as smart grid and the exposure to cyber-attacks ushered in by the IP-convergence phenomenon – designers must now consider cyber-security and cyber defense as first class design objectives. However, in order to do so, designers have to don a dual personality – while designing for robustness, reliability, functional safety – a model driven engineering approach would work – for designing for cyber-security and defense, the designer has to enter the mindset of a malicious attacker. For instance, one has to consider the various observations or sampling points of the system (e.g. sensors to read or sample the physical environment), and think how an attacker might compromise the unobservability of those points without authentication, and what knowledge of the system dynamics or the control mechanism of the system might be actually reconstructed by the attacker. One also has to consider the actuation points of the system, and ponder the least number of such actuation points the attacker has to take over in order to disrupt the dynamics of the system enough to create considerable damage. One must envision how to obfuscate the dynamics of the system even when certain sensing or actuation points are compromised. Also, it is known that a large percentage of attacks are induced by insider or a collusion of internal and external agents. Thus, perimeter defense alone cannot defend the system. In such cases, the symptoms of an ongoing attack in the dynamics of the system itself must be discerned continually.
This approach to viewing the system from an adversarial position requires us to topple the design paradigm over its head, and we will need to build models from data, and not just generate data from models. The designer must observe a system in action – even through partial observations, and construct a model close enough to the real system model – and then use the partial access to create damages to the because the approximate model allows her to do so. Almost like a schizophrenic duality, the engineer also has to wear the designers hat, and consider a game in which the observations are obfuscated enough to render it impossible for an attacker to build any useful model to induce clever attacks. The designer has to worry if she can construct from unobfuscated observations, a dynamics quickly enough so that the difference between the expected dynamics and the real dynamics can trigger alarms to alert the system administrators. In this talk, while discussing this view of system design, we will also talk about VSCADA – a virtual distributed SCADA lab we created for modeling SCADA systems for critical infrastructures, and how to use such a virtual lab completely implemented in simulation – to achieve the cyber security and cyber defense objectives of critical infrastructures – through attack injections, attack detection, and experiments on new defense mechanisms. We will also discuss the real SCADA test bed we are building at our center for cyber security of critical infrastructures at IIT Kanpur.
Autonomous Systems and Robotics
Hemendra Arya (IIT Bombay)
Automated Task and Motion Plan Generation for Multi-Robot Systems from Complex Specifications
by Indranil Saha (IIT Kanpur)
Autonomous multi-robot systems have tremendous potential to be useful in various applications including search and rescue, surveillance, law enforcement, precision agriculture and warehouse management. Given a high-level specification for a multi-robot system, it is technically challenging to determine the responsibilities of the individual robots and a plan for them to execute their responsibilities safely in such a way that the given specification is satisfied optimally. In this talk, I will present a task and motion planning framework for multi-robot systems where the desired behavior of a group of robots is specified using a set of linear temporal logic (LTL) properties. The method for generating task and motion plan for the robots in this framework relies on a library of motion primitives for the robots, using which we formulate the planning problem as an SMT solving problem and use an off-the-shelf SMT solver to generate safe trajectories for the robots. We will discuss various challenges that we face in scaling up our solution to large-scale multi-robot systems and describe how we address some of these challenges. As an example application, we will show how the multi-robot coverage problem can be effectively solved in our framework.
Software Engineering for CPS
Exploiting fog and edge resources for cloud-hosted cyber-physical system services
by Aniruddha Gokhale (Vanderbilt University)
Despite the known benefits of hosting cloud-based services, the longer and often unpredictable end-to-end network latencies between the end user and the cloud can be detrimental to the response time requirements of the interactive cloud-hosted applications. Existing efforts that exploit edge/fog technology to migrate services closer to clients in order to improve response times do not fully resolve this problem as they do not focus on performance and interference issues at the migrated locations. This talk proposes INDICES framework that addresses these limitations by providing a novel solution that determines when and to which MDC a service should be migrated to and thus provides the desired performance. Empirical results validating our claims are presented using a setup comprising a centralized cloud and MDCs composed of heterogeneous hardware.
Vinai Sundaram (SensorHound)
Hybrid Systems and Control
Formal synthesis of control strategies for dynamical systems
by Calin A. Belta (Boston University)
In control theory, complex models of physical processes, such as systems of differential equations, are analyzed or controlled from simple specifications, such as stability and set invariance. In formal methods, rich specifications, such as formulae of temporal logics, are checked against simple models of software programs and digital circuits, such as finite transition systems. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications.
In this talk, I will discuss a set of approaches to formal synthesis of control strategies for dynamical systems from temporal logic specifications. I will first show how automata games for finite systems can be extended to obtain conservative control strategies for low dimensional linear and multilinear dynamical systems. I will then present several methods to reduce conservativeness and improve the scalability of the control synthesis algorithms for more general classes of dynamics.
I will illustrate the usefulness of these approaches with examples from robotics and traffic control.
Venkatrao Ryali (GE Global Research)
Cross-domain solutions from a connected company
by Stefan Abendroth (Bosch)
As a connected company with strong roots in different domains, Bosch’s objective in a connected world is not only to enable new applications, but to achieve a unique user experience with strong requirements regarding safety, security, quality of service, and interoperability.
In this talk, I present tangible examples of how new solutions can be brought into traditional domains in order to combine the best of both worlds: Flexible services enabled by communication networks on the one hand, dependable systems for demanding applications on the other hand. (1) With physical layer security technologies, we provide plug&secure communications both in wireless sensor networks and in vehicles. (2) New wireless technologies enable ultra-reliable, low latency industrial applications. (3) Service-oriented communication brings cloud based functions deeply into the vehicle.
Formal verification of robustness properties of hybrid control systems
by Pavithra Prabhakar (Kansas State University)
Cyber-physical systems (CPSs) consist of complex systems that combine control, computation and communication to achieve sophisticated functionalities as in autonomous driving in driverless cars and automated load balancing in smart grids. The safety criticality of these systems demands strong guarantees about their correct functioning. Formal verification is an area of computer science that deals with rigorous and automated methods for correctness analysis based on mathematical models of systems and correctness specifications. In this talk, we present an overview of our work on formal verification techniques for cyber-physical systems analysis using the framework of hybrid systems. Hybrid systems capture an important feature of CPSs, namely, mixed discrete-continuous behaviors that arise due to the interaction of complex digital control software (discrete elements) with physical systems (continuous elements).
We will focus on the formal verification of a fundamental property in control design, namely, stability. Stability is a robustness property that capture notions such as small perturbations to the initial state or input to a system result in only small variations in the behavior of the system. We will present a novel algorithmic approach to stability analysis based on model-checking and abstraction-refinement techniques. We highlight the technical challenges in the development of an algorithmic framework for stability analysis owing to the robustness aspect. We will present experimental results using our tool AVERIST (Algorithmic VERifier for STability), that illustrate the practical benefits of the algorithmic approach as compared to well-known deductive methods for automated verification of stability based on Lyapunov functions. Finally, we will present some future research directions including automated design of hybrid control systems and formal analysis of hybrid systems in the presence of uncertainties.