VORTEX 2024 – Proceedings

7th ACM International Workshop on Verification and Monitoring at Runtime Execution (VORTEX 2024)

Frontmatter

Keynotes

R2U2: Runtime Verification Takes Off! (Keynote)
Kristin Yvonne Rozier
(Iowa State University, USA)
Runtime Verification (RV) has become critical to the deployment of intelligent, autonomous systems, including aircraft, spacecraft, satellites, rovers, and robots. The most useful, important, and safety-critical jobs require these systems to reliably sense and respond to both nominal and off-nominal conditions. They must react to challenging environments, and detect critical failures on-board, in real time to enable mitigation triggering. We are challenged by the constraints of real-life embedded operation that limit the system instrumentation, space, timing, power, weight, cost, and other operating conditions of on-board, runtime verification. While the research area of RV is vast, there is a dearth of RV tools that can operate within these constraints, and without violating, e.g., FAA rules for flight certification. The Realizable, Responsive, Unobtrusive Unit (R2U2) uniquely fills this need, analyzing formal system requirements on-board flight systems during runtime. We overview how R2U2 works and highlight recent success stories, including embedding on-board various UAS, a sounding rocket, the humanoid robot Robonaut2, and NASA's Lunar Gateway.

@InProceedings{VORTEX24p1, author = {Kristin Yvonne Rozier}, title = {R2U2: Runtime Verification Takes Off! (Keynote)}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {1--1}, doi = {10.1145/3679008.3685539}, year = {2024}, } Publisher's Version

Runtime Invariant Checking in Robotic Systems and Deep Learning Models (Keynote)
Xiangyu Zhang
(Purdue University, USA)
Invariant checking is an important runtime verification method. While it was invented for classic software systems, the concept can be extended to identifying runtime failures and attacks for other computation systems. In this talk, I will discuss how invariant checking can be extended to identifying physical attacks to robotic vehicles (RVs) and adversarial attacks to deep learning systems. For RV attack detection, we derive and monitor so-called Control Invariants (CI). More specifically, we propose a method to extract such invariants by jointly modeling a vehicle’s physical properties, its control algorithm and the laws of physics. These invariants are represented in a state-space form, which can then be implemented and inserted into the vehicle’s control program binary for runtime invariant check. Our evaluation on eleven RVs, including quadrotor, hexarotor, and ground rover, show that the invariant check can detect three common types of physical attacks – including sensor attack, actuation signal attack, and parameter attack – with very low runtime overhead. In addition, statistical distribution invariants can be derived for activation values of deep learning models. Checking such invariants enables runtime attack detection for such models.

@InProceedings{VORTEX24p2, author = {Xiangyu Zhang}, title = {Runtime Invariant Checking in Robotic Systems and Deep Learning Models (Keynote)}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {2--2}, doi = {10.1145/3679008.3685540}, year = {2024}, } Publisher's Version

Operational and Declarative Runtime Verification (Keynote)
Klaus Havelund, Moran Omer, and Doron Peled
(Jet Propulsion Laboratory at California Institute of Technology, USA; Bar-Ilan University, Israel)
Runtime verification (RV) is used to monitor executions of a system, checking them against a formal specification. It can detect failures, and can also be used to control a system, diverting its operation to avoid a failure. One can identify two main approaches of specifying properties to be monitored: operational specification and declarative specification. Operational specification describes, using a programming language like formalism, how each new monitored event updates a summary of the observed sequence of events, consisting of user defined variables. This kind of specification is attractive, e.g., for describing aggregated arithmetic calculations and can be very simple to implement. Declarative specification gives a more global view of the requirements that the monitored execution sequences must satisfy, based on a temporal formalism, e.g., propositional or first-order temporal logic. We describe an RV system designed and implemented to work with the two kinds of specifications. It allows the two parts to collaborate by sending ongoing results between them. This results in benefiting from both capabilities and reducing the deficiencies of each of the separate specification methods. We compare alternative approaches to combining operational and declarative specification as internal and external DSLs.

