SMTLOC:基于多源频谱的SMT求解器缺陷定位

SMT求解器作为重要的基础软件,其存在的缺陷可能会导致依赖于它的软件功能失效,甚至带来安全事故.然而,修复SMT求解器缺陷是一个十分耗时的任务,因为开发者需要花费大量的时间和精力来理解并找到缺陷的根本原因.虽然已有许多软件缺陷定位方面的研究,但尚未有系统的工作研究如何自动定位SMT求解器缺陷.因此,提出一种基于多源频谱的SMT求解器缺陷定位方法SMTLOC.首先,对于给定的SMT求解器缺陷,SMTLOC提出一种枚举算法,用以对触发该缺陷的公式进行变异,从而生成一组不触发缺陷,但与触发缺陷的公式具有相似执行路径的证人公式.然后,SMTLOC根据证人公式的执行路径以及SMT求解器的源码信息,提出一种融合覆盖频谱和历史频谱的文件可疑度计算方法,从而定位可能存在缺陷的文件.为了验证SMTLOC的有效性,收集60个SMT求解器缺陷.实验结果表明,SMTLOC的缺陷定位效果明显优于传统的频谱缺陷定位方法,SMTLOC可以将46.67%的缺陷定位在TOP-5的文件内,定位效果提升了133.33%.

基于SMT求解器的路径敏感程序验证

随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于SMT求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合F-Soft平台和Z3工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果.

使用SAT求解器产生所有极小冲突部件集

产生所有的极小冲突部件集为基于模型诊断中的一个重要步骤.本文将待诊断系统的行为模型及观测分别使用合取范式(CNF)形式的文件描述,从而提出将判定系统组件子集是否为冲突集的问题转化为:首先提取相关组件的CNF模型及观测,然后调用成熟的SAT求解器判定可满足性.随后,通过有效地结合CSISE-tree等方法来产生所有的极小冲突集.为进一步提高效率,给出了充分利用系统输入/输出结构信息的启发式策略.实验结果表明,使用结合SAT求解器及CSISE-tree等方法能够较快产生所有极小冲突集,并且启发式策略使得求解效率进一步提高(平均提高约21%,最高者甚至达到约48%).

一种基于混合SAT求解器的RTL验证方法

为了提高集成电路验证系统的性能,提出一种面向Verilog描述的寄存器传输级(RTL)电路验证方法.该方法将验证问题转化为RTL可满足性问题,并采用基于混合布尔可满足性问题(SAT)的求解器.与传统方法相比,其综合引擎取消了算术电路逻辑的实现,保留了电路特性及其优化信息.因为所需的待验证模型的抽象层次较高,综合系统所花的综合时间较少,尤其是验证引擎不需要处理较低级别的验证细节,由此大大提升了系统性能.不同规模的加法器实验结果表明,基于混合SAT引擎的RTL验证流程较传统流程有明显优势,对复杂电路的验证时间甚至可减少99%.

基于SMT求解器的微处理器指令验证数据约束生成技术

处理器研制过程中需要对指令算术数据路径进行覆盖验证.针对现有模拟验证方法存在的不足,提出了一种基于可满足模理论(satisfiability modulo theory,SMT)的指令约束求解方法:利用可满足模理论求解器将指令级功能验证任务转化成数据约束求解满足问题.在结果操作数约束、操作数间约束、指令内部约束以及浮点操作数约束4个方面分别给出示例,并分别给出了利用SMT求解器进行约束建模的关键过程以及可以用于指令级功能验证的元组数据.为提高求解模型效率,提出了2种解决方法:首先利用时间阈值实现问题求解超时即终止的策略;其次是结合进程管理与线程管理技术,实现了指令功能约束并行求解框架,将串行求解任务分派给可并行执行的多个线程,提高了求解速度.该技术已成功应用于系统级验证中,有效提升了测试覆盖与质量,取得了很好的效益.

CDCLSAT求解器的重启策略分析

