The First-Order Logic of Signals
Speaker: Thomas A. Henzinger
Formalizing properties of systems with continuous dynamics is a challenging task. In this paper, we propose a formal framework for specifying and monitoring rich temporal properties of real-valued signals. We introduce signal first-order logic (SFO) as a specification language that combines first-order logic with linear-real arithmetic and unary function symbols interpreted as piecewise-linear signals. We first show that while the satisfiability problem for SFO is undecidable, its membership and monitoring problems are decidable. We develop an offline monitoring procedure for SFO that has polynomial complexity in the size of the input trace and the specification, for a fixed number of quantifiers and function symbols. We show that the algorithm has computation time linear in the size of the input trace for the important fragment of bounded-response specifications interpreted over input traces with finite variability. We can use our results to extend signal temporal logic with first-order quantifiers over space and time parameters, while preserving its efficient monitoring. We finally demonstrate the practical appeal of our logic through a case study in the micro-electronics domain.
Thomas A. Henzinger is president of IST Austria (Institute of Science and Technology Austria). He holds a Dipl.-Ing. degree in Computer Science from Kepler University in Linz, Austria, an M.S. degree in Computer and Information Sciences from the University of Delaware, a Ph.D. degree in Computer Science from Stanford University (1991), and a Dr.h.c. from Fourier University in Grenoble, France (2012) and from Masaryk University in Brno, Czech Republic (2015). He was Assistant Professor of Computer Science at Cornell University (1992-95), Assistant Professor (1996-97), Associate Professor (1997-98), and Professor (1998-2004) of Electrical Engineering and Computer Sciences at the University of California, Berkeley. He was also Director at the Max-Planck Institute for Computer Science in Saarbruecken, Germany (1999) and Professor of Computer and Communication Sciences at EPFL in Lausanne, Switzerland (2004-09). His research focuses on modern systems theory, especially models, algorithms, and tools for the design and verification of reliable software, hardware, and embedded systems. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is an ISI highly cited researcher, a member of Academia Europaea, a member of the German Academy of Sciences (Leopoldina), a member of the Austrian Academy of Sciences, a Fellow of the AAAS, a Fellow of the ACM, and a Fellow of the IEEE. He has received the Milner Award of the Royal Society, the Wittgenstein Award of the Austrian Science Fund, and an ERC Advanced Investigator Grant.
Hitchhiker’s Guide to the IoT Galaxy full of Security & Privacy Challenges (An Attempt)
Speaker: Ahmad-Reza Sadeghi
The Internet of things (IoT) is rapidly emerging with the goal to connect the unconnected. Many new device manufacturers are entering the market of internet-connected appliances for smart homes and offices, ranging from motion sensors to virtual voice assistants. However, due to lack of security by design and flawed implementations we are facing significant security and privacy challenges specific to IoT, such as perilous IoT botnet attacks, and novel privacy threats caused by widespread installation of wireless sensors, actuators and smart home appliances even in the private setting of our homes. Unfortunately, standard security measures like properly encrypted communications do not protect against these threats.
The massive scale of the IoT device population and enormous diversity of device hardware, operating systems, software frameworks and manufacturers makes it very difficult to establish standard IoT security and privacy-protecting solutions by simply applying and extending known solutions, neither for per-device security architectures nor for network security measures. In particular, existing intrusion detection techniques seem ineffective to detect compromised IoT devices.
In this talk, we will present our recent work, including industry collaborations, on addressing various security and privacy challenges in the growing IoT landscape. In particular, we focus on approaches for flexible management of devices security association (device pairing) as well as automated device identification and reliable detection of compromised devices based on their inherent communication behavior.
Ahmad-Reza Sadeghi is a full professor of Computer Science at the TU Darmstadt, Germany. He is the head of the Systems Security Lab at the Cybersecurity Research Center of TU Darmstadt. Since 2012 he is also the director of the Intel Collaborative Research Institute for Secure Computing and Resilient Autonomous Systems at TU Darmstadt. He holds a Ph.D. in Computer Science from the University of Saarland, Germany. Prior to academia, he worked in R&D of Telecommunications enterprises, amongst others Ericsson Telecommunications. He has been continuously contributing to security and privacy research. For his influential research on Trusted and Trustworthy Computing he received the renowned German “Karl Heinz Beckurts” award. This award honors excellent scientific achievements with high impact on industrial innovations in Germany.
He has served as Editor-In-Chief of IEEE Security and Privacy Magazine, on editorial board of ACM Transactions on Information and System Security (TISSEC), and as guest editor of Transactions on Computer-Aided Design (TCAD), special Issue on Hardware Security and Trust. Currently he is serving on the editorial boards of ACM Security and Privacy Books, ACM Transactions on the Internet of Things (TIOT), and ACM Transactions on Design and Automation of Electronic Systems (TODAES).
Outside-In Autonomous Systems
Speaker: Dr. Jie Liu
Abstract: Breakthroughs in device intelligence promise autonomous systems that can achieve human level fidelity interacting with the physical world. While much attention has been focused on inside-out autonomous systems, such as self-driving cars, AR goggles, and robots, which must cope with complex environments using primarily onboard sensing and computing capabilities, we argue the importance of its dual. Outside-in autonomous systems (OIAS) create smart environments that observe and understand space, people, and things from bird’s eye points of view. In OIAS, people do not need to be augmented with wearable devices or change their natural behavior. Retail stores, factory floors, hospitals, and classrooms can all be augmented with various degrees of outside-in autonomy for better efficiency, higher productivity, and less mistakes.
We will discuss a few techniques, primarily on computer vision and sensor fusion, for building OIAS. These include people identification, people tracking, object identification, and activity recognition. We use autonomous retail stores as an example to illustrate current technology landscape and challenges of bringing lab-proven technologies to the real world. Due to their distributed, multi-modality and real-time nature, calibration, coordination and acceleration become keys for system scalability. Although fully autonomous systems still have a long way to go, technologies developed towards it can bring progressive values to live.
Dr. Jie Liu is a Partner Research Manager and the GM of the Ambient Intelligent Team at Microsoft AI Perception and Mixed Reality. He is an IEEE Fellow, an ACM Distinguished Scientist and an ACM Distinguished Speaker. His research interests root in sensing and interacting with the physical world through computing. Examples include time, location, and energy awareness, and Internet/Intelligence of Things. He has published broadly in areas such as sensor networks, embedded systems, mobile and ubiquitous computing, and data center management, and has received 6 best paper awards in top academic conferences. In addition, he holds more than 100 patents. He is an Associate Editor of ACM Trans. on Sensor Networks; was an Associate Editor of IEEE Trans. on Mobile Computing; and has chaired a number of top-tier conferences and their steering committees, including CPS Week, IPSN, and SenSys. He obtained his Ph.D. degree from Electrical Engineering and Computer Sciences, UC Berkeley in 2001, and his Master and Bachelor’s degrees from Department of Automation, Tsinghua University, Beijing, China. From 2001 to 2004, he was a research scientist in Palo Alto Research Center (formerly Xerox PARC).