基于GJB5369—2005的分級報告策略

賴策+劉茜

摘要：航天型號C語言安全子集是確保程序安全、正確運行的編程設(shè)計規(guī)范，它由語法、語義等級別的安全使用規(guī)則構(gòu)成。支持C安全子集是減少航天型號、軍工型號應(yīng)用在執(zhí)行環(huán)境中的安全隱患的重要途徑之一。本研究將對C語言安全子集規(guī)范進行細化分類，依據(jù)其危險程度形成不同安全等級；為C語言安全子集形成一整套規(guī)則化處理流程，包括對不同安全等級的規(guī)范建立一套規(guī)范化識別、分析以及決策處理流程。

關(guān)鍵詞：安全子集；分級流程；危險程度

中圖分類號：TP314 文獻標識碼：A 文章編號：1009-3044（2017）26-0086-01

1 C語言安全子集等級劃分技術(shù)

在安全子集中，編程規(guī)則通常包括推薦和強制兩種類型。推薦類為參照執(zhí)行的準則，而強制類型為必須遵循的準則，它們對應(yīng)了不同級別的安全隱患；對于同種準則，例如強制類型準則，編譯器語法、語義對其各個細則的識別能力以及識別位置也不盡相同。不同準則需要不同的識別、分析以及決策。為實現(xiàn)高覆蓋的安全檢測，本項目需要對子集規(guī)則進行深入分析和研究，將規(guī)則細化分類，對不同安全等級的規(guī)則建立規(guī)范的識別、分析以及決策處理流程。

2 關(guān)鍵技術(shù)

面向C語言安全子集的編譯技術(shù)面臨的最大挑戰(zhàn)是：覆蓋率與編譯效率可控性之間如何權(quán)衡？本技術(shù)將對C語言安全子集準則進行細化分類，形成不同安全等級。具體地，本研究將基于研發(fā)效率、覆蓋率進行分級考察。從相似性上按識別、分析和處理流程是否相似來分析。依據(jù)分析結(jié)果對C語言安全子集提出一套規(guī)范化處理流程，包括對不同安全等級的細則建立規(guī)范化識別、規(guī)范化分析以及決策處理流程。

3 創(chuàng)新點

在航天型號軟件C語言安全子集中，編程規(guī)則區(qū)分為不同種類，它們對應(yīng)了不同級別的安全隱患；對于同類準則，編譯器語法、語義對其各個細則的識別能力以及識別位置也不盡相同。不同準則需要不同的識別、分析以及決策。本研究將對子集規(guī)則開展深入分析和研究，將規(guī)則細化分類，根據(jù)不同規(guī)則所具有的危險性將其劃分為不同安全等級，為它們建立規(guī)范的 識別、分析以及決策處理流程。

4 初步結(jié)果

經(jīng)過研究和分析航天型號軟件C語言安全子集所有規(guī)則后，發(fā)現(xiàn)其中要實現(xiàn)的案例大部分都是屬于編譯前端的內(nèi)容，于是我們選擇了Gcc4.9.3編譯器作為我們的基準編譯器，深入研究Gcc的調(diào)用流程如圖1所示，并對GJB5369-2005中的案例進行手工編碼實現(xiàn)，通過對36個案例進行了成功的編碼實現(xiàn)，并分析案例與案例之間的異同，現(xiàn)初步將航天型號軟件C語現(xiàn)言安全子集分為3個錯誤級別，3個錯誤類型。

錯誤級別：

1） fatal：極高危險度，如內(nèi)存泄漏，引起不可預(yù)料后果等錯誤。

2） error：高危險度，如過程名被重用，禁止實參和形參類型不一致等錯誤。

3） Waring：中低危險度，如謹慎使用#pragma，避免使用setjmp/longjmp等錯誤。

錯誤類型：

1） 軟工管理：涉及函數(shù)，參數(shù)，宏相關(guān)，重定義相關(guān)錯誤。

2） 數(shù)值相關(guān)：涉及賦值，內(nèi)存相關(guān)錯誤。

3） 語言規(guī)范：涉及詞法，語法規(guī)范相關(guān)錯誤。

參考文獻：

[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].國防科學(xué)技術(shù)工業(yè)委員會.

[7] 申瑞芬.高可信安全編譯器的設(shè)計與實現(xiàn)[D].長沙：國防科技大學(xué)，2007.

[8] 皮慶基.一種語言靜態(tài)代碼檢測工具[D].北京：北京郵電大學(xué)，2013.

[9] 王蕾.一個C語言安全子集的可信編譯器[J].計算機科學(xué)，2013，40（9）：30-34.endprint