賴策+劉茜

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

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

中圖分類號：TP314 文獻(xiàn)標(biāo)識碼：A 文章編號：1009-3044（2017）26-0086-01

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

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

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

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

3 創(chuàng)新點(diǎn)

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

4 初步結(jié)果

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

錯(cuò)誤級別：

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

2） error：高危險(xiǎn)度，如過程名被重用，禁止實(shí)參和形參類型不一致等錯(cuò)誤。

3） Waring：中低危險(xiǎn)度，如謹(jǐn)慎使用#pragma，避免使用setjmp/longjmp等錯(cuò)誤。

錯(cuò)誤類型：

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

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

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

參考文獻(xià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è)委員會(huì).

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

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

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