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

Engineering Commons

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

Articles 1 - 30 of 122

Full-Text Articles in Engineering

Improving Neural Network Robustness Via Persistency Of Excitation, Kaustubh Sridhar, Oleg Sokolsky, Insup Lee, James Weimer Oct 2021

Improving Neural Network Robustness Via Persistency Of Excitation, Kaustubh Sridhar, Oleg Sokolsky, Insup Lee, James Weimer

Departmental Papers (CIS)

Improving adversarial robustness of neural networks remains a major challenge. Fundamentally, training a neural network via gradient descent is a parameter estimation problem. In adaptive control, maintaining persistency of excitation (PoE) is integral to ensuring convergence of parameter estimates in dynamical systems to their true values. We show that parameter estimation with gradient descent can be modeled as a sampling of an adaptive linear time-varying continuous system. Leveraging this model, and with inspiration from Model-Reference Adaptive Control (MRAC), we prove a sufficient condition to constrain gradient descent updates to reference persistently excited trajectories converging to the true parameters. The sufficient ...


Detecting Oods As Datapoints With High Uncertainty, Ramneet Kaur, Susmit Jha, Anirban Roy, Sangdon Park, Oleg Sokolsky, Insup Lee Jul 2021

Detecting Oods As Datapoints With High Uncertainty, Ramneet Kaur, Susmit Jha, Anirban Roy, Sangdon Park, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

Deep neural networks (DNNs) are known to produce incorrect predictions with very high confidence on out-of-distribution inputs (OODs). This limitation is one of the key challenges in the adoption of DNNs in high-assurance systems such as autonomous driving, air traffic management, and medical diagnosis. This challenge has received significant attention recently, and several techniques have been developed to detect inputs where the model’s prediction cannot be trusted. These techniques detect OODs as datapoints with either high epistemic uncertainty or high aleatoric uncertainty. We demonstrate the difference in the detection ability of these techniques and propose an ensemble approach for ...


Verisig 2.0: Verification Of Neural Network Controllers Using Taylor Model Preconditioning, Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee Jul 2021

Verisig 2.0: Verification Of Neural Network Controllers Using Taylor Model Preconditioning, Radoslav Ivanov, Taylor Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee

Departmental Papers (CIS)

This paper presents Verisig 2.0, a verification tool for closed-loop systems with neural network (NN) controllers. We focus on NNs with tanh/sigmoid activations and develop a Taylor-model-based reachability algorithm through Taylor model preconditioning and shrink wrapping. Furthermore, we provide a parallelized implementation that allows Verisig 2.0 to efficiently handle larger NNs than existing tools can. We provide an extensive evaluation over 10 benchmarks and compare Verisig 2.0 against three state-of-the-art verification tools. We show that Verisig 2.0 is both more accurate and faster, achieving speed-ups of up to 21x and 268x against different tools, respectively.


Modelguard: Runtime Validation Of Lipschitz-Continuous Models, Taylor J. Carpenter, Radoslav Ivanov, Insup Lee, James Weimer Jul 2021

Modelguard: Runtime Validation Of Lipschitz-Continuous Models, Taylor J. Carpenter, Radoslav Ivanov, Insup Lee, James Weimer

Departmental Papers (CIS)

This paper presents ModelGuard, a sampling-based approach to runtime model validation for Lipschitz-continuous models. Although techniques exist for the validation of many classes of models, the majority of these methods cannot be applied to the whole of Lipschitz-continuous models, which includes neural network models. Additionally, existing techniques generally consider only white-box models. By taking a sampling-based approach, we can address black-box models, represented only by an input-output relationship and a Lipschitz constant. We show that by randomly sampling from a parameter space and evaluating the model, it is possible to guarantee the correctness of traces labeled consistent and provide a ...


Improving Classifier Confidence Using Lossy Label-Invariant Transformations, Sooyong Jang, Insup Lee, James Weimer Apr 2021

Improving Classifier Confidence Using Lossy Label-Invariant Transformations, Sooyong Jang, Insup Lee, James Weimer

Departmental Papers (CIS)