@InProceedings{VORTEX24p3, author = {Klaus Havelund and Moran Omer and Doron Peled}, title = {Operational and Declarative Runtime Verification (Keynote)}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {3--12}, doi = {10.1145/3679008.3685541}, year = {2024}, } Publisher's Version

Papers

RVsec: Towards a Comprehensive Technology Stack for Secure Deployment of Software Monitors
Christian Colombo, Axel Curmi, and Robert Abela
(University of Malta, Malta)
Runtime monitors frequently need to be deployed in highly secure software environments to help further secure the system under scrutiny. In such contexts, the monitor could benefit from security hardening over and above the rest of the system since the monitoring component is of particular interest to the attacker. If the attacker successfully disables the monitor, the attack can be executed without potential alarms being raised, leaving no evidence behind. Furthermore, due to the separation of concerns inherent in runtime verification, monitors are typically separated from the rest of the system, facilitating isolation and a hardened security environment which would otherwise be difficult to achieve for the whole system. The combination of these observations, motivate us to consider a number of approaches for increased monitor security which we present as a technology stack called RVsec which could be instantiated in various contexts. Using a quantum-safe chat application as a case study, we present a pragmatic solution to various threat scenarios while considering the trade-offs in terms of additional setup and runtime costs.

@InProceedings{VORTEX24p13, author = {Christian Colombo and Axel Curmi and Robert Abela}, title = {RVsec: Towards a Comprehensive Technology Stack for Secure Deployment of Software Monitors}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {13--18}, doi = {10.1145/3679008.3685542}, year = {2024}, } Publisher's Version

