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

Engineering Commons

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

Articles 1 - 7 of 7

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 ...


Holistic Resource Allocation For Multicore Real-Time Systems, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Yuhan Lin, Haoran Li, Chenyang Lu, Insup Lee Apr 2019

Holistic Resource Allocation For Multicore Real-Time Systems, Meng Xu, Linh T.X. Phan, Hyon-Young Choi, Yuhan Lin, Haoran Li, Chenyang Lu, Insup Lee

Departmental Papers (CIS)

This paper presents CaM, a holistic cache and memory bandwidth resource allocation strategy for multicore real-time systems. CaM is designed for partitioned scheduling, where tasks are mapped onto cores, and the shared cache and memory bandwidth resources are partitioned among cores to reduce resource interferences due to concurrent accesses. Based on our extension of LITMUSRT with Intel’s Cache Allocation Technology and MemGuard, we present an experimental evaluation of the relationship between the allocation of cache and memory bandwidth resources and a task’s WCET. Our resource allocation strategy exploits this relationship to map tasks onto cores, and to ...


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 ...