Providing reliable model uncertainty estimates is imperative to enabling robust decision making by autonomous agents and humans alike. While recently there have been significant advances in confidence calibration for trained models, examples with poor calibration persist in most calibrated models. Consequently, multiple techniques have been proposed that leverage label-invariant transformations of the input (i.e., an input manifold) to improve worst-case confidence calibration. However, manifold-based confidence calibration techniques generally do not scale and/or require expensive retraining when applied to models with large input spaces (e.g., ImageNet). In this paper, we present the recursive lossy label-invariant calibration (ReCal) technique ...


Reconfiguring Non-Convex Holes In Pivoting Modular Cube Robots, Daniel Adam Feshbach, Cynthia Sung Jan 2021

Reconfiguring Non-Convex Holes In Pivoting Modular Cube Robots, Daniel Adam Feshbach, Cynthia Sung

Departmental Papers (CIS)

We present an algorithm for self-reconfiguration of admissible 3D configurations of pivoting modular cube robots with holes of arbitrary shape and number. Cube modules move across the surface of configurations by pivoting about shared edges, enabling configurations to reshape themselves. Previous work provides a reconfiguration algorithm for admissible 3D configurations containing no non-convex holes; we improve upon this by handling arbitrary admissible 3D configurations. The key insight specifies a point in the deconstruction of layers enclosing non-convex holes at which we can pause and move inner modules out of the hole. We prove this happens early enough to maintain connectivity ...


Verifying The Safety Of Autonomous Systems With Neural Network Controllers, Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee Dec 2020

Verifying The Safety Of Autonomous Systems With Neural Network Controllers, Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee

Departmental Papers (CIS)

This paper addresses the problem of verifying the safety of autonomous systems with neural network (NN) controllers. We focus on NNs with sigmoid/tanh activations and use the fact that the sigmoid/tanh is the solution to a quadratic differential equation. This allows us to convert the NN into an equivalent hybrid system and cast the problem as a hybrid system verification problem, which can be solved by existing tools. Furthermore, we improve the scalability of the proposed method by approximating the sigmoid with a Taylor series with worst-case error bounds. Finally, we provide an evaluation over four benchmarks, including ...


Compositional Probabilistic Analysis Of Temporal Properties Over Stochastic Detectors, Ivan Ruchkin, Oleg Sokolsky, James Weimer, Tushar Hedaoo, Insup Lee Nov 2020

Compositional Probabilistic Analysis Of Temporal Properties Over Stochastic Detectors, Ivan Ruchkin, Oleg Sokolsky, James Weimer, Tushar Hedaoo, Insup Lee

Departmental Papers (CIS)

Run-time monitoring is a vital part of safety-critical systems. However, early-stage assurance of monitoring quality is currently limited: it relies either on complex models that might be inaccurate in unknown ways, or on data that would only be available once the system has been built. To address this issue, we propose a compositional framework for modeling and analysis of noisy monitoring systems. Our novel 3-value detector model uses probability spaces to represent atomic (non-composite) detectors, and it composes them into a temporal logic-based monitor. The error rates of these monitors are estimated by our analysis engine, which combines symbolic probability ...


Case Study: Verifying The Safety Of An Autonomous Racing Car With A Neural Network Controller, Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee Apr 2020

Case Study: Verifying The Safety Of An Autonomous Racing Car With A Neural Network Controller, Radoslav Ivanov, Taylor J. Carpenter, James Weimer, Rajeev Alur, George Pappas, Insup Lee

Departmental Papers (CIS)

This paper describes a verification case study on an autonomous racing car with a neural network (NN) controller. Although several verification approaches have been recently proposed, they have only been evaluated on low-dimensional systems or systems with constrained environments. To explore the limits of existing approaches, we present a challenging benchmark in which the NN takes raw LiDAR measurements as input and outputs steering for the car. We train a dozen NNs using reinforcement learning (RL) and show that the state of the art in verification can handle systems with around 40 LiDAR rays. Furthermore, we perform real experiments to ...


Calibrated Prediction With Covariate Shift Via Unsupervised Domain Adaptation, Sangdon Park, Osbert Bastani, James Weimer, Insup Lee Mar 2020

Calibrated Prediction With Covariate Shift Via Unsupervised Domain Adaptation, Sangdon Park, Osbert Bastani, James Weimer, Insup Lee

