唐成华，侯梦迪，高庆泽，强保华2，

1(桂林电子科技大学 广西可信软件重点实验室，广西 桂林 541004)

2(广西云计算与大数据协同创新中心，广西 桂林 541004)

3(广西密码学与信息安全重点实验室，广西 桂林 541004)

1 引 言

恶意软件是网络和信息安全的主要威胁，对网络信息技术应用带来极大的困扰.随着代码混淆技术的发展和使用，恶意软件的行为变得更加复杂，增加了恶意软件被检测的难度.软件行为在代码混淆前后具有一致性，对恶意软件进行语义描述，采用形式化方法表示软件行为可以更直观地展现出软件代码的目的，有利于提高恶意软件的检测准确率.

由于逻辑语言在表达能力、灵活性和语义完整性上具有先天优势，将描述逻辑引入软件体系、状态特征等方面已是研究热点.基于传统时序逻辑的语义描述方法多是具有状态基结构属性，难以描述语义动态效应或指针程序的语义性质，而基于霍尔逻辑的扩展系统虽然推理性好，但仍属于一阶逻辑的范畴，表达能力依旧欠缺.因此，需要进行高阶逻辑的扩展，以达到语义过程描述的动态效应过程.Delbianco等[1]基于高阶分离逻辑建立了一种对象线性化推理方法，能接受线性化点的动态特征及其修改，实现分离逻辑中指针更新到线性化点时间位置修改的动态模拟.Mario等[2]基于动态逻辑引入某种时序的模态算子，属于动态规约和行为推理的范畴，但通常不具备描述静态结构属性的能力.而采用……