MC-PoisonVerif: Model Checking-Driven Poisoning Attack Formal Verification Algorithm

Aiming at two core problems in data poisoning attack detection, namely the lack of formal modeling and the insufficient guarantee of theoretical completeness, this paper proposes a model checking-driven formal verification algorithm for poisoning attacks. First, the AI system is abstracted into a quadruple, and poisoning attacks (label flipping, feature perturbation, backdoor poisoning, gradient tampering) are modeled as a triple. Meanwhile, CTL* and PCTL temporal logic formulas are adopted to characterize the features of the above attacks, respectively. Second, equivalent mapping from formal features to logic formulas is established by constructing atomic propositions and Kripke structures, and automated detection and verification are realized based on the SPIN and PRISM tools. Furthermore, three core theorems are proposed and strictly proved: the characterization completeness theorem of the formal model for poisoning attacks, the completeness and correctness theorem of the detection algorithm, and the robustness theorem of the defense framework. Theoretical proofs and experimental results demonstrate that, when the proportion of malicious samples is no more than 20%, the missing detection rate is ≤2% and the false detection rate is ≤3.5%. After defense deployment, the accuracy drop of the model is controlled within 8%. This work provides a formally verifiable and theoretically guaranteed solution for poisoning attack detection in AI systems.