精华内容
下载资源
问答
  • 人工智能系统的形式化验证技术研究进展与趋势国际研究现状   这是《2019-2020中国计算机科学技术发展报告》中的一篇报告,主要从形式化方法的角度观察过去三年内(主要从2017年起)基于形式化方法的人工智能


      这是《2019-2020中国计算机科学技术发展报告》中的一篇报告,主要从形式化方法的角度观察过去三年内(主要从2017年起)基于形式化方法的人工智能系统安全可信研究的进展。
      我在这里对其做一个概括介绍,希望自己能够坚持写学习笔记,养成一个良好的记录习惯。

    国际研究现状

    人工智能系统安全内涵

      关于人工智能系统的可信性目前并没有统一的定义。大多数文献主要围绕其某个具体的性质进行研究。目前主要研究的性质包括:鲁棒性,安全性,可靠性,可解释性等性质。

      鲁棒性从狭义上讲,指的是对于系统的输入数据中出现的小的偏差(噪声)以及非正常分布的数据,系统的结果和性能不应当受到大的影响。文章里后续讨论的也都是狭义上的鲁棒性,系统的鲁棒性是安全性的前提,有些文献里也将安全性简单地专指为鲁棒性。

      普林斯顿大学的研究人员综合考虑了可信机器学习中的隐私性和鲁棒性,并且通过分析高鲁棒模型的内部结构特征,提出了新的基于对抗样本预测的“成员推断攻击”的概念[5]。“成员推断攻击”的原理是通过判定特定的数据是否属于目标机器学习的训练集/测试集,对学习目标进行攻击,提出“鲁棒模型往往泄漏了更多的成员数据信息”和“其训练算法本身往往使得模型对训练数据更加敏感”等结论。

    此外,本文还给出了一些与可信性相关的性质的形式化表示:
    输出可达性P( f,η),表示输入空间η中所有输入的输出结果集合。
    区间属性I( f,η),表示一个能包含P( f,η)的凸集合,我们称I( f,η)为一个区间。
    利普希茨属性,一个函数 f 是利普希茨连续的当其满足|| f(y) – f(x) || ≤ K|| y – x ||,直观地讲,利普希茨连续限制了函数的变化速度不能超过某个具体的值,Lips( f,η,Lp)表示函数 f 在η上的利普希茨值。

    文献[9]中给出了上述性质之间的关系,如图1所示,箭头表示后者可以通过前者计算得到。
    在这里插入图片描述

    人工智能系统形式化验证技术

    现有的深度神经网络的验证工作可以分为以下几个类别:
    ● 确定性保证,即可以“确定”地阐述某个性质是否成立。
    ● 单边性保证,即只需提供一个“上界”或者“下界”,便可判断某个性质是否成立。
    ● 收敛性保证,即针对某个性质成立提供“收敛”的上下界。
    ● 统计性保证,即量化某个性质成立的“概率”。

    确定性保证:确定性保证方法首先将所验证问题转化成为一个约束的集合(无论是否具有优化目标函数),然后使用约束求解的方法来解决这个问题。此类方法主要依赖于当下各类约束求解器,譬如SMT求解器、SAT求解器、线性规划求解器、混合整数规划求解器等。

    基于SMT/SAT的求解方法,2010年文献[12]中提出了一种基于SMT求解的抽象精化方法来验证神经网络;2017年文献[14]提出了针对神经网络的得SMT求解器Reluplex;2019年文献[16]提出了Marabou框架,可以验证全连接和卷积神经网络。除了基于SMT的求解验证,文献[17-18]于2018年提出了基于SAT求解来验证一类特殊的神经网络,即二值神经网络。

    基于混合整数规划(MILP)的求解方法,2017年文献[19]将全连接神经网络编码成混合整数规划,把其上的ReLU激活函数表达成一系列混合整数规划,以便计算输出范围。同年,文献[20]在混合整数规划的基础上加入了启发法来加速求解过程。

    单边性保证:这类方法的优势在于它避免了现有约束求解器的实现过程中可能会出现的浮点问题,大部分现有的约束求解器在进行浮点计算时只能提供估计值,所以有可能发生计算出的估计值不是真实最优解的情况。

    抽象解释,神经网络可以看作是一类特殊的程序,输入一般是高维的,激活函数是非线性的。因此,对神经网络进行精确推理代价很大,需要用抽象解释对网络的具体语义进行抽象。苏黎世理工学院(ETH)的一个研究组最早提出了一种基于抽象解释的框架AI2,来验证神经网络的安全性和鲁棒性[28]。在这之后,ETH研究组面向神经网络验证设计了专门的子多面体抽象域[32]。为了提高验证的精度,ETH研究组还将基于抽象解释的方法和更精确的基于线性规划的方法进行了结合[33]

    线性近似,文献[35]在考虑激活函数为ReLU的神经元时,提出了在局部对神经网络用线性函数做上近似和下近似,从而帮助验证鲁棒性的Fast-Lin算法。2019年,文献[39]提出了针对循环网络结构的POPQORN算法,可以用来验证简单的RNN、长短期记忆(LSTM)和GRU(Gated Recurrent Unit)等。
    凸优化,2018年,文献[40]提出了凸优化的方法来学习包含ReLU激活函数的神经网络。

    区间分析,2018年,文献[42]提出区间运算可以用于计算深度神经网络的输出结果的界值。

    输出可达集估计,2018年,文献[44]提出了另一种叫作输出可达集估计的方法来评估神经网络的鲁棒性。

    收敛性保证:上述提到的验证方法通常只能运用在小型网络上,譬如隐藏神经元在千个数量级别的网络。这里要介绍的是对于较大型深度神经网络的验证可以提供收敛性保证的方法,即同时提供针对某个性质成立的上界以及下界,并且证明这两个上下界收敛。

    逐层精化,文献[8]于2016年提出了一个可以自动化验证深度神经网络的基于SMT的框架,它采用了逐层精化的方法,从神经网络的输入层分析至其隐藏层并且最终可以达到输出层。

    双选手博弈,文献[46]在2018年针对深度神经网络的鲁棒性提出了两个研究问题:一是最大安全半径问题;二是特征鲁棒性问题。这两个问题又可以转换成双选手轮流博弈的最优解,在此博弈中,一位选手选择输入图片上的特征,另一位选手则判断在选定的特征内如何干扰。

    全局优化,2018年,文献[10]证明了现有深度神经网络中大部分的层都是利普希茨连续的,从而在此基础上利用全局优化提出了针对神经网络的DeepGO验证算法。

    统计性保证:利用一个量化的概率值表示性质是否被满足或者某个值是否是下界等问题的结果。

    基于极限值理论的利普希茨常数估计,2018年,文献[51]提出了一种名为CLEVER的度量,并以此来估计利普希茨常数的值。

    鲁棒性估计,2016年,文献[53]针对神经网络中存在反例的频率和严重度分别提出了两种对于鲁棒性的统计度量方法,此种方法基于上文引入的最大安全半径问题。

    人工智能系统的测试技术

    从三个方面对当前国际上比较流行的深度学习模型测试方法加以总结,即:
    ● 现有深度学习模型的测试标准。
    ● 现有针对深度学习模型生成测试用例的测试技术。
    ● 其他测试技术在神经网络中的应用。

    测试标准:根据覆盖粒度,神经网络的测试覆盖准则可分为三类:神经元覆盖、网络层级覆盖、神经元对覆盖。

    神经元覆盖,这是最早被提出的深度学习模型测试标准,神经元覆盖率指标可以视为软件测试中语句覆盖的一个变种[54]。它将神经元被激活与否作为该神经元是否被覆盖的标准,并将整个测试集中被激活的神经元的比例,即神经元覆盖率,作为衡量模型测试程度的指标。不过该指标在实际中过于容易实现,因而对评价模型的被测试程度并没有太多指导意义。

    网络层级覆盖,鉴于神经元覆盖率的局限性,马等人在其工作DeepGauge[58]中提出网络层级的top-k神经元覆盖准则。

    神经元对覆盖,文献[57]提出了一个扩展指标MC/DC,直观上讲是说如果一个神经元被覆盖,那么所有可能影响到该神经元激活情况的神经元(激活与否)都应当被测试所覆盖。

    测试技术:神经网络测试技术的主要手段是针对当前模型,生成针对提升某一测试指标更加有效的测试用例,添加所生成测试用例到原先训练数据集进行模型的重新训练,以期来增强最终训练出神经网络的安全性和鲁棒性。

    变异测试,南京大学陈等人[60]提出了模型层面的变异算子,对神经网络的结构直接进行变异操作生成变异神经网络,用于评估神经网络测试数据集的完整性。

    蜕变测试,蜕变测试是根据判断多个输入输出之间的关系是否被满足,来判断被测软件的正确性。利用该方法,DeepTest[63]将蜕变测试应用在基于深度神经网络的自动驾驶系统上,主要用来测试深度神经网络是否对同样场景不同天气条件的情况输出相似的转向角,即自动驾驶系统不受天气因素的影响或影响较小。

    测试用例生成方法,有一系列针对覆盖指标生成测试用例的方法。例如,文献[54]结合差分测试,通过求解联合目标优化问题生成测试用例,以使得多个神经网络判别出现分歧同时尽可能提高神经元覆盖率。

    其他测试技术在神经网络中的应用:除了上述测试方法之外,一些新的测试技术为神经网络测试提供了不同的角度和思想。例如,文献[56]发现攻击样本在输入和模型扰动下相比正常样本有更高的敏感度,因此提出利用此特点并结合变异测试从输入样本中检测攻击样本。

    人工智能系统的可解释性

    人工智能的可解释性是近年来提出的一个概念,指人工智能系统决策机制能够被人类理解的程度[66]

    特征排序:目前主要的特征排序方法可以归为两大类:基于反向传播和基于输入扰动,两种特征排序方法往往都依赖于启发式算法来实现。

    文献[67]中针对ConvNet模型的图片分类可视化工作是反向传播方法早期的典型代表。其中,ConvNet图像分类器在一个具体输入点附近的行为被近似为一个线性方程,这个线性方程的参数是通过对网络在这个具体输入点上进行求导获得的。以后的基于反向传播的特征排序工作也多沿袭了对机器学习模型的函数求导。

    与上文提到的只需要一次反向传播的特征提取方法不同,基于扰动的方法通过反复采样输入空间来寻求更高的准确度。LIME[74]是基于输入扰动的特征排序的诸多方法中很典型的一种。给定一个输入,LIME通过覆盖一部分输入特征来在给定输入点附近进行采样,并通过分析这些样本与机器学习模型分类结果之间的变化关系,来构建这个机器学习模型在采样点附近的线性行为模型,然后以此对输入特征的重要性进行排序。

    量化追踪:最新的研究发现,对信息流在神经网络各个隐藏层表示的统计特性进行追踪,是理论理解深度学习的训练过程的关键。而信息论作为研究信息的基础理论,被用来量化深度学习的训练过程,起源于以色列理工的Tishby的团队在2015年和2017年的开创性工作[81-82]。其主要思想是把DNN的训练过程放入信息瓶颈的框架之中,把DNN的学习过程和泛化过程用两个互信息量来衡量。

    人工智能系统建模

    对神经网络系统本身如何进行形式化建模目前还处于探索阶段。研究者们目前提出的各种技术,主要有有限自动机、规则集合、决策树和程序等。

      由于有限自动机与神经网络(尤其是RNN)之间存在着很大相似,大多数研究工作采用有限自动机来表示神经网络的知识萃取或模型。早期的自动机提取技术主要采用层次聚类分析来分析神经网络的连续空间状态[89-91]。此外,有些研究者提出了基于采样的方式来提取自动机,文献[101]中提出了第一个基于采样的方法。但这些基于采样的方法存在着宏观状态的不一致性问题。

      为了解决不一致问题,概率自动机[106]这个方案被提了出来,文献[107]提出了一个从RNN中提取概率自动机的方法。

      上述方法都属于白盒方法,需要了解神经网络的结构及其内部状态。一些研究者提出了与之相反的黑盒方法,例如,文献[117]提出了一种从应用于序列数据的黑盒系统中提取权重自动机的学习方法。

      近两年,还有一些研究者试图从形式语言的角度来理解RNN,文献[128]结合了近似可能正确和约束求解,提出了从RNN中提取线性时序逻辑的方法,以解释RNN的决策过程。

    对抗攻击与形式化验证

    攻击技术的目的在于给缺少理论保证的深度神经网络提供实例证明,与之对应的是防御技术,可以通过提高神经网络的鲁棒性来减少对抗样本的数量,也可以从矫正输入中取出对抗样本。

    对抗攻击:现存的大多数攻击技术主要是针对计算机视觉方面的对抗样本。这里列举几个比较有代表性的产生对抗样本的方法:有限存储的BFGS算法(L-BFGS)[7],FGSM(Fast Gradient Sign Method)[142],JSMA[144],DeepFool[145],C&W[146]

    通过自然转换的对抗攻击:除了上述能够发现像素级别的对抗攻击的方法,还可以通过自然转换来挑选对抗样本。包括对输入图像进行旋转和平移[149],基于流场的空间转换的对抗样本[150]

    更加实际的机器学习验证:裴等人[151]为了评估DNN等的鲁棒性,提出一个带有12个实际转换的通用模型(VeriVis),分别是均值平滑、中值平滑、腐蚀、膨胀、对比度、亮度、闭合、旋转、修建、尺度变化、平移和映射。对所有的输入都穷尽这些变换以验证给定的DNN的鲁棒性。

    对抗攻击技术的总结:表1从五个方面,总结了常用对抗攻击方法的主要相似点和不同点。
    在这里插入图片描述

    国内研究现状

    人工智能系统安全内涵

      中国科学院何积丰在2017年首次提出可信人工智能的概念,他认为可信人工智能应该具备与人类智能类似的特质,表现为鲁棒性、自我反省、自适应、透明性和可解释性,以及公平性。为了对智能系统不确定环境的形式化建模理论进行扩展,何积丰提出了基于程序代数的概率程序演算模型[158]

      在人工智能系统的可信度量方面,李德毅在其专著《不确定性人工智能》中提出用超熵来度量智能系统的不确定性,并对不确定性人工智能研究的发展方向进行了展望[160]

      在人工智能安全体系架构和标准体系方面,方滨兴在其专著《人工智能安全》中提出人工智能安全体系架构,并提出了相关的人工智能安全伦理准则[165]。中国电子技术标准化研究院、清华大学、百度、华为、360、阿里巴巴等联合编写的《人工智能安全标准化白皮书》对人工智能系统安全风险的内涵进行了分析,并提出了一系列针对人工智能安全的标准体系[166]

    人工智能系统形式化验证技术

      目前,国内对人工智能形式验证的工作主要集中在神经网络、深度学习程序以及黑盒系统的验证工作。

      在神经网络的形式化验证方面,中科院软件所、国防科技大学、英国利物浦大学的团队合作研究提出了一种基于符号传播的方法来提高基于抽象解释的神经网络验证的精确性[30]

      北京大学、国防科技大学、香港科技大学的团队合作研究关注开发者编写的深度学习程序本身(即神经网络架构,如采用TensorFlow编写的程序)的缺陷,主要技术途径是将基于抽象解释的静态分析方法应用于人工智能深度学习程序中数值缺陷的检测[169]

      在黑盒系统形式验证方面,中科院软件所薛白、北京大学孙猛等人合作提出了一种在可能近似正确学习框架下计算黑盒系统安全输入特征集的线性规划方法[170]

    人工智能系统的测试技术

      近年来,国内学者在神经网络测试方面做了大量的工作,并取得系列重要进展。这里对其中的测试覆盖准则、测试用例生成等主要方面做简要介绍。

      在神经网络测试方面,在DeepGauge[58]基础上,哈尔滨工业大学马雷等人也提出了基于变异的覆盖制导模糊测试技术DeepHunter,以生成测试用例实现高覆盖度测试[172]

      南京大学冯洋与陈振宇等人基于变异测试技术提出了模型层面的变异算子,该团队还提出了DeepGini[176]技术,用于神经网络的测试用例排序。清华大学软件学院姜宇等提出了基于差分对抗模糊测试的测试用例生成和后门检测加固工作[178-180],实现对抗样本的快速生成和后门数据的高效植入。

      北京大学孙猛团队提出从模型输出不确定性的角度来区分正常样本和攻击样本,并发现了许多不易被之前测试方法所覆盖的攻击样本[181]

    人工智能系统的可解释性

      在人工智能可解释性方面,相关研究近两年来得到了广泛的关注,国内研究者在该方面有了一定的快速发展。

      其中,上海交通大学的张拳石团队对卷积神经网络、生成网络等的可解释性都有较为充分的研究[190-191]。该系列研究通过解释图、决策树等方法对卷积神经网络进行可解释分析和图解。北京大学的朱占星团队在经过对抗训练的卷积神经网络进行了初步的可解释性探索[193]

      国内在特征排序的研究上也取得了一系列的成果。在文献[194]中,来自中科院、南京大学、京东安全中心的学者与美国宾夕法尼亚州立大学和弗吉尼亚理工大学的学者合作,研究了针对安全软件的深度学习系统的特征排序。清华大学的刘奕群、马少平等人在文献[195]中将用户评论作为推荐系统的特征,通过对评论的排序来提高推荐系统的性能。

    人工智能系统建模

      在人工智能系统建模方面,国内研究者也取得了一些相关成果。

      南京大学周志华团队提出了一种从神经网络集成器中提取符号化规则的方法REFNE[199],和一种基于聚类算法从RNN中提取自动机的算法[200]。上海交通大学张拳石等人[192]提出了从CNN中提取决策树的方法,该方法的思想是将中间特征层分别与语义对象和CNN的预测关联起来。

    对抗攻击与形式化验证

      近年来,国内学者在神经网络的对抗攻击方面取得一些初步的研究成功,主要工作集中在2018年以后,主要以和国外的研究机构合作为主,现阶段作者全部是国内团队的工作还比较少。这里着重介绍黑盒对抗攻击算法,相比白盒攻击算法,黑盒攻击对算法有更高的要求。

      京东AI研究院的易津锋与美国加州洛杉矶大学和IBM合作,于2018年将针对硬标签的黑盒攻击问题转化为一种找寻到决策边界最短距离的方法,提出了Opt-Attack的黑盒对抗攻击算法[202]。与此同时,为了寻找到合适的对抗攻击策略并且能够有效地提升模型本身的鲁棒性,清华大学的朱军团队提出了基于动量的迭代算法来构造对抗攻击样本,取名为MI-FGSM[206],它能同时成功攻击白盒和黑盒模型。

      此外,国内还有一些团队结合进化算法和遗传算法提出了一些新的对抗攻击算法。比如,浙江工业大学的陈晋音团队提出了一种利用不同噪声点的像素阈值、噪声点数量和噪声点大小三个参数来产生不同的扰动的攻击方法,取名为POBA-GA[208]

    国内外研究进展比较

      从前面介绍过的六个方面进行比较分析:

      针对人工智能安全内涵,当前国内外都尚未形成统一的标准。如何从不同的维度全面地刻画人工智能系统的安全,并利用形式化的方法给出严格的定义,是目前国内外都需要解决的关键问题。

      在人工智能系统的形式化验证方面,目前国内外都比较聚焦于系统鲁棒性的验证。主要原因有两个:一是鲁棒性是智能系统可靠性的一个重要的参数之一。另一个原因是鲁棒性在数学中有精确的定义,因此在形式化方法中相对容易描述与验证。与国际上关于智能系统的形式化验证相比,国内的相关的研究相对较少,同时缺乏原创性的成果。另外,由于智能系统中智能模块的不可解释性和结构复杂性,在系统的形式化描述,性质的形式化定义,以及算法的可扩展性等核心问题上,至今国内外研究依然停留在理论阶段,尚无有效的方法解决工业领域内智能系统的验证问题。

      在人工智能系统测试方面,近三年来国内在人工智能系统测试领域取得了一系列重要前沿成果,并处在国际前沿水平。不过由于当前大部分智能系统本身的不可解释性,相关的测试标准依然缺少足够的理论基础以确保测试结果的可靠性和准确性。

      在人工智能系统可解释性方面,相对于国外研究,国内众多团队形成了自己的研究特色。不过,目前的国内外研究大多基于启发式方法,还缺乏对可解释性的严格统一定义,亟待提出严格的理论框架对可解释性进行建模和相应的理论分析。

      关于神经网络知识模型构建方面的研究,绝大多数活跃在国外,国内对于这方面的研究尚未开始重视,活跃在这一领域的学者还不够多,同传统的形式化建模尚未形成一定的联系。

      对抗攻击技术作为生成测试用例的一种特殊方法,如何将对抗攻击与传统的测试用例生成技术相结合,生成有效的测试数据,如何根据测试结果更好地提升系统的安全可靠性,都是当前需要解决的问题。

    发展趋势与展望

      人工智能系统的可信性已经逐渐成为制约人工智能技术在安全攸关领域应用的关键问题。可以预见,人工智能的可信性问题将会是工业界与学术界共同关注的焦点。

      另外,因为人工智能经常被用来处理非常复杂的、高维度的输入数据,一个最直接的问题便是决定输入数据的哪些特征真正对人工智能的判断起了关键影响。在可预见的未来,特征排序会在人工智能领域起到越来越重要的作用。

      随着神经网络规模越来越大,结构越来越复杂,以往的算法可能不再适用,如何从这些新型复杂网络中提取知识,特别是可解释可分析的形式化模型,可能是未来研究的一个关注点。从模型的角度,如何从神经网络提取表达能力更强的模型也是未来研究方向之一。

    参考文献

      参考文献数量过多,原谅我的懒惰,就不一一列出来了。有兴趣的同学可以访问https://dl.ccf.org.cn/books/detail.html?_ack=2&id=5161520744974336查看原文,或者留言找我获取。

    展开全文
  • 基于层次组合抽象的智能系统形式化验证.pdf
  • 高可靠性智能灌溉系统的形式化验证方法.pdf
  • 近期,笔者注意到一款智能合约自动形式化验证工具Beosin—VaaS推出了离线免费版。所谓**“离线免费版”,相较于之前该公司推出的在线免费版、企业版而言,亮点自然不言而喻。对于开发者来说,离线版的验证工具将提供...

    形式化验证工具之离线免费版Beosin—VaaS

    近期,笔者注意到一款智能合约自动形式化验证工具Beosin—VaaS推出了离线免费版。所谓**“离线免费版”,相较于之前该公司推出的在线免费版、企业版而言,亮点自然不言而喻。对于开发者来说,离线版的验证工具将提供一个不联网的测试环境,在很大程度上能从根源上将黑客攻击的可能拒之门外。
    在这里插入图片描述
    经笔者测试,虽然这次推出的版本为免费版,但功能毫不逊色,依然能
    有效检测出智能合约的常规安全漏洞,并精确定位到有风险的代码位置,以及导开发者修改合约代码。**对大多数智能合约的安全性而言,需求都已经满足。在此附体验网址:https://beosin.com/#/,有需要的朋友可自行前往体验。

    尽管笔者认为离线免费版Beosin—VaaS的功能已足够强大,但根据官方发布的消息,对于一些复杂类型的业务合约、以及对安全性要求高的业务合约,比如数字金融类(如DeFi)、物流供应链类、跨境支付类、防伪溯源类等等,还是建议选择企业版Beosin—VaaS人工审计服务更好。

    下面笔者将针对这款离线免费版Beosin—VaaS工具进行简单展述。

    1.什么是形式化验证技术?

    其实,形式化验证技术最早是应用于航空、军事等领域的安全关键软件中的技术,本身受众范围没那么广。当成都链安最早尝试将形式化验证技术应用在验证智能合约的安全性上,最后发现审计效果比起传统的验证方式,更具备优势。

    **形式化验证技术是一种基于数学和逻辑学的方法。**具体来讲,在智能合约部署之前,对其代码和文档进行形式化建模,然后通过数学的手段对代码的安全性和功能正确性进行严格的证明,可有效检测出智能合约是否存在安全漏洞和逻辑漏洞。

    该方法可有效弥补传统靠人工经验查找代码逻辑漏洞的缺陷,其优势在于,用传统的测试等手段无法穷举所有可能输入,而用数学证明的角度,就能克服这一问题,提供更加完备的安全审计。

    2.什么是Beosin—VaaS工具?

    Beosin—VaaS相关工具就是将形式化验证技术应用在对智能合约安全性验证的集大成者。Beosin—VaaS能够面向EVM和WASM智能合约,自动化检测智能合约的10大项32小项常规安全漏洞,为智能合约提供**“军事级”的安全保护**;并精准定位风险代码位置并给出修改建议;检测准确率>97%,全球最高;从源码到字节码完备的形式化验证;支持多个智能合约编程语言,如Solidity、Go、C++、Python等。

    3.一些Beosin—VaaS的测试实例

    笔者选取了655个测试问题进行检测,Beosin—VaaS工具总计检测出635个问题,命中率为96.9%;误报共115个,误报率为15.3%。因此,Beosin—VaaS工具可检测出业务类大多合约案例,具体检测项如下:

    Beosin—VaaS工具检测项

    漏洞检测项Beosin—VaaS工具
    ERC20 标准规范
    Fake Recharge Vulnerability(假充值)
    TransferToZeroAddress(目标零地址检测)
    Re Entrancy(重入)
    TXOriginAuthentication(tx.origin使用错误)
    Invoke Low Level Calls(call调用,delegatecall调用,自杀函数调用)
    BlockMembers Manipulation(区块参数依赖)
    Invoke Extcodesize(调用Extcodesize函数)
    Invoke Ecrecover(调用Ecrecover函数)
    Unchecked Call Or Send Return Values
    (call和send的返回值检测)
    Redefine Variable From Base Contracts(合约继承中的变量覆盖)
    Unprotected Ether Withdrawal(无保护的转账)×
    Check This Balance(合约资金受到严格限制)
    ArbitraryJumpwith Function(具有函数类型变量的任)
    Overload Assert(重写assert函数)
    CompilerVersionDeclaration(编译器版本声明)
    Constructor Mistyping(构造函数失配)
    Unary Operation(+= 写成=+ )
    No Return(返回值适配)
    Unchecked Api Return Values(没检查API返回值)
    Emit Event Beforerevert(事件在revert前触发了)
    Integer Overflow(整数溢出)
    Exception State(异常检测,包括数组越界、除0、assert失败等))
    Call problem
    Function problem
    Require Fail

    通过大体测试,离线免费版自动形式化验证工具Beosin—VaaS在很大程度上都能够满足大多数开发者的验证需要。大家可以前往https://beosin.com/#/进行体验,不吝赐教。

    展开全文
  • 基于这样的背景,本体生态伙伴成都链安(Beosin)推出以太坊后全球第二个高度自动化智能合约形式化验证平台——VaaS-ONT。 早在去年7月,成都链安加入本体“共建者计划”,与本体共同聚焦于区块链智能合约开发、...

    在区块链技术领域,智能合约一直在多语言开发环境中发挥着至关重要的作用。如此一来,保证智能合约的安全显得尤为重要。基于这样的背景,本体生态伙伴成都链安(Beosin)推出以太坊后全球第二个高度自动化智能合约形式化验证平台——VaaS-ONT。
    在这里插入图片描述
    早在去年7月,成都链安加入本体“共建者计划”,与本体共同聚焦于区块链智能合约开发、安全审计、形式化验证等领域,以提高智能合约和底层链平台的安全性,进一步打造安全、放心、可靠的区块链基础设施。VaaS-ONT 作为成都链安继以太坊后开发的第二个公链形式化验证安全产品,已在本体智能合约集成开发环境 SmartX 中深度集成。
    在这里插入图片描述
    本体智能合约集成开发环境 SmartX

    VaaS-ONT 依托成都链安形式化验证技术在民航、军事领域多年的深厚积累,带来“军事级”形式化验证服务。相较于人工审计智能合约的传统安全防护手段,VaaS-ONT “一键式”形式化验证工具能够精确定位到有风险的代码位置,迅速找出原因,有效验证智能合约或区块链应用的常规安全漏洞、安全属性和功能正确性,从而显著提高安全等级。

    开发者可通过进入 VaaS-ONT 产品官方链接全方位体验:

    https://smartx.ont.io/

    在这里插入图片描述

    VaaS-ONT 产品页面

    锁定下方即刻体验

    VaaS-ONT 产品官方链接

    https://smartx.ont.io/

    形式化验证工具 VaaS-ONT 相关资料

    https://github.com/ontio/ontology-python-compiler/tree/master/vaas

    形式化验证工具VaaS-ONT 测试用例

    https://github.com/ontio/ontology-python-compiler/tree/master/vaas/example

    《本体形式化工具检测功能列表》:

    https://github.com/ontio/ontology-python-compiler/tree/master/vaas

    关于形式化验证

    ✔ 基本介绍

    形式化方法是计算机科学中一种面向软硬件的基于规约、开发以及验证的数学方法。将形式化方法应用于软硬件设计的动机,是为了使其如其他工程规范一样,借助于数学分析的方法加强系统的可靠性和稳固性。

    在这里插入图片描述

    为基于符号执行的模型检测技术形式化验证工具设计原理图

    在区块链智能合约领域,形式化验证使用数学和逻辑语言精确定义智能合约、智能合约的运行环境以及智能合约的正确性和安全性,并通过数学证明和逻辑推理来证明智能合约的确满足其正确性和安全性定义。与传统测试方法相比,形式化方法通常更加精确,并严格地保证较高的覆盖率。在正常的开发过程中形式化验证方法与其他保证安全的方法有机结合为区块链安全提供保障。

    ✔ 本体形式化验证工具主要验证功能

    1. 静态检测:该部分编译器本身已完成大部分基本检查,可配合编译器做更多检查。

    2. 动态检测:也是形式化验证工具最有价值的部分。细分为:除0检测、数组越界检测、断言检测、Require 检测、溢出检测、存储注入攻击检测等。

    详见《本体形式化工具检测功能列表》:

    在这里插入图片描述
    在这里插入图片描述
    在这里插入图片描述
    在这里插入图片描述

    操作步骤

    1.1 登录 SmartX

    使用 Chrome 浏览器访问 https://smartx.ont.io/ ,可以点击下方图标使用第三方 GitHub 账号进行登录;

    在这里插入图片描述

    1.2 创建项目

    登录成功后,通过 Create Project 按钮创建项目,目前形式化验证仅支持 Python 版本;

    在这里插入图片描述

    选择项目语言

    1.3 编写智能合约

    通过为您提供的合约模板快速创建并编辑合约;
    在这里插入图片描述

    1.4 编译智能合约
    编写完合约后,选择编译器版本为 version 2.0(目前形式化验证仅支持2.0版本),点击 Compile 进行编译;
    在这里插入图片描述
    1.5 智能合约形式化验证
    编译成功后切换到 Verify 页签,点击 Formal verification 进行形式化验证,验证结束后结果将显示在页面右侧。
    在这里插入图片描述

    展开全文
  • 硅谷Live / 实地探访 / 热点探秘 / 深度探讨CertiK: 智能合约和区块链系统的形式化验证平台区块链时代,智能合约的安全性被无限放大,一个小小的bug就能导致...

    640?wx_fmt=jpeg&wxfrom=5&wx_lazy=1


    硅谷Live / 实地探访 / 热点探秘 / 深度探讨


    640?wx_fmt=png&wxfrom=5&wx_lazy=1&retryload=1

    CertiK: 智能合约和区块链系统的形式化验证平台


    区块链时代,智能合约的安全性被无限放大,一个小小的bug就能导致上亿美元的损失。美链(BEC)近日被爆出安全漏洞,被黑客用以太坊ERC-20智能合约中BatchOverFlow漏洞攻击,引发价格闪崩,当日币价几乎归0。除了美链,据英国和新加坡的研究人员统计,超过34000个智能合约都有可被利用的安全隐患。


    智能合约的安全问题频频亮红灯,黑客简单的一串数字就能套利千万,让人血本无归。想要保证智能合约能够100%的正确,只有形式化验证(Formal Verification)可以确保这些漏洞完全被检测。具体的方式我们用美链来探讨一下。


    美链到底出了什么安全漏洞?


    美链这个安全漏洞其实非常简单!美链智能合约中一个batchTransfer函数, 主要目的是实现BEC token的批量转账: 将固定整数数量(_value) 转账到一批接收账号的数组里 (_receivers). 为了实现这样的批量转账, BEC的开发人员, 首先计算需要转账的总金额, 计算的公式是:


    总金额 (amount) = 需要给每个接收方转账的额度(_value) x 总共需要转账的账户个数 (_cnt)


    然后在确保发送方拥有足够的余额后, 给每个接收方发送转账的额度.


    但是, 出了什么问题呢?


    在计算 amount = _value x _cnt 的过程中, 开发人员并没有考虑到256位整数数据溢出的可能性.


    因此黑客们, 依靠这个漏洞, 成功的余额不足的情况下, 依然从账户中转走了总计2²⁵⁶个BEC Token.


    640?wx_fmt=png

    用形式化验证方法轻松检测漏洞


    事后看来好像美链这个安全漏洞看起来是个愚蠢的错误,但是类似BEC的安全漏洞其实很容易忽略,而智能合约上一个小的程序上的疏忽,就能导致上千万甚至上亿的损失。


    自动化的形式化验证平台很可能能帮助检测和避免类似的错误。来看看Certik的自动化形式化验证平台是如何做到的。


    640?wx_fmt=gif

    CertiK 的验证引擎能够轻易的检测到BEC的溢出错误


    将这段代码提交到CertiK的验证引擎,添加几个标签,Certik的自动化验证引擎能够轻易的检测到BEC的溢出错误。


    640?wx_fmt=png


    Certik的形式化验证引擎能够处理这些标签并且能够根据标签来检查代码实现的正确性。如果美链的智能合约提交之前能够被CertiK做安全检测,那么这上亿的损失就能被避免。


    关于 CertiK


    CertiK 致力于通过全球领先的形式化验证技术重构大家对于智能合约和区块链的信任。Certik 能提供最有竞争力的规模化智能合约验证服务来保证智能合约和区块链系统的安全性。


    CertiK 是来自于耶鲁大学,哥伦比亚大学和硅谷的精英团队,联合创始人邵中是耶鲁大学计算机系系主任/终身教授、中科大名誉院长、清华大学大师讲习团成员,20余年安全领域经验。联合创始人顾荣辉,清华大学本科、耶鲁大学博士、哥伦比亚大学助理教授。


    关于商务合作欢迎联系 info@certik.org




    推荐阅读

    640?wx_fmt=jpeg

    区块链报告 脑机接口报告 

    硅谷人工智能 | 斯坦福校长

    卫哲 | 姚劲波 | 胡海泉 

    垂直种植 | 无人车

    王者荣耀 | 返老还童 



    640?wx_fmt=jpeg



    展开全文
  • 针对这一安全性问题,国内外研究学者一致认为,严格的形式化验证方法能够有效地提高区块链生态系统的安全性。 为此,兼具中国“985工程”与“双一流”称号的电子科技大学信息与软件工程学院杨霞副教...
  • 引言:创立于电子科大科技园军事电子创新加速器的“成都链安科技有限公司”,近日获得分布式资本种子轮投资,是分布式资本唯一资助的中国第一家专门从事区块链形式化验证技术研发的公司。区块链作为大数据时代计算机...
  • 再加上形式化方法的大多数理论还停留在上个世纪,由于程序越来越复杂,导致形式化方法进行验证需要大量人工和时间,以至于现在绝大部分软件开发人员完全没有考虑过这个方法,甚至没有听说过这个名词。 ​ 形式化方法...
  • 为进一步提升本体(Ontology)及其公链上智能合约、区块链应用的安全性、稳定性和功能正确性,Beosin成都链安发布以太坊后全球第二个形式化验证平台VaaS-ONT,...
  • 在去年9月,万向组织的第三届全球区块链峰会上,主办方邀请我做了一个「智能合约形式化验证」的主题演讲,当时引起了大家的关注。 不过那个时候,我们还没有做自动化的工具,要靠人工来做。但人也会犯错,我就想如何...
  • 我与大家分享的是我们团队做的面向以太坊的智能合约形式化验证平台VaaS,这个形式化验证平台是为了提高智能合约安全性的。我们从2016年底开始做这个事情,现在已经做了一些东西出来,在今天的大会与大家分享。 ...
  • 我与大家分享的是我们团队做的面向以太坊的智能合约形式化验证平台VaaS,这个形式化验证平台是为了提高智能合约安全性的。我们从2016年底开始做这个事情,现在已经做了一些东西出来,在今天的大会与大家分享。 我们...
  • 智能合约和形式验证

    2018-03-10 09:37:08
    在之前一篇关于人工智能的文章(http://www.yinwang.org/blog-cn/2017/04/23/ai)里,我指出了“自动编程”的不可能性。今天我想来谈谈一个相关的话题:以太坊式的智能合约的形式验证。有些人声称要实现基于“深度...
  • 任何一个行业,任何一个企业,现在都可以落地AI应用了。只要你有场景,有积累的数据,有算力,能开发出算法,“落地速度会远远超过你的预期”。从上世纪50年代中期人工智能被提出以来,历经了60多...
  • 形式化方法

    2020-10-17 21:17:54
    在计算机科学和软件工程领域,形式化方法是基于数学的特种技术,适合于软件和硬件系统的描述、开发和验证。将形式化方法用于软件和硬件设计,是期望能够像其它工程学科一样,使用适当的数学分析以提高设计的可靠性和...
  • 什么是形式化方法?

    2020-10-25 22:50:29
    形式化方法使软件开发人员可以应用严格的数学符号来说明、开发和验证基于计算机的系统。 这种方法特别在数学、计算机科学、人工智能等领域得到广泛运用。它能精确地揭示各种逻辑规律,制定相应的逻辑规则,使各种...
  • 软件形式化方法概述

    千次阅读 2018-11-10 10:09:55
    软件形式化方法概述
  • 什么是形式化

    千次阅读 2018-08-10 05:22:32
    形式化方法在古代就运用了,而在现代逻辑中又有了进一步的发展和完善。这种方法特别在数学、计算机科学、人工智能等领域得到广泛运用。它能精确地揭示各种逻辑规律,制定相应...
  • AI人工智能专业词汇集

    万次阅读 多人点赞 2017-08-01 16:14:24
    作为最早关注人工智能技术的媒体,机器之心在编译国外技术博客、论文、专家观点等内容上已经积累了超过两年多的经验。期间,从无到有,机器之心的编译团队一直在积累专业词汇。虽然有很多的文章因为专业性我们没能...
  • AI 人工智能学习路线

    千次阅读 2019-02-14 11:45:08
    阶段一、人工智能基础 - 高等数学必知必会 本阶段主要从数据分析、概率论和线性代数及矩阵和凸优化这四大块讲解基础,旨在训练大家逻辑能力,分析能力。拥有良好的数学基础,有利于大家在后续课程的学习中更好的...
  • 2020形式化方法复习笔记

    千次阅读 多人点赞 2020-07-08 22:31:17
    每个形式系统应当包括语法+语义 2.1 语法 The syntax P⋁PP \bigvee PP⋁P :析取 P⋀PP \bigwedge PP⋀P:合取 P→PP \to PP→P:蕴含 2.2 证明系统 The proof system 数学上:Hibert系统,构造性,没有规律可言...
  • ai人工智能的本质和未来Chinese philosophy yin and yang represent how the seemingly opposite poles can complement each other and achieve harmony.中国的阴阳哲学代表着看似相反的两极如何相互补充,实现和谐...
  • 随着人工智能的发展与应用,AI测试逐渐进入到我们的视野,传统的功能测试策略对于算法测试而言,心有余而力不足,难以满足对人工智能 (AI) 的质量保障。 结合在人脸检测、检索算法上的测试探索、实践的过程,本文将...

空空如也

空空如也

1 2 3 4 5 ... 20
收藏数 38,789
精华内容 15,515
关键字:

人工智能形式化验证