D4+: Emergent Adversarial Driving Maneuvers with Approximate Functional Optimization

TL;DR

This paper introduces a formal, scenario-based framework using metric temporal logic to identify vulnerabilities in autonomous vehicles caused by malicious drivers, aiming to enhance safety verification in adversarial environments.

Contribution

It presents a novel formal method framework for testing autonomous vehicle safety against malicious environment interactions using MTL specifications.

Findings

Identifies safety violations in autonomous vehicle scenarios

Provides a method to find malicious behaviors exploiting vehicle vulnerabilities

Helps designers define safe operational boundaries

Abstract

Intelligent mechanisms implemented in autonomous vehicles, such as proactive driving assist and collision alerts, reduce traffic accidents. However, verifying their correct functionality is difficult due to complex interactions with the environment. This problem is exacerbated in adversarial environments, where an attacker can control the environment surrounding autonomous vehicles to exploit vulnerabilities. To preemptively identify vulnerabilities in these systems, in this paper, we implement a scenario-based framework with a formal method to identify the impact of malicious drivers interacting with autonomous vehicles. The formalization of the evaluation requirements utilizes metric temporal logic (MTL) to identify a safety condition that we want to test. Our goal is to find, through a rigorous testing approach, any trace that violates this MTL safety specification. Our results can help designers identify the range of safe operational behaviors that prevent malicious drivers from exploiting the autonomous features of modern vehicles.