Departmental Papers (CIS)

Reliable uncertainty estimates are an important tool for helping autonomous agents or human decision makers understand and leverage predictive models. However, existing approaches to estimating uncertainty largely ignore the possibility of covariate shift—i.e., where the real-world data distribution may differ from the training distribution. As a consequence, existing algorithms can overestimate certainty, possibly yielding a false sense of confidence in the predictive model. We propose an algorithm for calibrating predictions that accounts for the possibility of covariate shift, given labeled examples from the training distribution and unlabeled examples from the real-world distribution. Our algorithm uses importance weighting to ...


Pac Confidence Sets For Deep Neural Networks Via Calibrated Prediction, Sangdon Park, Osbert Bastani, Nikolai Matni, Insup Lee Feb 2020

Pac Confidence Sets For Deep Neural Networks Via Calibrated Prediction, Sangdon Park, Osbert Bastani, Nikolai Matni, Insup Lee

Departmental Papers (CIS)

We propose an algorithm combining calibrated prediction and generalization bounds from learning theory to construct confidence sets for deep neural networks with PAC guarantees---i.e., the confidence set for a given input contains the true label with high probability. We demonstrate how our approach can be used to construct PAC confidence sets on ResNet for ImageNet, a visual object tracking model, and a dynamics model for the half-cheetah reinforcement learning problem.


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.


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


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


Correct-By-Construction Implementation Of Runtime Monitors Using Stepwise Refinement, Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clement Pit-Claudel, Insup Lee, Oleg Sokolsky Sep 2018

Correct-By-Construction Implementation Of Runtime Monitors Using Stepwise Refinement, Teng Zhang, John Wiegley, Theophilos Giannakopoulos, Gregory Eakman, Clement Pit-Claudel, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

Runtime verification (RV) is a lightweight technique for verifying traces of computer systems. One challenge in applying RV is to guarantee that the implementation of a runtime monitor correctly detects and signals unexpected events. In this paper, we present a method for deriving correct-by-construction implementations of runtime monitors from high-level specifications using Fiat, a Coq library for stepwise refinement. SMEDL (Scenario-based Meta-Event Definition Language), a domain specific language for event-driven RV, is chosen as the specification language. We propose an operational semantics for SMEDL suitable to be used in Fiat to describe the behavior of a monitor in a relational ...


Reducing Pulse Oximetry False Alarms Without Missing Life-Threatening Events, Hung Nguyen, Sooyong Jang, Radoslav Ivanov, Christopher P. Bonafide, James Weimer, Insup Lee Sep 2018

Reducing Pulse Oximetry False Alarms Without Missing Life-Threatening Events, Hung Nguyen, Sooyong Jang, Radoslav Ivanov, Christopher P. Bonafide, James Weimer, Insup Lee

Departmental Papers (CIS)

Alarm fatigue has been increasingly recognized as one of the most significant problems in the hospital environment. One of the major causes is the excessive number of false physiologic monitor alarms. An underlying problem is the inefficient traditional threshold alarm system for physiologic parameters such as low blood oxygen saturation (SpO2). In this paper, we propose a robust classification procedure based on the AdaBoost algorithm with reject option that can identify and silence false SpO2 alarms, while ensuring zero misclassified clinically significant alarms. Alarms and vital signs related to SpO2 such as heart rate and pulse rate ...


Injected And Delivered: Fabricating Implicit Control Over Actuation Systems By Spoofing Inertial Sensors, Yazhou Tu, Zhiqiang Lin, Insup Lee, Xiali Hei Aug 2018

Injected And Delivered: Fabricating Implicit Control Over Actuation Systems By Spoofing Inertial Sensors, Yazhou Tu, Zhiqiang Lin, Insup Lee, Xiali Hei

Departmental Papers (CIS)

Inertial sensors provide crucial feedback for control systems to determine motional status and make timely, automated decisions. Prior efforts tried to control the output of inertial sensors with acoustic signals. However, their approaches did not consider sample rate drifts in analog-to-digital converters as well as many other realistic factors. As a result, few attacks demonstrated effective control over inertial sensors embedded in real systems.

