Verifying DNN-based Semantic Communication Against Generative Adversarial Noise

TL;DR

This paper introduces VSCAN, a verification framework that provides formal robustness guarantees for DNN-based semantic communication systems against adversarial noise, addressing security vulnerabilities with mathematical proofs.

Contribution

VSCAN formulates adversarial noise as mixed integer programming problems and verifies end-to-end properties across interconnected networks, offering formal guarantees unlike empirical defenses.

Findings

VSCAN verifies 44% of properties with robustness guarantees.

Compact latent spaces (16D) achieve 50% verified robustness.

VSCAN matches attack methods in vulnerability detection.

Abstract

Safety-critical applications like autonomous vehicles and industrial IoT are adopting semantic communication (SemCom) systems using deep neural networks to reduce bandwidth and increase transmission speed by transmitting only task-relevant semantic features. However, adversarial attacks against these DNN-based SemCom systems can cause catastrophic failures by manipulating transmitted semantic features. Existing defense mechanisms rely on empirical approaches provide no formal guarantees against the full spectrum of adversarial perturbations. We present VSCAN, a neural network verification framework that provides mathematical robustness guarantees by formulating adversarial noise generation as mixed integer programming and verifying end-to-end properties across multiple interconnected networks (encoder, decoder, and task model). Our key insight is that realistic adversarial constraints (power limitations and statistical undetectability) can be encoded as logical formulae to enable efficient verification using state-of-the-art DNN verifiers. Our evaluation on 600 verification properties characterizing various attacker's capabilities shows VSCAN matches attack methods in finding vulnerabilities while providing formal robustness guarantees for 44% of properties -- a significant achievement given the complexity of multi-network verification. Moreover, we reveal a fundamental security-efficiency tradeoff: compact 16-dimensional latent spaces achieve 50% verified robustness compared to 64-dimensional spaces.