Biblio

Filters: Author is Pajic, Miroslav  [Clear All Filters]
2019-12-02
Elfar, Mahmoud, Zhu, Haibei, Cummings, M. L., Pajic, Miroslav.  2019.  Security-Aware Synthesis of Human-UAV Protocols. 2019 International Conference on Robotics and Automation (ICRA). :8011–8017.
In this work, we synthesize collaboration protocols for human-unmanned aerial vehicle (H-UAV) command and control systems, where the human operator aids in securing the UAV by intermittently performing geolocation tasks to confirm its reported location. We first present a stochastic game-based model for the system that accounts for both the operator and an adversary capable of launching stealthy false-data injection attacks, causing the UAV to deviate from its path. We also describe a synthesis challenge due to the UAV's hidden-information constraint. Next, we perform human experiments using a developed RESCHU-SA testbed to recognize the geolocation strategies that operators adopt. Furthermore, we deploy machine learning techniques on the collected experimental data to predict the correctness of a geolocation task at a given location based on its geographical features. By representing the model as a delayed-action game and formalizing the system objectives, we utilize off-the-shelf model checkers to synthesize protocols for the human-UAV coalition that satisfy these objectives. Finally, we demonstrate the usefulness of the H-UAV protocol synthesis through a case study where the protocols are experimentally analyzed and further evaluated by human operators.
2018-09-12
Park, Junkil, Ivanov, Radoslav, Weimer, James, Pajic, Miroslav, Son, Sang Hyuk, Lee, Insup.  2017.  Security of Cyber-Physical Systems in the Presence of Transient Sensor Faults. ACM Trans. Cyber-Phys. Syst.. 1:15:1–15:23.
This article is concerned with the security of modern Cyber-Physical Systems in the presence of transient sensor faults. We consider a system with multiple sensors measuring the same physical variable, where each sensor provides an interval with all possible values of the true state. We note that some sensors might output faulty readings and others may be controlled by a malicious attacker. Differing from previous works, in this article, we aim to distinguish between faults and attacks and develop an attack detection algorithm for the latter only. To do this, we note that there are two kinds of faults—transient and permanent; the former are benign and short-lived, whereas the latter may have dangerous consequences on system performance. We argue that sensors have an underlying transient fault model that quantifies the amount of time in which transient faults can occur. In addition, we provide a framework for developing such a model if it is not provided by manufacturers. Attacks can manifest as either transient or permanent faults depending on the attacker’s goal. We provide different techniques for handling each kind. For the former, we analyze the worst-case performance of sensor fusion over time given each sensor’s transient fault model and develop a filtered fusion interval that is guaranteed to contain the true value and is bounded in size. To deal with attacks that do not comply with sensors’ transient fault models, we propose a sound attack detection algorithm based on pairwise inconsistencies between sensor measurements. Finally, we provide a real-data case study on an unmanned ground vehicle to evaluate the various aspects of this article.
2018-05-16
Park, Junkil, Pajic, Miroslav, Sokolsky, Oleg, Lee, Insup.  2017.  Automatic Verification of Finite Precision Implementations of Linear Controllers. Tools and Algorithms for the Construction and Analysis of Systems: 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, P. :153–169.
Jakovljevic, Zivana, Mitrovic, Stefan, Pajic, Miroslav.  2017.  Cyber Physical Production Systems–-An IEC 61499 Perspective. Proceedings of 5th International Conference on Advanced Manufacturing Engineering and Technologies: NEWTECH 2017. :27–39.
Jakovljevic, Zivana, Majstorovic, Vidosav, Stojadinovic, Slavenko, Zivkovic, Srdjan, Gligorijevic, Nemanja, Pajic, Miroslav.  2017.  Cyber-Physical Manufacturing Systems (CPMS). Proceedings of 5th International Conference on Advanced Manufacturing Engineering and Technologies: NEWTECH 2017. :199–214.
Lesi, Vuk, Jovanov, Ilija, Pajic, Miroslav.  2017.  Security-Aware Scheduling of Embedded Control Tasks. ACM Trans. Embed. Comput. Syst.. 16:188:1–188:21.
Ivanov, Radoslav, Pajic, Miroslav, Lee, Insup.  2016.  Attack-Resilient Sensor Fusion for Safety-Critical Cyber-Physical Systems. ACM Transactions on Embedded Computing Systems. 15:21:1–21:24.
2017-05-19
Ivanov, Radoslav, Pajic, Miroslav, Lee, Insup.  2016.  Attack-Resilient Sensor Fusion for Safety-Critical Cyber-Physical Systems. ACM Trans. Embed. Comput. Syst.. 15:21:1–21:24.