This work studies the out-of-band signal injection methods to deliver adversarial control to embedded MEMS inertial sensors and evaluates consequent vulnerabilities exposed in control systems relying on them. Acoustic signals injected into inertial sensors are out-of-band ...


Bandwidth Optimal Data/Service Delivery For Connected Vehicles Via Edges, Deepak Gangadharan, Oleg Sokolsky, Insup Lee, Baekgyu Kim, Chung-Wei Lin, Shinichi Shiraishi Jul 2018

Bandwidth Optimal Data/Service Delivery For Connected Vehicles Via Edges, Deepak Gangadharan, Oleg Sokolsky, Insup Lee, Baekgyu Kim, Chung-Wei Lin, Shinichi Shiraishi

Departmental Papers (CIS)

The paradigm of connected vehicles is fast gaining lot of attraction in the automotive industry. Recently, a lot of technological innovation has been pushed through to realize this paradigm using vehicle to cloud (V2C), infrastructure (V2I) and vehicle (V2V) communications. This has also opened the doors for efficient delivery of data/service to the vehicles via edge devices that are closer to the vehicles. In this work, we propose an optimization framework that can be used to deliver data/service to the connected vehicles such that a bandwidth cost objective is optimized. For the first time, we also integrate a ...


Data Freshness Over-Engineering: Formulation And Results, Dagaen Golomb, Deepak Gangadharan, Sanjian Chen, Oleg Sokolsky, Insup Lee May 2018

Data Freshness Over-Engineering: Formulation And Results, Dagaen Golomb, Deepak Gangadharan, Sanjian Chen, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