Devising a TraceObject Class for Improved Runtime Monitoring of ooRexx Applications
Rony G. Flatscher and Till Winkler
(Vienna University of Economics and Business, Austria)
The dynamic programming language ooRexx includes a runtime monitoring keyword instruction named TRACE. This keyword instruction produces a trace line for each traced statement. Although additional trace information was added, ooRexx 5.0.0 is missing important information, such as tracing threads, whether a method is currently guarded, the guard locks state, and the interpreter instance. With the introduction of a specific trace-related class, TraceObject, it is now possible to maintain all ooRexx-related trace information for each traced statement in a proper directory that can be analyzed at runtime. This article will introduce the TraceObject class and its properties, including the ability to collect all produced trace objects for inspection and analysis. It focuses on the trace line (the trace object's string) representation that can be formatted to include the missing aspects for analyzing dynamic, multi-threaded, guarded methods on multi-instance ooRexx applications.

@InProceedings{VORTEX24p19, author = {Rony G. Flatscher and Till Winkler}, title = {Devising a TraceObject Class for Improved Runtime Monitoring of ooRexx Applications}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {19--24}, doi = {10.1145/3679008.3685543}, year = {2024}, } Publisher's Version

Optimising Aggregate Monitors for Spatial Logic of Closure Spaces Properties
Gianluca Aguzzi, Giorgio Audrito, and Mirko Viroli
(University of Bologna, Italy; University of Turin, Italy)
The advent of highly distributed systems, such as the Internet of Things, has led to the development of distributed systems that require efficient and resilient runtime monitoring. Among the various monitoring techniques, runtime verification is a lightweight verification method that assesses the correctness of a running system concerning a formal specification. In this paper, we investigate the optimization of aggregate monitors, i.e., monitors that operate on ensembles of devices, for properties expressed in Spatial Logic of Closure Spaces (SLCS)--a formal logic designed to reason about spatial relationships between entities in a distributed system. We propose three different algorithms for the implementation of the "somewhere" operator, a key construct in SLCS, and we evaluate their performance through a series of simulations, comparing their convergence time and computational load.

@InProceedings{VORTEX24p25, author = {Gianluca Aguzzi and Giorgio Audrito and Mirko Viroli}, title = {Optimising Aggregate Monitors for Spatial Logic of Closure Spaces Properties}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {25--31}, doi = {10.1145/3679008.3685544}, year = {2024}, } Publisher's Version

Real-Time Guarantees for SLCS Monitors in XC
Giorgio Audrito, Ferruccio Damiani, and Gianluca Torta
(University of Turin, Italy)
The behavior of distributed systems situated in space can be required to satisfy spatial properties, in addition to the more widely known temporal properties. In particular, it has been previously shown that fully distributed monitors in eXchange Calculus (XC) can be automatically derived for verifying properties of situated systems expressed in the Spatial Logic of Closure Spaces (SLCS). While it has been proven that such monitors eventually compute the truth value of the desired properties, the actual time required for such computations has been thus far disregarded. In the present paper, we fill this gap by investigating the real-time guarantees that can be given in terms of upper bounds on the time taken by the XC monitors to compute the truth of SLCS properties after stabilisation of inputs.

@InProceedings{VORTEX24p32, author = {Giorgio Audrito and Ferruccio Damiani and Gianluca Torta}, title = {Real-Time Guarantees for SLCS Monitors in XC}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {32--37}, doi = {10.1145/3679008.3685545}, year = {2024}, } Publisher's Version

Identifying Potential Deadlocked Instructions in a Multi-threaded ooRexx Program
Rony G. Flatscher and Till Winkler
(Vienna University of Economics and Business, Austria)
In dynamic runtime environments, like ooRexx applications, guard-locked multi-threaded applications may be deadlocked for many reasons. Breaking deadlocked code may yield the location of a deadlocked instruction but may not allow for identifying other deadlocked threads such that the causes may be difficult or even impossible to locate. With the introduction of collectible TraceObject instances in ooRexx 5.1, a new infrastructure becomes available that can be put to work for identifying guard lock-related deadlocks on any number of threads. This article introduces the principles for creating TraceObject trace logs that can be externalized (e.g., encoded as JSON or XML text files) and internalized later as the originally ordered collection of trace objects for analyzing and processing purposes. The ooRexx guard lock-based multi-threading rules can then be used to develop an algorithm to identify all deadlocked program instructions "post immobilization," analyzing the TraceObject trace logs and supplying information about the affected objects and threads.

@InProceedings{VORTEX24p38, author = {Rony G. Flatscher and Till Winkler}, title = {Identifying Potential Deadlocked Instructions in a Multi-threaded ooRexx Program}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {38--43}, doi = {10.1145/3679008.3685546}, year = {2024}, } Publisher's Version

Runtime Verified Neural Networks for Cyber-Physical Systems
Dhiren Tripuramallu, Ayush Anand, Srinivas Pinisetty, Hammond Pearce, and Partha Roop
(IIT Bhubaneswar, India; UNSW, Sydney, Australia; University of Auckland, New Zealand)
There is increasing use of artificial neural networks in Cyber-Physical Systems (CPS) such as autonomous vehicles (AVs). Here, convolutional neural networks (CNNs) are widely used for different types of computer-vision tasks. The complex nature of the CNN makes verification of CNN-based CPS extremely difficult. Through this work, we propose a formal runtime verification (RV) approach that employs user-specified policies constructed through Valued Discrete Timed Automata (VDTA). This innovative approach serves as a powerful tool for ensuring the adherence of the system to predefined safety-critical policies, providing a formalized method to handle the complexities of CNNs in safety-critical contexts by treating them as black boxes. To demonstrate the effectiveness of this runtime verification approach, we model a CNN-based AV that is embedded with a runtime monitor. The different control units of the AV are trained using RL-based Q-Learning technique and integrate them into some of its key components. We also analyse how increase in the number of properties to be monitored affects the execution time of the overall system.

@InProceedings{VORTEX24p44, author = {Dhiren Tripuramallu and Ayush Anand and Srinivas Pinisetty and Hammond Pearce and Partha Roop}, title = {Runtime Verified Neural Networks for Cyber-Physical Systems}, booktitle = {Proc.\ VORTEX}, publisher = {ACM}, pages = {44--51}, doi = {10.1145/3679008.3685547}, year = {2024}, } Publisher's Version

proc time: 2.13