人工智能已在社会各行业得到了广泛应用,如人脸识别、自动驾驶、智慧医疗等。机器学习是实现人工智能的重要途径,相关系统在安全攸关领域的应用不断增加,随之而来的安全问题也层出不穷。由于深度学习泛化能力不足,通过对原样本添加微小扰动即可导致深度学习模型输出错误分类结果,这种方法被称为对抗攻击,它给人工智能系统带来了很多威胁,尤其是图像识别系统。形式化验证基于严格的数学符号定义,能够验证系统模型是否满足期望性质。近年来,学术界开始关注对抗攻击,希望借助形式化验证来研究对抗攻击的相关性质,不过研究点大多集中于健壮性,鲜见对抗攻击的评估。Goodfellow等人认为对抗攻击缺少相应的评估手段,难以评估对抗攻击的效果。目前已有的研究方案以可满足模块理论、数学表示、多线程序列运算等为基础,本文则立足于命题投影时序逻辑（Propositional Projection Temporal Logic,PPTL）验证性质的能力,通过验证结果断定对抗攻击的重要性质满足与否,以此达到评估对抗攻击的目的。本文提出一种基于时序逻辑程序设计语言（Modeling,Simulation and Verification Language,MSVL）的对抗攻击相关性质的验证框架,研究了样本抵抗性、扰动可识别性、对抗样本迁移性以及对抗攻击有效性的4种性质,并对4种性质进行了验证与分析。该框架的具体流程为:首先,通过分析对抗攻击方法特点,提取了以上4种性质,并给出了严格的数学公式定义;其次,设计针对训练手写识别体的CNN模型,基于Cleverhans对抗攻击防御库来实现4种对抗攻击方法,通过实验确定较佳参数配置,输出高质量对抗攻击所生成的样本集,在此基础上使用MSVL实现CNN模型;然后,逐一分析4种对抗攻击性质的数学公式,使用MSVL函数实现数学计算函数,基于MSVL程序变量定义PPTL命题,将性质数学公式转换为对应的PPTL公式;最后,将MSVL模型与PPTL公式输入PPTLCheck平台,验证4种性质在所有样本集上的可满足情况,分析了验证结果与相应对抗攻击方法的关系,结果表明这4种性质具备一定的评估对抗攻击的能力,本文方案具有实用性及可行性,可用于辅助研究对抗攻击。