A symbolic execution-based method to perform untargeted attack on feed-forward neural networks

DeepCheck is a symbolic execution-based method to attack feed-forward neural networks. However, in the untargeted attack, DeepCheck suffers from a low success rate due to the limitation of preserving neuron activation patterns and the weakness of solving the constraint by SMT solvers. Therefore, this paper proposes a method to improve the success rate of DeepCheck. Compared to DeepCheck, the proposed method has two main differences including (i) does not force to preserve neuron activation patterns and (ii) uses a heuristic solver rather than SMT solvers. The experimental results on MNIST, Fashion-MNIST, and A-Z handwritten alphabets show three promising results. In the 1-pixel attack, while DeepCheck obtains an average of 0.7% success rate, the proposed method could achieve an average of 54.3% success rate. In the n-pixel attack, while DeepCheck obtains an average of at most 16.9% success rate for using the Z3 solver and at most 26.8% for using the SMTInterpol solver, the proposed method achieves an average of at most 98.7% success rate. In terms of solving cost, while the average running time of the proposed heuristic solver is around 0.4 s per attack, the average running time of DeepCheck is usually larger significantly. These results show the effectiveness of the proposed method to deal with the limitation of DeepCheck.