Runtime Invariant Checking in Robotic Systems and Deep Learning Models (Keynote)

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.