Open Access. Powered by Scholars. Published by Universities.®

Engineering Commons

Open Access. Powered by Scholars. Published by Universities.®

2019

Series

PDF

Computer Engineering

CPS Formal Methods

Articles 1 - 9 of 9

Full-Text Articles in Engineering

Detecting Security Leaks In Hybrid Systems With Information Flow Analysis, Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, Rajeev Alur Oct 2019

Detecting Security Leaks In Hybrid Systems With Information Flow Analysis, Luan Viet Nguyen, Gautam Mohan, James Weimer, Oleg Sokolsky, Insup Lee, Rajeev Alur

Departmental Papers (CIS)

Information flow analysis is an effective way to check useful security properties, such as whether secret information can leak to adversaries. Despite being widely investigated in the realm of programming languages, information-flow- based security analysis has not been widely studied in the domain of cyber-physical systems (CPS). CPS provide interesting challenges to traditional type-based techniques, as they model mixed discrete-continuous behaviors and are usually expressed as a composition of state machines. In this paper, we propose a lightweight static analysis methodology that enables information security properties for CPS models.We introduce a set of security rules for hybrid automata that ...


Overhead-Aware Deployment Of Runtime Monitors, Teng Zhang, Greg Eakman, Insup Lee, Oleg Sokolsky Oct 2019

Overhead-Aware Deployment Of Runtime Monitors, Teng Zhang, Greg Eakman, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

One important issue needed to be handled when applying runtime verification is the time overhead introduced by online monitors. According to how monitors are deployed with the system to be monitored, the overhead may come from the execution of monitoring logic or asynchronous communication. In this paper, we present a method for deciding how to deploy runtime monitors with awareness of minimizing the overhead. We first propose a parametric model to estimate the overhead given the prior knowledge on the distribution of incoming events and the time cost of sending a message and executing monitoring logic. Then, we will discuss ...


A Retrospective Look At The Monitoring And Checking (Mac) Framework, Sampath Kannan, Moonzoo Kim, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan Oct 2019

A Retrospective Look At The Monitoring And Checking (Mac) Framework, Sampath Kannan, Moonzoo Kim, Insup Lee, Oleg Sokolsky, Mahesh Viswanathan

Departmental Papers (CIS)

The Monitoring and Checking (MaC) project gave rise to a framework for runtime monitoring with respect to formally specified properties, which later came to be known as runtime verification. The project also built a pioneering runtime verification tool, Java-MaC, that was an instantiation of the approach to check properties of Java programs. In this retrospective, we discuss decisions made in the design of the framework and summarize lessons learned in the course of the project.


Runtime Verification Of Parametric Properties Using Smedl, Teng Zhang, Ramneet Kaur, Insup Lee, Oleg Sokolsky Sep 2019

Runtime Verification Of Parametric Properties Using Smedl, Teng Zhang, Ramneet Kaur, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

Parametric properties are typical properties to be checked in runtime verification (RV). As a common technique for parametric monitoring, trace slicing divides an execution trace into a set of sub traces which are checked against non-parametric base properties. An efficient trace slicing algorithm is implemented in MOP. Another RV technique, QEA further allows for nested use of universal and existential quantification over parameters. In this paper, we present a methodology for parametric monitoring using the RV framework SMEDL. Trace slicing algorithm in MOP can be expressed by execution of a set of SMEDL monitors. Moreover, the semantics of nested quantifiers ...


Fly-By-Logic: A Tool For Unmanned Aircraft System Fleet Planning Using Temporal Logic, Yash Vardhan Pant, Rhudii A. Quaye, Houssam Abbas, Akarsh Varre, Rahul Mangharam May 2019

Fly-By-Logic: A Tool For Unmanned Aircraft System Fleet Planning Using Temporal Logic, Yash Vardhan Pant, Rhudii A. Quaye, Houssam Abbas, Akarsh Varre, Rahul Mangharam

Real-Time and Embedded Systems Lab (mLAB)

