返回主页


为了提高软件的安全性和可靠性,本项目研究恶意程序的主动防御和检测理论与方法。恶意程序防御和检测从广义上来说是不可判定的。因此,本项目首先要建立恶意程序防御与检测的可判定子集和具有高效防御策略和检测算法的可判定子集。然后,研究基于语义的恶意程序主动防御理论与方法,以及基于语义的恶意代码主动检测理论与方法。最后,在理论研究的基础上,开发恶意程序主动防御与检测支撑工具集。

本项目按照计划完成了研究内容,达到了预期目标,取得了一些国际领先的研究成果,包括:图灵奖获得者Clarke等人提出的抽象模型精化CEGAR方法的模型精化算法复杂度是指数级(O(2n))的,反例路径检测算法的复杂度是多项式级(O(p(n)))的, 我们提出了二次多项式(O(n2))抽象模型精化算法以及线性复杂度(O(n))的虚假反例路径检测算法;针对命题投影时序逻辑PPTL不能描述内存演化的相关性质的不足,结合分离逻辑SL与命题投影时序逻辑PPTL,提出了二维(时间和空间)逻辑PPTL^SL;针对Craig插值(Interpolation)的不足,提出了错误插值(Error Interpolation)和安全插值(Safety Interpolation),缩减了模型检测中的状态空间,提高了检测的规模; 针对随机生成测试用例导致的大量无效测试的问题和非RFC制导的差异测试中无评价标准的问题,提出了RFC制导的、基于动态符号执行的浏览器证书生成方法RFCcert,检测出了谷歌,微软等8大著名浏览器未曾发现的35个安全漏洞; 针对从程序中提取模型的困难,提出了一种基于MSVL的代码级的运行时验证方法,能够验证现有工具无法验证的完全正则时序性质;针对国外学者对区间时序逻辑不可判定的错误结论,证明了基于区间的时序逻辑在有穷和无穷区间都是可判定的,特别是,2016年进一步提出了canonical范型,得到了更高效的判定算法。开发了建模、仿真和验证平台MSV。 在ACM Transactions on Software Engineering and Methodology,IEEE Transactions on Software Engineering,IEEE Transactions on Knowledge & Data Engineering, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on Reliability,Theoretical Computer Science,Formal Aspects of Computing 等著名国际期刊,以及ASE、ICSE、IJCAI 等著名国际会议发表论文56篇,其中SCI检索26篇,EI检索30篇;获教育部自然科学一等奖(2016);获陕西省安全攸关智能软件创新团队(2018); 培养“长江学者”特聘教授1名,博士9名、硕士31名;授权专利15项(含美国专利1项);组织国内会议5次、合作组织国际会议7次、邀请国内外知名学者讲学31人次、参加国际会议32次。