安全C语言验证器中形状系统的形状检查方法
|
摘要
在一个基于霍尔逻辑和形状图逻辑的C语言自动验证器中,设计并实现了对形状图中所含易变数据结构的形状检查方法.本工作在验证器的形状系统中实现了显式形状检查与隐式形状检查,并通过引入不同的形状级别,使验证器能够根据不同的严格程度及时发现程序中不符合形状定义的易变数据结构,避免对形状图逻辑的相关演算造成影响.此外,为分解易变数据结构中不同指针域带来的复杂性,形状检查方法引入了三阶段处理框架:形状分割、形状分析及形状推断,分别实现形状图的预处理,针对指针指向与节点类型等方面进行分析,以及根据相关规则推断易变数据结构的形状级别.
In an automatic verifier for C programs based on Hoare logic and Shape Graph Logic,we have designed and implemented an approach for checking the shapes of mutable data structures in shape graphs. In particular,we have implemented both explicit shape checking and implicit shape checking in the shape system of the verifier. By introducing different shape levels,the verifier is capable of identifying mutable data structures which do not conform to the shape definitions in time with different levels of rigor,so that the computation of shape graph logic will not be affected. Furthermore,in order to reduce the complexity caused by different pointer field types of mutable data structures,the proposed approach utilizes a three-phase processing framework: shape splitting,shape analysis and shape deduction. The three phases perform the following three tasks,respectively: preprocessing graphs,analyzing " points-to" information of pointers and the type of nodes,and deducing the shape levels for mutable data structures according to related rules.
In an automatic verifier for C programs based on Hoare logic and Shape Graph Logic,we have designed and implemented an approach for checking the shapes of mutable data structures in shape graphs. In particular,we have implemented both explicit shape checking and implicit shape checking in the shape system of the verifier. By introducing different shape levels,the verifier is capable of identifying mutable data structures which do not conform to the shape definitions in time with different levels of rigor,so that the computation of shape graph logic will not be affected. Furthermore,in order to reduce the complexity caused by different pointer field types of mutable data structures,the proposed approach utilizes a three-phase processing framework: shape splitting,shape analysis and shape deduction. The three phases perform the following three tasks,respectively: preprocessing graphs,analyzing " points-to" information of pointers and the type of nodes,and deducing the shape levels for mutable data structures according to related rules.
引文
[1] Schanda F L F,Matthews S R. SPARK 2014:a language for safety and security[C]. Iet International Conference on System Safety and Cyber Security,IET,2015:1-5.
[2] Nanevski A,Morrisett G,Shinnar A,et al. Ynot:dependent types for imperative programs[C]. In Proceedings of the 13th ACMSIGPLAN International Conference on Functional Programming(ICFP'08),NewYork,USA,ACM,2008:229-240.
[3] Barnett M,Leino K R M,Schulte W. The spec#programming system:an overview[C]. In Communication and Social Science Information Service(CASSIS'04),Berlin,Heidelberg,Springer,2004:49-69.
[4] Flanagan C,Leino K R M,Lillibridge M,et al. Extend static checking for Java[C]. In Proceedings of the Conference on Programming Language Design and Implementation(PLDI'02),NewYork,USA,ACM,2002:234-245.
[5] Hoare C A R. An axiomatic basis for computer programing[C].Communications of ACM(CACM),NewYork,USA,ACM,1969:576-580.
[6] Li Zhao-peng,Zhang Yu,Chen Yi-yun. A shape graph logic and shape system[J]. Journal of Computer Science and Technology,2013,28(6):1063-1084.
[7] Zhang Yu,Chen Yi-yun,Li Zhao-peng. Theorem proving for a theory of shape graphs[J]. Chinese Journal of Computers,2015,38(26):1-23.
[8] Song Yan-hui,Li Zhao-peng,Chen Yi-yun. Automatic inference of pre and post shape graphs for pointer-type recursive functions[J].Journal of Chinese Computer Systems,2014,35(4):759-765.
[9] Li Yun-long,Luo Qi-ming,Chen Yi-yun. Automatic interference of loop invariant shape graphs for binary tree program[J]. Journal of Chinese Computer Systems,2017,38(5):913-918.
[10] Moura L D,Bjrner N. Z3:an efficient SMT solver[M]. Tools and Algorithms for the Construction and Analysis of Systems,Berlin,Heidelberg,Springer,2008:337-340.
[11] Zhang Zhi-tian,Li Zhao-peng,Chen Yi-yun,et al. An automatic program verifier for pointerC:design and implementation[J]. Journal of Computer Research and Development,2013,50(5):1044-1054.
[12] Qiu X,Garg P,tefǎnescu A,et al. Natural proofs for structure,data,and separation[C]. In Proceedings of the 34th ACMSIGPLAN Conference on Programming Language Design and Implementation(PLDI'13),NewYork,USA,ACM,2013:231-242.
[13] Reynolds J C. Separation logic:a logic for shared mutable data structures[C]. IEEE Symposium on Logic in Computer Science,IEEE Computer Society,2002:55-74.
[14] Lammich P. Refinement based verification of imperative data structures[C]. In Proceedings of the 5th ACMSIGPLAN Conference on Certified Programs and Proofs(CPP 2016),NewYork,USA,ACM,2016:27-36.
[15] Roe K,Smith S F,Roe K,et al. Using the coq theorem prover to verify complex data structure invariants[C]. In Proceedings of the15th ACM-IEEE International Conference on Formal Methods and Models for System Design(MEMOCODE'17),NewYork,USA,ACM,2017:118-121.
[7]张昱,陈意云,李兆鹏.形状图理论的定理证明[J].计算机学报,2015,38(26):1-23.
[8]宋艳辉,李兆鹏,陈意云.指针类型递归函数前后形状图的自动推断[J].小型微型计算机系统,2014,35(4):759-765.
[9]李云龙,罗奇鸣,陈意云.二叉树程序循环不变形状图的自动推断[J].小型微型计算机系统,2017,38(5):913-918.
[11]张志天,李兆鹏,陈意云,等.一个程序验证器的设计和实现[J].计算机研究与发展,2013,50(5):1044-1054.
1全称为Safe C Specification Language,是课题组在ACSL:frama-c. com/acsl. html基础上扩展得到的安全C语言规范语言
[2] Nanevski A,Morrisett G,Shinnar A,et al. Ynot:dependent types for imperative programs[C]. In Proceedings of the 13th ACMSIGPLAN International Conference on Functional Programming(ICFP'08),NewYork,USA,ACM,2008:229-240.
[3] Barnett M,Leino K R M,Schulte W. The spec#programming system:an overview[C]. In Communication and Social Science Information Service(CASSIS'04),Berlin,Heidelberg,Springer,2004:49-69.
[4] Flanagan C,Leino K R M,Lillibridge M,et al. Extend static checking for Java[C]. In Proceedings of the Conference on Programming Language Design and Implementation(PLDI'02),NewYork,USA,ACM,2002:234-245.
[5] Hoare C A R. An axiomatic basis for computer programing[C].Communications of ACM(CACM),NewYork,USA,ACM,1969:576-580.
[6] Li Zhao-peng,Zhang Yu,Chen Yi-yun. A shape graph logic and shape system[J]. Journal of Computer Science and Technology,2013,28(6):1063-1084.
[7] Zhang Yu,Chen Yi-yun,Li Zhao-peng. Theorem proving for a theory of shape graphs[J]. Chinese Journal of Computers,2015,38(26):1-23.
[8] Song Yan-hui,Li Zhao-peng,Chen Yi-yun. Automatic inference of pre and post shape graphs for pointer-type recursive functions[J].Journal of Chinese Computer Systems,2014,35(4):759-765.
[9] Li Yun-long,Luo Qi-ming,Chen Yi-yun. Automatic interference of loop invariant shape graphs for binary tree program[J]. Journal of Chinese Computer Systems,2017,38(5):913-918.
[10] Moura L D,Bjrner N. Z3:an efficient SMT solver[M]. Tools and Algorithms for the Construction and Analysis of Systems,Berlin,Heidelberg,Springer,2008:337-340.
[11] Zhang Zhi-tian,Li Zhao-peng,Chen Yi-yun,et al. An automatic program verifier for pointerC:design and implementation[J]. Journal of Computer Research and Development,2013,50(5):1044-1054.
[12] Qiu X,Garg P,tefǎnescu A,et al. Natural proofs for structure,data,and separation[C]. In Proceedings of the 34th ACMSIGPLAN Conference on Programming Language Design and Implementation(PLDI'13),NewYork,USA,ACM,2013:231-242.
[13] Reynolds J C. Separation logic:a logic for shared mutable data structures[C]. IEEE Symposium on Logic in Computer Science,IEEE Computer Society,2002:55-74.
[14] Lammich P. Refinement based verification of imperative data structures[C]. In Proceedings of the 5th ACMSIGPLAN Conference on Certified Programs and Proofs(CPP 2016),NewYork,USA,ACM,2016:27-36.
[15] Roe K,Smith S F,Roe K,et al. Using the coq theorem prover to verify complex data structure invariants[C]. In Proceedings of the15th ACM-IEEE International Conference on Formal Methods and Models for System Design(MEMOCODE'17),NewYork,USA,ACM,2017:118-121.
[7]张昱,陈意云,李兆鹏.形状图理论的定理证明[J].计算机学报,2015,38(26):1-23.
[8]宋艳辉,李兆鹏,陈意云.指针类型递归函数前后形状图的自动推断[J].小型微型计算机系统,2014,35(4):759-765.
[9]李云龙,罗奇鸣,陈意云.二叉树程序循环不变形状图的自动推断[J].小型微型计算机系统,2017,38(5):913-918.
[11]张志天,李兆鹏,陈意云,等.一个程序验证器的设计和实现[J].计算机研究与发展,2013,50(5):1044-1054.
1全称为Safe C Specification Language,是课题组在ACSL:frama-c. com/acsl. html基础上扩展得到的安全C语言规范语言