汇编级顺序语句块的自动形式化规约及其验证

doi:10.19678/j.issn.1000-3428.0053152

计算机工程 ›› 2019, Vol. 45 ›› Issue (10): 64-69,77. doi: 10.19678/j.issn.1000-3428.0053152

汇编级顺序语句块的自动形式化规约及其验证

祁龙云¹, 吕小亮¹, 路红², 黄皓²

1. 南京南瑞信息通信科技有限公司, 南京 210003;
2. 南京大学计算机软件新技术国家重点实验室, 南京 210023

收稿日期:2018-11-16 修回日期:2019-01-21 出版日期:2019-10-15 发布日期:2019-01-29
作者简介:祁龙云(1979-),男,工程师,主研方向为形式化验证、可信计算;吕小亮,工程师;路红,讲师、博士研究生;黄皓,教授、博士。
基金资助:
国家电网公司2018年总部科技项目"可信嵌入式操作系统关键技术研究"（SGJSNT00FZJS1800129）。

Automatic Formal Specification and Its Verification of Assembly-Level Sequential Statement Blocks

QI Longyun¹, Lü Xiaoliang¹, LU Hong², HUANG Hao²

1. NARI Information and Communication Technology Co., Ltd., Nanjing 210003, China;
2. State Key Laboratory for Novel Software Technology at Nanjing University, Nanjing 210023, China

Received:2018-11-16 Revised:2019-01-21 Online:2019-10-15 Published:2019-01-29

摘要/Abstract

摘要： 软件的形式化验证是保障软件可证明性、可靠性和安全性的重要手段，但传统形式化验证脚本的生成过程复杂且需要形式化验证专家的大量手工验证。为提高证明效率，构建一种自动证明模型，并在此基础上提出语义自动规约算法以及对所规约的语义自动生成证明脚本的算法。利用C++和Python并通过交互式定理证明器Isabelle 2017在基准数据中随机选择10个程序进行测试，结果表明，与完全人工操作相比，该算法具有较高的验证效率，可实现顺序语句块的自动化规约与验证。

关键词: 自动形式化规约, 自动化验证, 定理证明器, 交互式定理, 形式化验证

Abstract: Formal verification of software is an important means to guarantee the provability,reliability and security of software, but the generation process of traditional formal verification script is complex and requires a lot of manual verification of formal verification experts.In order to improve the efficiency of proof,this paper constructs an automatic proof model,and on this basis,proposes a semantic automatic specification algorithm and its automatic generation algorithm for generating proof scripts.Using C++ and Python and randomly selecting 10 programs in the benchmark data by the interactive theorem prover Isabelle 2017 to run the test,results show that compared with the fully manual operation,the algorithm has higher verification efficiency,and can implement automatic specification and verification of sequential statement.

Key words: automatic formal specification, automatic verification, theorem prover, interactive theorem, formal verification

中图分类号:

TP391

祁龙云, 吕小亮, 路红, 黄皓. 汇编级顺序语句块的自动形式化规约及其验证[J]. 计算机工程, 2019, 45(10): 64-69,77.

QI Longyun, Lü Xiaoliang, LU Hong, HUANG Hao. Automatic Formal Specification and Its Verification of Assembly-Level Sequential Statement Blocks[J]. Computer Engineering, 2019, 45(10): 64-69,77.

http://www.ecice06.com/CN/Y2019/V45/I10/64

图/表 2

参考文献 28