In many application scenarios, data consumed by real-time tasks are required to meet a maximum age, or freshness, guarantee. In this paper, we consider the end-to-end freshness constraint of data that is passed along a chain of tasks in a uniprocessor setting. We do so with few assumptions regarding the scheduling algorithm used. We present a method for selecting the periods of tasks in chains of length two and three such that the end-to-end freshness requirement is satisfied, and then extend our method to arbitrary chains. We perform evaluations of both methods using parameters from an embedded benchmark suite (E3S ...


Openice-Lite: Towards A Connectivity Platform For The Internet Of Medical Things, Radoslav Ivanov, Hung Nguyen, James Weimer, Oleg Sokolsky, Insup Lee May 2018

Openice-Lite: Towards A Connectivity Platform For The Internet Of Medical Things, Radoslav Ivanov, Hung Nguyen, James Weimer, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

The Internet of Medical Things (IoMT) is poised to revolutionize medicine. However, medical device communication, coordination, and interoperability present challenges for IoMT applications due to safety, security, and privacy concerns. These challenges can be addressed by developing an open platform for IoMT that can provide guarantees on safety, security and privacy. As a first step, we introduce OpenICE-lite, a middleware for medical device interoperability that also provides security guarantees and allows other IoMT applications to view/analyze the data in real time. We describe two applications that currently utilize OpenICE-lite, namely (i) a critical pulmonary shunt predictor for infants during ...


Generic Formal Framework For Compositional Analysis Of Hierarchical Scheduling Systems, Jalil Boudjadar, Jin Hyun Kim, Linh Thi Xuan Phan, Insup Lee, Kim G. Larsen, Ulrik Nyman May 2018

Generic Formal Framework For Compositional Analysis Of Hierarchical Scheduling Systems, Jalil Boudjadar, Jin Hyun Kim, Linh Thi Xuan Phan, Insup Lee, Kim G. Larsen, Ulrik Nyman

Departmental Papers (CIS)

We present a compositional framework for the specification and analysis of hierarchical scheduling systems (HSS). Firstly we provide a generic formal model, which can be used to describe any type of scheduling system. The concept of Job automata is introduced in order to model job instantiation patterns. We model the interaction between different levels in the hierarchy through the use of state-based resource models. Our notion of resource model is general enough to capture multi-core architectures, preemptiveness and non-determinism.


Context-Aware Detection In Medical Cyber-Physical Systems, Radoslav Ivanov, James Weimer, Insup Lee Apr 2018

Context-Aware Detection In Medical Cyber-Physical Systems, Radoslav Ivanov, James Weimer, Insup Lee

Departmental Papers (CIS)

This paper considers the problem of incorporating context in medical cyber-physical systems (MCPS) applications for the purpose of improving the performance of MCPS detectors. In particular, in many applications additional data could be used to conclude that actual measurements might be noisy or wrong (e.g., machine settings might indicate that the machine is improperly attached to the patient); we call such data context. The first contribution of this work is the formal definition of context, namely additional information whose presence is associated with a change in the measurement model (e.g., higher variance). Given this formulation, we developed the ...


Parameter Invariant Monitoring For Signal Temporal Logic, Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, Insup Lee Apr 2018

Parameter Invariant Monitoring For Signal Temporal Logic, Nima Roohi, Ramneet Kaur, James Weimer, Oleg Sokolsky, Insup Lee

Departmental Papers (CIS)

Signal Temporal Logic (STL) is a prominent specification formalism for real-time systems, and monitoring these specifications, specially when (for different reasons such as learning) behavior of systems can change over time, is quite important. There are three main challenges in this area: (1) full observation of system state is not possible due to noise or nuisance parameters, (2) the whole execution is not available during the monitoring, and (3) computational complexity of monitoring continuous time signals is very high. Although, each of these challenges has been addressed by different works, to the best of our knowledge, no one has addressed ...


Multi-Mode Virtualization For Soft Real-Time Systems, Haoran Li, Meng Xu, Chong Li, Chenyang Lu, Christopher Gill, Linh T.X. Phan, Insup Lee, Oleg Sokolsky Apr 2018

Multi-Mode Virtualization For Soft Real-Time Systems, Haoran Li, Meng Xu, Chong Li, Chenyang Lu, Christopher Gill, Linh T.X. Phan, Insup Lee, Oleg Sokolsky

Departmental Papers (CIS)

Real-time virtualization is an emerging technology for embedded systems integration and latency-sensitive cloud applications. Earlier real-time virtualization platforms require offline configuration of the scheduling parameters of virtual machines (VMs) based on their worst-case workloads, but this static approach results in pessimistic resource allocation when the workloads in the VMs change dynamically. Here, we present Multi-Mode-Xen (M2-Xen), a real-time virtualization platform for dynamic real-time systems where VMs can operate in modes with different CPU resource requirements at run-time. M2-Xen has three salient capabilities: (1) dynamic allocation of CPU resources among VMs in response to their mode changes, (2) overload avoidance at ...


Repulmo: A Remote Pulmonary Monitoring System, Hung Nguyen, Radoslav Ivanov, Sara B. Demauro, James Weimer Apr 2018

Repulmo: A Remote Pulmonary Monitoring System, Hung Nguyen, Radoslav Ivanov, Sara B. Demauro, James Weimer

Departmental Papers (CIS)

Remote physiological monitoring is increasing in popularity with the evolution of technologies in the healthcare industry. However, the current solutions for remote monitoring of blood-oxygen saturation, one of the most common continuously monitored vital signs, either have inconsistent accuracy or are not secure for transmitting over the network. In this paper, we propose RePulmo, an open-source platform for secure and accurate remote pulmonary data monitoring. RePulmo satisfies both robustness and security requirements by utilizing hospital-grade pulse oximeter devices with multiple layers of security enforcement. We describe two applications of RePulmo, namely (1) a remote pulmonary monitoring system for infants to ...


Logsafe: Secure And Scalable Data Logger For Iot Devices, Hung Nguyen, Radoslav Ivanov, Linh T.X. Phan, Oleg Sokolsky, James Weimer, Insup Lee Apr 2018

Logsafe: Secure And Scalable Data Logger For Iot Devices, Hung Nguyen, Radoslav Ivanov, Linh T.X. Phan, Oleg Sokolsky, James Weimer, Insup Lee

Departmental Papers (CIS)

As devices in the Internet of Things (IoT) increase in number and integrate with everyday lives, large amounts of personal information will be generated. With multiple discovered vulnerabilities in current IoT networks, a malicious attacker might be able to get access to and misuse this personal data. Thus, a logger that stores this information securely would make it possible to perform forensic analysis in case of such attacks that target valuable data. In this paper, we propose LogSafe, a scalable, fault-tolerant logger that leverages the use of Intel Software Guard Extensions (SGX) to store logs from IoT devices efficiently and ...