This article focuses on the design of safe and attack-resilient Cyber-Physical Systems (CPS) equipped with multiple sensors measuring the same physical variable. A malicious attacker may be able to disrupt system performance through compromising a subset of these sensors. Consequently, we develop a precise and resilient sensor fusion algorithm that combines the data received from all sensors by taking into account their specified precisions. In particular, we note that in the presence of a shared bus, in which messages are broadcast to all nodes in the network, the attacker’s impact depends on what sensors he has seen before sending the corrupted measurements. Therefore, we explore the effects of communication schedules on the performance of sensor fusion and provide theoretical and experimental results advocating for the use of the Ascending schedule, which orders sensor transmissions according to their precision starting from the most precise. In addition, to improve the accuracy of the sensor fusion algorithm, we consider the dynamics of the system in order to incorporate past measurements at the current time. Possible ways of mapping sensor measurement history are investigated in the article and are compared in terms of the confidence in the final output of the sensor fusion. We show that the precision of the algorithm using history is never worse than the no-history one, while the benefits may be significant. Furthermore, we utilize the complementary properties of the two methods and show that their combination results in a more precise and resilient algorithm. Finally, we validate our approach in simulation and experiments on a real unmanned ground robot.

2018-05-16
Bogdan, Paul, Pajic, Miroslav, Pande, Partha Pratim, Raghunathan, Vijay.  2016.  Making the Internet-of-things a Reality: From Smart Models, Sensing and Actuation to Energy-efficient Architectures. Proceedings of the Eleventh IEEE/ACM/IFIP International Conference on Hardware/Software Codesign and System Synthesis. :25:1–25:10.
Ibrahim, Mohamed, Boswell, Craig, Chakrabarty, Krishnendu, Scott, Kristin, Pajic, Miroslav.  2016.  A Real-time Digital-microfluidic Platform for Epigenetics. Proceedings of the International Conference on Compilers, Architectures and Synthesis for Embedded Systems. :10:1–10:10.
Park, Junkil, Pajic, Miroslav, Lee, Insup, Sokolsky, Oleg.  2016.  Scalable Verification of Linear Controller Software. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). :662–679.
Pajic, Miroslav, Park, Junkil, Lee, Insup, Pappas, George J., Sokolsky, Oleg.  2015.  Automatic Verification of Linear Controller Software. Proceedings of the 12th International Conference on Embedded Software. :217–226.
Al Faruque, Mohammad, Regazzoni, Francesco, Pajic, Miroslav.  2015.  Design Methodologies for Securing Cyber-physical Systems. Proceedings of the 10th International Conference on Hardware/Software Codesign and System Synthesis. :30–36.
Park, Junkil, Ivanov, Radoslav, Weimer, James, Pajic, Miroslav, Lee, Insup.  2015.  Sensor Attack Detection in the Presence of Transient Faults. Proceedings of the ACM/IEEE Sixth International Conference on Cyber-Physical Systems. :1–10.
2018-05-23
Jiang, Zhihao, Pajic, Miroslav, Alur, Rajeev, Mangharam, Rahul.  2014.  Closed-loop verification of medical devices with model abstraction and refinement. International Journal on Software Tools for Technology Transfer. 16:191–213.
Jiang, Zhihao, Pajic, Miroslav, Moarref, Salar, Alur, Rajeev, Mangharam, Rahul.  2012.  Modeling and Verification of a Dual Chamber Implantable Pacemaker. Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. :188–203.