[1]	梅妍.结构化测试在MIS软件性能验证中的应用研究[D].上海:复旦大学,2011.
[2]	郑红军,张乃孝.软件开发中的形式化方法[J].计算机科学,1997,24(6):90-96.
[3]	王戟,李宣东.形式化方法与工具专刊前言[J].软件学报,2011,22(6):1121-1122.
[4]	傅育熙,李国强,田聪.形式化方法的理论基础专题前言[J].软件学报,2018,29(6):1049-1050.
[5]	王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
[6]	卜磊,解定宝.混成系统形式化验证[J].软件学报,2014,25(2):219-233.
[7]	游珍,薛锦云.基于Isabelle定理证明器算法程序的形式化验证[J].计算机工程与科学,2009,31(10):85-89.
[8]	谯婷婷,王乐,王芳,等.基于Coq的软件安全性验证[J].计算机应用,2012,32(2):96-100.
[9]	张杰,王少超,关永.基于形式化方法的有限域乘法器的建模与验证[J].电子技术应用,2018(1):109-113.
[10]	KLEIN G,ELPHINSTONE K,HEISER G,et al.SeL4:formal verification of an OS kernel[C]//Proceedings of the 22nd ACM SIGOPS Symposium on Operating Systems Principles.New York,USA:ACM Press,2009:207-220.
[11]	BECKERT B,MOSKAL M.Deductive verification of system software in the verisoft XT project[J].KI-Künstliche Intelligenz,2010,24(1):57-61.
[12]	DAUM M,DORRENBACHER J,BOGAN S.Model stack for the pervasive verification of a microkernel-based operating system[C]//Proceedings of the 5th IEEE International Verification Workshop.Washington D.C.,USA:IEEE Press,2008,372:56-70.
[13]	GU Liang,VABNBERG A,FORD B,et al.CertiKOS:a certified kernel for secure cloud computing[C]//Proceedings of the 2nd Asia-Pacific Workshop on Systems.New York,USA:ACM Press,2011:3.
[14]	XU Fengwei,FU Ming,FENG Xinyu,et al.A practical verification framework for preemptive OS kernels[C]// Proceedings of International Conference on Computer Aided Verification.Berlin,Germany:Springer,2016:59-79.
[15]	陈丽蓉,李允,罗蕾.嵌入式操作系统的形式化验证研究[J].计算机科学,2015,42(8):203-214.
[16]	陈钢,于林宇,裘宗燕,等.基于逻辑的形式化验证方法:进展及应用[J].北京大学学报(自然科学版),2016,52(2):363-373.
[17]	张恒若,付明.基于Z3的Coq自动证明策略的设计和实现[J].软件学报,2017,28(4):819-826.
[18]	LEINO K R M.Dafny:an automatic program verifier for functional correctness[C]//Proceedings of International Conference on Logic for Programming Artificial Intelligence and Reasoning.Berlin,Germany:Springer,2010:348-370.
[19]	BOND B,HAWBLITZEL C,KAPRITSOS M,et al.Vale:verifying high-performance cryptographic assembly code[C]//Proceedings of IEEE USENIX Security Sympo-sium.Washington D.C.,USA:IEEE Press,2017:158-169.
[20]	何炎祥,吴伟,陈勇,等.基于SMT求解器的路径敏感程序验证[J].软件学报,2012,23(10):2655-2664.
[21]	胡凯.智能合约的形式化验证方法[J].信息安全研究,2016,12(2):1080-1089.
[22]	NELSON L,SIGURBLARNARSON H,ZHANG Kaiyuan,et al.Hyperkernel:push-Button verification of an OS kernel[C]//Proceedings of the 26th Symposium on Operating Systems Principles.New York,USA:ACM Press,2017:252-269.
[23]	郝耀辉,郭渊博,罗婷,等.基于Hoare逻辑的密码软件形式化验证系统[J].计算机工程,2012,38(3):121-123.
[24]	钱振江,黄皓,宋方敏.操作系统汇编级形式化设计和验证方法[J].软件学报,2016,27(12):3143-3157.
[25]	BEYER D.Competition on software verification (SV-COMP)[EB/OL].[2018-10-16].https://sv-comp.sosy-lab.org/2018/.
[26]	LI Jiaying,SUN Jun,LI Li,et al.Automatic loop-invariant generation and refinement through selective sampling[C]//Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering.Washington D.C.,USA:IEEE Press,2017:782-792.
[27]	BOUNOV D,DEROSSI A,MENARINI M,et al.Inferring loop invariants through gamification[C]//Proceedings of the 2018 Conference on Human Factors in Computing Systems.Montreal,Canada:[s.n.],2018:231.
[28]	XIE Xiaofei,CHEN Bihuan,ZOU Liang,et al.Automatic loop summarization via path dependency analysis[J].IEEE Transactions on Software Engineering,2018(99):1.

选择文件类型/文献管理软件名称

选择包含的内容

汇编级顺序语句块的自动形式化规约及其验证

Automatic Formal Specification and Its Verification of Assembly-Level Sequential Statement Blocks

RichHTML

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

图/表 2

参考文献 28

相关文章 15

编辑推荐

Metrics

本文评价

[1]	夏锐, 钱振江, 刘苇. 一种基于Isabelle/HOL的安全通信协议验证方法[J]. 计算机工程, 2021, 47(1): 146-153.
[2]	欧阳恒一, 熊焰, 黄文超. 一种代币智能合约的形式化建模与验证方法[J]. 计算机工程, 2020, 46(10): 41-45,51.
[3]	钟建, 徐扬, 陈树伟, 何星星. 一阶逻辑中基于稳定度的项评估方法[J]. 计算机工程, 2019, 45(11): 183-190,197.
[4]	林荣峰, 施健, 朱晏庆, 沈怡颹, 周宇. 基于STP方法的SCADE模型形式化验证框架[J]. 计算机工程, 2019, 45(10): 70-77.
[5]	李堃,张雪松. STP安全通信协议设计与形式化验证[J]. 计算机工程, 2018, 44(12): 120-128.
[6]	李青,朱晓冉,郭建. AUTOSAR OS存储保护机制的形式化验证框架[J]. 计算机工程, 2017, 43(1): 79-85.
[7]	杨世瀚,吴尽昭,丁广泓,秦董洪. 模拟与混合信号电路的形式化验证[J]. 计算机工程, 2016, 42(8): 34-38,45.
[8]	彭展,梁根,周炳. 电信服务系统特征交互的Z规格及验证[J]. 计算机工程, 2016, 42(8): 19-23.
[9]	罗尔聪,郭宇. μC / OS-Ⅲ任务调度器在Coq 中的验证[J]. 计算机工程, 2015, 41(3): 53-58.
[10]	杨龙婴,郭宇. 针对NAND闪存硬件的形式化建模[J]. 计算机工程, 2015, 41(11): 94-99.
[11]	纪明宇, 王海涛, 陈志远. 基于综合性能的Markov过程验证与分析[J]. 计算机工程, 2013, 39(5): 318-321.
[12]	陈振庆. 基于时序描述逻辑的UML顺序图形式化方法[J]. 计算机工程, 2013, 39(3): 36-40.
[13]	徐亮，谭煌. BLP改进模型的形式化描述及自动化验证[J]. 计算机工程, 2013, 39(12): 130-135.
[14]	郝耀辉, 郭渊博, 罗婷, 燕菊维. 基于Hoare逻辑的密码软件形式化验证系统[J]. 计算机工程, 2012, 38(3): 121-123.
[15]	钱振江, 刘苇, 黄皓. 操作系统形式化设计与验证综述[J]. 计算机工程, 2012, 38(11): 234-238.

模态框（Modal）标题

选择文件类型/文献管理软件名称

选择包含的内容

汇编级顺序语句块的自动形式化规约及其验证

Automatic Formal Specification and Its Verification of Assembly-Level Sequential Statement Blocks

RichHTML

PDF

可视化

被引次数

摘要/Abstract

引用本文

使用本文

图/表 2

参考文献 28

相关文章 15

编辑推荐

Metrics

本文评价