Safe planning for fleets of Unmaned Aircraft Systems (UAS) performing complex missions in urban environments has typically been a challenging problem. In the United States of America, the National Aeronautics and Space Administration (NASA) and the Federal Aviation Administration (FAA) have been studying the regulation of the airspace when multiple such fleets of autonomous UAS share the same airspace, outlined in the Concept of Operations document (ConOps). While the focus is on the infrastructure and management of the airspace, the Unmanned Aircraft System (UAS) Traffic Management (UTM) ConOps also outline a potential airspace reservation based system for operation where operators ...


Synthesizing Stealthy Reprogramming Attacks On Cardiac Devices, Nicola Paoletti, Zhihao Jiang, Ariful Islam, Houssam Abbas, Rahul Mangharam, Shan Lin, Zachary Gruber, Scott A. Smolka Apr 2019

Synthesizing Stealthy Reprogramming Attacks On Cardiac Devices, Nicola Paoletti, Zhihao Jiang, Ariful Islam, Houssam Abbas, Rahul Mangharam, Shan Lin, Zachary Gruber, Scott A. Smolka

Real-Time and Embedded Systems Lab (mLAB)

An Implantable Cardioverter Defibrillator (ICD) is a medical device used for the detection of potentially fatal cardiac arrhythmias and their treatment through the delivery of electrical shocks intended to restore normal heart rhythm. An ICD reprogramming attack seeks to alter the device’s parameters to induce unnecessary therapy or prevent required therapy. In this paper, we present a formal approach for the synthesis of ICD reprogramming attacks that are both effective, i.e., lead to fundamental changes in the required therapy, and stealthy, i.e., are hard to detect. We focus on the discrimination algorithm underlying Boston Scientific devices (one ...


Temporal Logic Robustness For General Signal Classes, Houssam Abbas, Yash Vardhan Pant, Rahul Mangharam Apr 2019

Temporal Logic Robustness For General Signal Classes, Houssam Abbas, Yash Vardhan Pant, Rahul Mangharam

Real-Time and Embedded Systems Lab (mLAB)

In multi-agent systems, robots transmit their planned trajectories to each other or to a central controller, and each receiver plans its own actions by maximizing a measure of mission satisfaction. For missions expressed in temporal logic, the robustness function plays the role of satisfaction measure. Currently, a Piece-Wise Linear (PWL) or piece-wise constant reconstruction is used at the receiver. This allows an efficient robustness computation algorithm - a.k.a. monitoring - but is not adaptive to the signal class of interest, and does not leverage the compression properties of more general representations. When communication capacity is at a premium, this is ...


Lcv: A Verification Tool For Linear Controller Software, Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee Apr 2019

Lcv: A Verification Tool For Linear Controller Software, Junkil Park, Miroslav Pajic, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

In the model-based development of controller software, the use of an unverified code generator/transformer may result in introducing unintended bugs in the controller implementation. To assure the correctness of the controller software in the absence of verified code genera- tor/transformer, we develop Linear Controller Verifier (LCV), a tool to verify a linear controller implementation against its original linear controller model. LCV takes as input a Simulink block diagram model and a C code implementation, represents them as linear time-invariant system models respectively, and verifies an input-output equivalence between them. We demonstrate that LCV successfully detects a known bug ...


Verisig: Verifying Safety Properties Of Hybrid Systems With Neural Network Controllers, Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, Insup Lee Apr 2019

Verisig: Verifying Safety Properties Of Hybrid Systems With Neural Network Controllers, Radoslav Ivanov, James Weimer, Rajeev Alur, George J. Pappas, Insup Lee

Departmental Papers (CIS)

This paper presents Verisig, a hybrid system approach to verifying safety properties of closed-loop systems using neural networks as controllers. We focus on sigmoid-based networks and exploit the fact that the sigmoid is the solution to a quadratic differential equation, which allows us to transform the neural network into an equivalent hybrid system. By composing the network’s hybrid system with the plant’s, we transform the problem into a hybrid system verification problem which can be solved using state-of-theart reachability tools. We show that reachability is decidable for networks with one hidden layer and decidable for general networks if ...