基于GJB5369—2005的分级报告策略

赖策+刘茜

摘要：航天型号C语言安全子集是确保程序安全、正确运行的编程设计规范，它由语法、语义等级别的安全使用规则构成。支持C安全子集是减少航天型号、军工型号应用在执行环境中的安全隐患的重要途径之一。本研究将对C语言安全子集规范进行细化分类，依据其危险程度形成不同安全等级；为C语言安全子集形成一整套规则化处理流程，包括对不同安全等级的规范建立一套规范化识别、分析以及决策处理流程。

关键词：安全子集；分级流程；危险程度

中图分类号：TP314 文献标识码：A 文章编号：1009-3044（2017）26-0086-01

1 C语言安全子集等级划分技术

在安全子集中，编程规则通常包括推荐和强制两种类型。推荐类为参照执行的准则，而强制类型为必须遵循的准则，它们对应了不同级别的安全隐患；对于同种准则，例如强制类型准则，编译器语法、语义对其各个细则的识别能力以及识别位置也不尽相同。不同准则需要不同的识别、分析以及决策。为实现高覆盖的安全检测，本项目需要对子集规则进行深入分析和研究，将规则细化分类，对不同安全等级的规则建立规范的识别、分析以及决策处理流程。

2 关键技术

面向C語言安全子集的编译技术面临的最大挑战是：覆盖率与编译效率可控性之间如何权衡？本技术将对C语言安全子集准则进行细化分类，形成不同安全等级。具体地，本研究将基于研发效率、覆盖率进行分级考察。从相似性上按识别、分析和处理流程是否相似来分析。依据分析结果对C语言安全子集提出一套规范化处理流程，包括对不同安全等级的细则建立规范化识别、规范化分析以及决策处理流程。

3 创新点

在航天型号软件C语言安全子集中，编程规则区分为不同种类，它们对应了不同级别的安全隐患；对于同类准则，编译器语法、语义对其各个细则的识别能力以及识别位置也不尽相同。不同准则需要不同的识别、分析以及决策。本研究将对子集规则开展深入分析和研究，将规则细化分类，根据不同规则所具有的危险性将其划分为不同安全等级，为它们建立规范的 识别、分析以及决策处理流程。

4 初步结果

经过研究和分析航天型号软件C语言安全子集所有规则后，发现其中要实现的案例大部分都是属于编译前端的内容，于是我们选择了Gcc4.9.3编译器作为我们的基准编译器，深入研究Gcc的调用流程如图1所示，并对GJB5369-2005中的案例进行手工编码实现，通过对36个案例进行了成功的编码实现，并分析案例与案例之间的异同，现初步将航天型号软件C语现言安全子集分为3个错误级别，3个错误类型。

错误级别：

1） fatal：极高危险度，如内存泄漏，引起不可预料后果等错误。

2） error：高危险度，如过程名被重用，禁止实参和形参类型不一致等错误。

3） Waring：中低危险度，如谨慎使用#pragma，避免使用setjmp/longjmp等错误。

错误类型：

1） 软工管理：涉及函数，参数，宏相关，重定义相关错误。

2） 数值相关：涉及赋值，内存相关错误。

3） 语言规范：涉及词法，语法规范相关错误。

参考文献：

[1] Milner R，Weyhrauch R. Proving compiler correctness in a mechanized logic[C]//Machine Intelligence 7：proc of the 7th annual Machine Intelligence Workshio，1972：51-72.

[2] The Comp Certverifified C compiler.pdf[EB/OL].

http：//research.microsoft.com/en-us/um/redmond/events/ss2011/slides/friday/xavier_leroy.pdf.

[3] Pnueli A，Siegel M， Singerman E.Translation validation[C].Proc.of the TACAS，1998：151-166.

[4] Ngo V C，Talpin J，Gautier T，et al，Besnard L.Formal verification of synchronous data-flow program transformations toward certified compilers[J].Frontiers of Computer Science，2013：598-616.

[5] Bringing Extensibility to Verified Compilers[J].Acm Sigplan Notices，2010，45（6）：111-121.

[6] 航天软件型号软件C语言安全子集[Z].国防科学技术工业委员会.

[7] 申瑞芬.高可信安全编译器的设计与实现[D].长沙：国防科技大学，2007.

[8] 皮庆基.一种语言静态代码检测工具[D].北京：北京邮电大学，2013.

[9] 王蕾.一个C语言安全子集的可信编译器[J].计算机科学，2013，40（9）：30-34.endprint