Research On The Property Verification Framework Of Adversarial Attacks On MSVL

Artificial intelligence has been widely used in various industries,such as face recognition,autonomous driving,and wise information technology of med.Machine learning is an important way to realize artificial intelligence.The application of related systems in safetycritical fields is on the rise,bringing along endless safety-related issues.Due to the problem of deep learning generalization ability,a slight tweak to the original sample would fool the deep learning model and result in misclassifications.Known as adversarial attacks,such an attack threatens the artificial intelligence system,especially image identification systems.Formal verification is based on the strict definitions of mathematical symbols,and it can verify whether the system model satisfies the expected properties.In recent years,scholars have begun to pay attention to adversarial attacks,hoping to use formal verification to study the relevant properties of adversarial attacks.However,most research studies focus on the robustness of samples;and evaluation of adversarial attacks is rare.Goodfellow et al.have pointed out that evaluation methods for adversarial attacks are lacking,thus making the evaluation of the effects of adversarial attacks difficult.Existing research plans are based on satisfiability modulo theories,mathematical representation,multi-threaded sequence operations,etc.This thesis uses PPTL(Propositional Projection Temporal Logic)to verify the properties,and judge the important properties of adversarial attacks through the verification results and achieve the purpose of evaluating adversarial attacks.Using an approach based on MSVL(Modeling,Simulation and Verification Language),this thesis proposes a research framework for the research of adversarial attacks' properties,and four kinds of properties are researched: the resistance of the sample,the recognizability of the perturbation,the transferability of the adversarial examples,and the effectiveness of adversarial attacks which are verified and analyzed in this thesis.The steps of the research framework are as follows: Firstly,through the analysis on the features of adversarial attacks,four kinds of properties are extracted,and then strict Mathematical formulas are given.Secondly,a convolutional neural network model for handwriting recognition is designed.Based on Cleverhans adversarial attacks and defense library,five kinds of adversarial attacks are implemented.Through experiments,optimal parameter configurations of each adversarial attack are confirmed,which can ensure sample sets' quality.On this basis,MSVL is used to implement the CNN model.Thirdly,four kinds of mathematical formulas of adversarial attack properties are analyzed one by one.And mathematical calculation functions are implemented by the MSVL function and PPTL propositions are defined by MSVL program variables.Based on that,mathematical formulas of properties are converted into corresponding PPTL formulas.Finally,the MSVL model and the PPTL formula are input into the PPTLCheck platform to verify the satisfaction of four kinds of properties in each sample set.There are results through analyzing the relationship between the verification results and the corresponding adversarial attack method.And results show that these properties are useful in evaluating adversarial attacks.Our research plan is practical and feasible and can be used to assist in the research of adversarial attacks.