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.

翻译：自动驾驶和工业物联网等安全关键应用正在采用基于深度神经网络（DNN）的语义通信系统，通过仅传输与任务相关的语义特征来降低带宽并提高传输速度。然而，针对这些基于DNN的语义通信系统的对抗攻击，可以通过操纵传输的语义特征导致灾难性故障。现有的防御机制依赖于经验性方法，无法针对完整的对抗性扰动谱提供形式化保证。我们提出了VSCAN，一种神经网络验证框架，通过将对抗噪声生成表述为混合整数规划问题，并验证跨多个互连网络（编码器、解码器和任务模型）的端到端属性，从而提供数学上的鲁棒性保证。我们的核心见解是，现实的对抗约束（功率限制和统计不可检测性）可以被编码为逻辑公式，从而能够使用最先进的DNN验证器进行高效验证。我们在600个表征各种攻击者能力的验证属性上的评估表明，VSCAN在发现漏洞方面与攻击方法相当，同时为44%的属性提供了形式化鲁棒性保证——考虑到多网络验证的复杂性，这是一项重要成就。此外，我们揭示了一个根本性的安全与效率权衡：与64维潜在空间相比，紧凑的16维潜在空间实现了50%的已验证鲁棒性。