CDCL SAT求解器在形式验证等领域应用广泛,但重启策略众多且参数控制复杂,导致通常选择默认参数下的策略,从而降低求解器的效率和易用性.为了提高CDCL SAT求解器的实用性,通过实验分析重启序列、重启间隔、间隔增长系数等因素对实例求解效率的影响,以及求解初期的决策变量数等行为特征数据集与重启策略集之间的关系.实验结果表明,通过改变重启策略可以提高求解效率,所得到的最优解比缺省解的效率可提高6 959%,平均提高411%;重启策略在求解过程中表现出较大的个体差异性和一定的群体差异性;相比重启频率,重启序列对求解效率影响更大.进一步用7种重启策略集合覆盖97%案列的最优重启策略,通过求解初期的特征值变化频率与相应的重启策略关联,为后期选择最优重启策略提供技术支持.

SMT求解器理论组合技术研究

可满足模理论(SMT)求解器是计算机科学中用来判定一阶逻辑公式可满足性的程序,是许多形式化方法的验证引擎。理论求解器实现了SMT基于不同理论背景的求解过程,然而实际问题常以多个理论为背景。因此,本文重点介绍理论组合判定方法,概述SMT求解器的发展现状,并分析了几个主流SMT求解器理论组合判定关键技术。通过对照实验,评估各组合判定方法的优缺点以及目前流行的支持理论组合SMT求解器在工业应用中的性能。

一种基于SAT求解器的组合电路重汇聚现象分析方法

为了研究组合电路重汇聚现象,提出了一种基于SAT求解器的分析方法。通过深度优先搜索算法,确定瞬态脉冲产生节点和输出节点之间的所有路径;建立待检查列表,对表中的元素施加敏化约束条件,并采用SAT求解器求解元素可满足性;最后判断是否存在满足条件的输入向量,使瞬态脉冲通过不同路径在输出节点发生重汇聚。所提方法可以有效地对较大规模组合电路进行分析,采用EPFL和ISCAS’85作为测试集,实验结果表明,ISCAS’85测试集中约有一半节点处产生的瞬态脉冲能够发生重汇聚,这一比例明显高于EPFL测试集,因此不同类型功能电路重汇聚现象的发生率存在较大差异。

基于SMT求解器的BPEL过程数据流错误检测

针对现有检测数据流反模式错误方法常采用枚举策略,存在路径爆炸和异常误报等问题,提出一种基于可满足性模理论(SMT)约束求解器的符号编码去检测所有可行路径中的数据流反模式错误的方法。进行符号编码,包括最常见的3种数据流反模式,根据SMT约束求解器进行数据流反模式错误的识别检测。使用工业界中真实的BPEL过程作为数据集进行实验,实验结果表明,所提方法能够高效无误地检测出BPEL过程中的数据流异常错误。

一种快速低内存消耗的SMT全解求解器

SMT全解求解器为许多研究领域提供辅助,但现有的SMT全解求解器在速度、内存消耗或者支持的求解类型方面存在局限性。首先,提出了求解器的4种新的潜在应用;其次,设计了一种基于二分查找(Binary Search,BS)的新型求解器,可以支持多种求解类型,同时,结合上下文感知(Context Aware,CA)机制来提升求解器的速度,并通过暂停恢复(Suspend Resume,SR)机制降低内存消耗。初步试验表明,BS、BS+CA、BS+SR和所提方法分别能将传统的阻塞子句方法(Blocking Clauses Method,BCM)的求解速度提高了4.6倍、13.4倍、7.3倍以及32.4倍;与BCM相比,提出的方案的内存消耗降低至35.3%。此外,试验结果表明,可以通过并行化进一步提升方案的性能。

SMT求解技术的发展及最新应用研究综述

可满足性模理论(satisfiability modulo theories,SMT)是判定一阶逻辑公式在组合背景理论下的可满足性问题.SMT的背景理论使其能很好地描述实际领域中的各种问题,结合高效的可满足性判定算法,SMT在测试用例自动生成、程序缺陷检测、RTL(register transfer level)验证、程序分析与验证、线性逻辑约束公式优化问题求解等一些最新研究领域中有着突出的优势.首先阐述SMT问题的基础SAT(satisfiability)问题及判定算法;其次对SMT问题、判定算法进行了总结,分析了主流的SMT求解器,包括Z3,Yices2,CVC4等;然后着重介绍了SMT求解技术在典型领域中的实际应用,对目前的研究热点进行了阐述;最后对SMT未来的发展前景进行了展望,目的是试图推动SMT的发展,为此领域的相关人员提供有益的参考.

