VPN: Verification of Poisoning in Neural Networks

TL;DR

This paper introduces a verification method for detecting data poisoning in neural networks by formulating poisoning checks as properties verifiable with existing tools, enabling detection of triggers that cause misclassification.

Contribution

It presents a novel approach to verify data poisoning in neural networks using formal tools, including transferability of triggers across models and applicability to real-world image classifiers.

Findings

Verification of poisoning triggers is feasible with existing tools.

Discovered triggers transfer from small to large models.

Applicable to state-of-the-art image classification models.

Abstract

Neural networks are successfully used in a variety of applications, many of them having safety and security concerns. As a result researchers have proposed formal verification techniques for verifying neural network properties. While previous efforts have mainly focused on checking local robustness in neural networks, we instead study another neural network security issue, namely data poisoning. In this case an attacker inserts a trigger into a subset of the training data, in such a way that at test time, this trigger in an input causes the trained model to misclassify to some target class. We show how to formulate the check for data poisoning as a property that can be checked with off-the-shelf verification tools, such as Marabou and nneum, where counterexamples of failed checks constitute the triggers. We further show that the discovered triggers are `transferable' from a small model to a larger, better-trained model, allowing us to analyze state-of-the art performant models trained for image classification tasks.