SMT求解技术简述

SMT问题是在特定理论下判定一阶逻辑公式可满足性问题。它在很多领域,尤其是形式验证、程序分析、软件测试等领域,都有重要的应用。介绍了SMT问题的基本概念、相关定义以及目前的主流理论。近年来出现了很多提高SMT求解效率的技术,着重介绍并分析了这些技术,包括积极类算法、惰性算法及其优化技术等。介绍了目前的主流求解器和它们各自的特点,包括Z3、Yices、CVC3/CVC4等。对SMT求解技术的前景进行了展望,量词的处理、优化问题和解空间大小的计算等尤其值得关注。

基于可满足性问题求解器的星上FPGA永久损伤容错技术研究

现代卫星广泛使用的FPGA在空间高能粒子的影响下,会产生门电路的永久性损伤。而传统的三模冗余等容错方法不但成倍增加了系统硬件开销,还存在因冗余器件耗尽而失效的风险。因此,提出一种利用FPGA自身冗余资源,修复永久性损伤的容错方案。该方案通过建立FPGA内部资源的功能模型,将容错问题转化为数学上的可满足性问题。并且利用经过改进的GSAT算法对该问题求解,可以获得在功能上与损伤前完全相同的电路结构,及其所对应的FPGA配置文件。将该文件重新下载到FPGA中,可以屏蔽损伤带来的影响,从而达到利用FPGA自身冗余资源容错的目的。通过实验和分析可以看出,本文方案具有对损伤修复成功率高、计算量小和需要内存空间少的特点,因此符合星上计算能力和硬件资源十分有限的实际情况。

基于SAT的ARX不可能差分和零相关区分器的自动化搜索

ARX(Addition,Rotation,Xor)算法基于模整数加,异或加和循环移位三种运算,便于软硬件的快速实现.不可能差分分析和零相关分析是攻击ARX的有效方法,攻击的关键是搜索更长轮数、更多数量的不可能差分和零相关区分器.目前很多的搜索方法都没有充分考虑非线性组件的性质,往往不能搜索得到更好、更准确的区分器.本文提出了基于SAT(Satisfiability)的ARX不可能差分和零相关区分器的自动化搜索算法.通过分析ARX算法组件的性质,特别是常规模加和密钥模加这两种非线性运算差分和线性传播的特性,给出了高效简单的SAT约束式.在此基础上,建立SAT模型进行区分器的搜索.作为应用,本文首次给出了Chaskey算法13条4轮不可能差分和1条4轮零相关区分器;首次给出了SPECK32算法10条6轮零相关区分器和SPECK48算法15条6轮零相关区分器;在较短的时间内,给出了HIGHT算法17轮的不可能差分和零相关区分器.与现有结果相比,无论是区分器的条数,还是搜索区分器的时间均有明显的提升.此外,通过重新封装求解器STP的输出接口,建立了自动化的SAT\\SMT分析模型,能够给出ARX算法在特殊输入输出差分和掩码集合下,不可能差分和零相关区分器轮数的上界.

基于约束求解的城市轨道交通CBTC系统事件序列测试用例生成方法

城市轨道交通CBTC系统采用无线通信技术实现车−地连续双向、大容量信息传输。当前,我国正在大力发展自主化CBTC系统,为保障系统软件安全性,对系统进行信息交互测试是极为必要的。针对现有研究对CBTC系统的信息交互顺序测试不充分而引发的系统软件安全性问题,提出一种基于约束求解的事件序列测试用例生成方法。首先,根据系统蕴含的信息交互事件及其约束关系,提出一种基于事件索引的约束处理方法,实现顺序约束条件的1阶逻辑表示,继而采用约束求解器实现测试用例生成过程中的合法性校验及可扩展性校验。然后,基于贪心算法框架,提出事件序列测试用例的初始化、扩展与校验策略,实现事件序列测试用例集的高效精简生成。最后,以列车进站场景下的CBTC系统移动授权生成功能为研究对象,辨识各子系统间的信息交互事件、交互顺序及其约束,采用所提方法构建CBTC系统事件序列测试用例集。结果表明,所提方法可高效精简生成满足约束条件与覆盖准则的事件序列测试用例集,提高了测试的有效性与完备性。与穷举法相比,所提方法的测试用例集规模精简幅度可达到72.5%。与随机法相比,在生成相同规模的测试用例集时,所提方法的t-维事件序列覆盖率显著高于随机法,可在保证事件序列检错效力的前提下提高测试效率,从而为高效开展CBTC系统的信息交互顺序测试提供了理论依据。

一种计算ARX密码差分—线性偏差的新方法

ARX密码由模加、循环移位和异或这3种基本运算组成。目前ARX密码差分—线性区分器偏差的计算大多采用统计分析的方法。在2022年美密会上,NIU等给出了一种计算ARX密码差分—线性区分器相关度的非统计分析的方法,并给出了SPECK32/64的10轮差分—线性区分器。基于BLONDEAU等和BAR-ON等的方法,给出了差分—线性特征的定义,并首次提出了用差分—线性特征计算差分—线性区分器偏差的方法。同时,提出了一种基于布尔可满足性问题(SAT)自动化技术搜索差分—线性特征的方法,给出了计算ARX密码差分—线性区分器偏差的非统计分析的新方法。作为应用,对NIU等给出的SPECK32/64的10轮差分—线性区分器偏差进行计算,得到的理论值为2-15.00,非常接近统计分析的实验值2-14.90,且优于NIU等给出的理论值2-16.23。同时,首次给出了SIMON32/64的9轮差分—线性区分器偏差的理论值2-8.41,接近统计分析得到的实验值2-7.12。实验结果说明了这种方法的有效性。

可满足性模理论综述

可满足性模理论(SMT)是指判定一阶逻辑公式在特定背景理论下的可满足性问题。基于一阶逻辑的SMT相比SAT描述能力更强、抽象能力更高,能处理更加复杂的问题。SMT求解器在各个领域都有应用,已经成为重要的形式化验证引擎。目前,SMT已被广泛应用在人工智能、硬件RTL验证、自动化推理和软件工程等领域。根据近些年SMT的发展,首先阐述SMT基本知识和常见的背景理论;然后分析总结Eager方法、Lazy方法和DPLL(T)方法的实现流程,并进一步介绍主流求解器Z3、CVC5和MathSAT5的实现过程;接着介绍SMT的扩展问题#SMT、SMT应用在深度神经网络的SMTlayer方法和量子SMT求解器;最后对SMT的发展进行展望,并讨论其面临的挑战。

基于SAT的路径规划系统的设计

本文主要介绍了基于SAT路径规划算法以及路径规划系统的设计方案。通过移动机器人抓取积木为例,介绍了基于SAT路径规划算法包括的规划问题的命题表示方法以及如何使用SAT求解器对规划命题进行求解。该系统较传统的路径规划系统而言,路径规划解提取速度较快,无需传感器的反复检测初始状态及目标状态,规划效率较高。

基于MiniSAT的命题极小模型计算方法

计算命题公式的极小模型在人工智能推理系统中是一项必不可少的任务.然而,即使是正CNF(conjunctive normal form)公式,其极小模型的计算和验证都不是易处理的.当前,计算CNF公式极小模型的主要方法之一是将其转换为析取逻辑程序后用回答集程序(answer set programming,ASP)求解器计算其稳定模型回答集.针对计算CNF公式的极小模型的问题,提出一种基于可满足性问题(satisfiability problem,SAT)求解器的计算极小模型的方法MMSAT;然后结合最近基于极小归约的极小模型验证算法CheckMinMR,提出了基于极小模型分解的计算极小模型方法MRSAT;最后对随机生成的大量的3CNF公式和SAT国际竞赛上的部分工业基准测试用例进行测试.实验结果表明:MMSAT和MRSAT对随机3CNF公式和SAT工业测试用例都是有效的,且计算极小模型的速度都明显快于最新版的clingo,并且在SAT工业实例上发现了clingo有计算出错的情况,而MMSAT和MRSAT则更稳定.

基于频次的SAT问题学习子句混合评估算法

为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句。传统的评估方式是基于学习子句的长度,保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息。以Syrup求解器(GLUCOSE4.1并行版本)为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多。