安全關(guān)鍵軟件的AADL模型自動(dòng)逆向構(gòu)造方法

邱志凱，楊志斌，謝 健，周 勇，程高輝，陳俊文

1(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106) 2(高安全系統(tǒng)的軟件開(kāi)發(fā)與驗(yàn)證技術(shù)工信部重點(diǎn)實(shí)驗(yàn)室，南京 211106) 3(北京控制與電子技術(shù)研究所，北京 100038)

1 引 言

安全關(guān)鍵軟件(Safety-Critical Software，SCS)[1]是指應(yīng)用于航空、航天、能源等領(lǐng)域的安全關(guān)鍵系統(tǒng)中，且其運(yùn)行情況可能引起系統(tǒng)處于危險(xiǎn)狀態(tài)，從而導(dǎo)致財(cái)產(chǎn)損失、環(huán)境破壞或者人員傷害的一類軟件.即，安全關(guān)鍵軟件一般為安全關(guān)鍵系統(tǒng)的一部分，它可能引起或者助長(zhǎng)不安全的條件，這類軟件被認(rèn)為是安全關(guān)鍵的[2].

模型驅(qū)動(dòng)開(kāi)發(fā)方法(Model-Driven Development，MDD)[3]是一種由對(duì)象管理組織(Object Management Group，OMG)提出的基于抽象模型的軟件開(kāi)發(fā)方法，該方法具有通用性、可擴(kuò)展性、可重用性等特點(diǎn).近年來(lái)，模型驅(qū)動(dòng)開(kāi)發(fā)方法逐漸成為安全關(guān)鍵軟件開(kāi)發(fā)方法的一種發(fā)展趨勢(shì)，例如國(guó)際民航領(lǐng)域使用的機(jī)載系統(tǒng)適航審定中的軟件開(kāi)發(fā)標(biāo)準(zhǔn)DO-178C[4]就將模型驅(qū)動(dòng)和形式化方法作為其核心標(biāo)準(zhǔn)的重要技術(shù)補(bǔ)充.在實(shí)際開(kāi)發(fā)過(guò)程中，構(gòu)造模型的途徑主要有兩種：從需求中構(gòu)造模型，即正向構(gòu)造[5]；從代碼中構(gòu)造模型，即逆向構(gòu)造.在安全關(guān)鍵軟件系統(tǒng)開(kāi)發(fā)與維護(hù)過(guò)程中，部分需求與設(shè)計(jì)信息往往遺留在源代碼中，使用逆向工程將這部分遺留信息從代碼中構(gòu)造到設(shè)計(jì)模型是十分重要的.

模型驅(qū)動(dòng)的逆向工程(Model-DrivenReverse Engineering，MDRE)是逆向工程領(lǐng)域的一個(gè)分支，F(xiàn)avre等人[6]將MDRE定義成“從已經(jīng)存在的系統(tǒng)中構(gòu)造描述性模型”.通常來(lái)說(shuō)，MDRE一般包括兩步：模型發(fā)現(xiàn)和模型理解.MDRE的信息來(lái)源包括源代碼、二進(jìn)制代碼、API等等多種形式，因此，MDRE是從較低抽象級(jí)別的系統(tǒng)模型開(kāi)始，構(gòu)造更高抽象級(jí)別的視圖.相比傳統(tǒng)的逆向工程，MDRE繼承了模型驅(qū)動(dòng)開(kāi)發(fā)的特點(diǎn)，并具有兩個(gè)優(yōu)勢(shì)：首先，模型構(gòu)造過(guò)程是自動(dòng)化的，可以對(duì)逆向過(guò)程進(jìn)行控制；其次，逆向結(jié)果為模型，從而可以分析逆向模型的質(zhì)量[7].近年來(lái)，MDRE也逐漸受到安全關(guān)鍵系統(tǒng)領(lǐng)域的重視和應(yīng)用，例如適航認(rèn)證標(biāo)準(zhǔn)DO-178C和DO-254[8]將MDRE作為其重要的技術(shù)補(bǔ)充.

我們將MDRE已有研究分為兩類：面向通用領(lǐng)域和面向特定領(lǐng)域的逆向構(gòu)造方法.在通用的模型逆向構(gòu)造方法方面，Bruneliere[9]等提出MoDisco，MoDisco是一個(gè)支持系統(tǒng)模型驅(qū)動(dòng)逆向工程的Eclipse開(kāi)源項(xiàng)目，為歷史遺留系統(tǒng)的理解分析、演化、質(zhì)量保障等工作提供了支持.在特定領(lǐng)域的模型逆向構(gòu)造方法方面，在安卓系統(tǒng)領(lǐng)域，Nirumand A[10]提出了一個(gè)基于模型驅(qū)動(dòng)逆向工程框架(VAnDroid)，該框架會(huì)自動(dòng)提取Android應(yīng)用程序中一些與安全有關(guān)的信息，并將其表示為特定領(lǐng)域的模型，可以識(shí)別通信相關(guān)的安全風(fēng)險(xiǎn)和漏洞.

安全關(guān)鍵系統(tǒng)領(lǐng)域常用的建模語(yǔ)言有UML[11]、SysML[12]、EAST-ADL[13]和AADL[14]等.AADL采用統(tǒng)一模型支持多種分析的方式，支持對(duì)安全關(guān)鍵嵌入式系統(tǒng)的軟硬件混合建模，是一種非常適用于安全關(guān)鍵系統(tǒng)的體系結(jié)構(gòu)建模與分析語(yǔ)言.目前AADL正向代碼自動(dòng)生成方面有較多的研究，例如，OCARINA[15]和RAMSES[16]等工具支持AADL模型到C、Ada、Java的代碼自動(dòng)生成.在逆向工程方面，商業(yè)工具STOOD和AADL Inspector支持C/Ada到AADL模型的逆向構(gòu)造，但并未給出具體逆向方法和規(guī)則；Lesovoy[17]等人提出了一種從ARINC 653軟件源代碼中提取AADL模型的方法，該方法主要面向綜合化航空電子設(shè)備(IMA)系統(tǒng)；Bordin[18]等人提出了一種Ada spark到AADL模型雙向轉(zhuǎn)換方法，該方法為了解決異構(gòu)系統(tǒng)集成時(shí)的完整性驗(yàn)證.

本文提出一種C代碼到AADL模型逆向構(gòu)造方法——C2AADL.安全關(guān)鍵軟件常需要考慮安全編碼規(guī)范，因此，我們考慮安全C子集-MISRAC[19].另外，由于源代碼往往運(yùn)行在各種嵌入式平臺(tái)上，所以逆向工程需要處理靜態(tài)結(jié)構(gòu)、動(dòng)態(tài)運(yùn)行時(shí)、功能行為等信息.尤其是，隨著多核處理器在未來(lái)安全關(guān)鍵軟件中廣泛使用，多線程同步互斥、通信、線程調(diào)度和安全編碼規(guī)范等關(guān)鍵信息的逆向構(gòu)造成為重要難題.相比已有的AADL逆向構(gòu)造方法，本文更為完整地考慮了AADL構(gòu)件結(jié)構(gòu)、行為、多線程運(yùn)行時(shí)信息和安全編碼規(guī)范等多個(gè)方面的逆向構(gòu)造.

2 研究背景

2.1 AADL

2004 年，美國(guó)汽車(chē)工程師協(xié)會(huì) SAE(Society of Automotive Engineers)在MetaH、UML 等語(yǔ)言的基礎(chǔ)上，提出嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言 AADL(Architecture Analysis & Design Language)，并發(fā)布為 SAE AS5506 標(biāo)準(zhǔn).AADL采用單一模型支持多種分析的方式，支持對(duì)安全關(guān)鍵嵌入式系統(tǒng)的軟硬件混合建模，是一種非常適用于安全關(guān)鍵系統(tǒng)的體系結(jié)構(gòu)建模與分析語(yǔ)言.

安全關(guān)鍵系統(tǒng)是一種將硬件平臺(tái)、軟件和運(yùn)行時(shí)環(huán)境深度融合的復(fù)雜系統(tǒng)，而AADL是一種基于構(gòu)件(Component)的軟硬件建模語(yǔ)言，并與之對(duì)應(yīng)的提供了硬件、軟件、執(zhí)行模型3種建模概念，核心構(gòu)件如圖1所示.

圖1 AADL基本建模概念Fig.1 AADL basic modeling concepts

在AADL核心構(gòu)件的基礎(chǔ)上，AADL還提供了兩種擴(kuò)展機(jī)制，分別是基于自定義屬性集(Property Set)的擴(kuò)展和基于附件(Annex)的擴(kuò)展.構(gòu)件內(nèi)部的功能行為描述可以通過(guò)AADL Behavior Annex[20]、C和Ada實(shí)現(xiàn).Behavior Annex與執(zhí)行模型有密切的關(guān)系：執(zhí)行模型的分發(fā)機(jī)制定義了線程、子程序周期性或非周期性地讀取數(shù)據(jù)、計(jì)算、發(fā)送數(shù)據(jù)，BA則是對(duì)計(jì)算狀態(tài)內(nèi)的執(zhí)行行為進(jìn)行詳細(xì)刻畫(huà).

2.2 MISRA C

MISRA C是由汽車(chē)工業(yè)軟件可靠性協(xié)會(huì) (The Motor Industry Software Reliability Association，MISRA)提出的嵌入式C語(yǔ)言開(kāi)發(fā)標(biāo)準(zhǔn)，目的是提高嵌入式系統(tǒng)的安全性、可讀性和可移植性.

在MISRAC：2012中，共有159條規(guī)則和指令，其中規(guī)則143條，指令16條.而這些指令和規(guī)則又分為5個(gè)類：建議規(guī)則、建議指令、必要規(guī)則、必要指令和強(qiáng)制規(guī)則.任何符合MISRAC：2012編程規(guī)范的代碼都應(yīng)該嚴(yán)格地遵循強(qiáng)制規(guī)則的要求，需要遵循必要指令/規(guī)則(如果背離，需要注明背離原因)，并應(yīng)該在條件允許的情況下盡可能符合建議規(guī)則/指令.表1列出部分安全編碼規(guī)范內(nèi)容.

表1 安全編碼規(guī)范Table 1 Secure coding standards

3 逆向構(gòu)造方法

C2AADL逆向構(gòu)造方法的總體框架如圖2所示，主要分為4個(gè)部分：

1)源碼解析：將輸入的多線程C代碼轉(zhuǎn)換為抽象語(yǔ)法樹(shù)，抽象語(yǔ)法樹(shù)中包含了源碼的結(jié)構(gòu)和行為信息，運(yùn)行時(shí)性質(zhì)則包含在具體的語(yǔ)句中；

2) 中間模型提?。涸创a解析的抽象語(yǔ)法樹(shù)和安全編碼規(guī)范作為輸入，根據(jù)本文提出的轉(zhuǎn)換規(guī)則，將規(guī)則所需要的結(jié)構(gòu)、行為、運(yùn)行時(shí)性質(zhì)和安全編碼規(guī)范信息從輸入中提取到中間模型；

3) AADL模型生成：包含了源碼結(jié)構(gòu)、行為、運(yùn)行時(shí)信息的中間模型作為輸入，根據(jù)轉(zhuǎn)換規(guī)則將中間模型的元素與AADL模型之間進(jìn)行對(duì)應(yīng)轉(zhuǎn)換.

4)模型驗(yàn)證：在逆向構(gòu)造之后，可以基于模型檢測(cè)工具UPPAAL[21]和組合驗(yàn)證工具AGREE[22]對(duì)AADL模型進(jìn)行形式化驗(yàn)證.

圖2 C2AADL框架Fig.2 Framework of C2AADL

本文主要給出前3步從源代碼的AADL模型的逆向構(gòu)造工作.

3.1 源語(yǔ)言分析

本節(jié)將介紹基于抽象語(yǔ)法樹(shù)提取的C程序的對(duì)象文檔模型(Document Object Model，DOM)，在Eclipse C/C++開(kāi)發(fā)工具(CDT)中DOM的思想被用來(lái)在CDT程序內(nèi)部存儲(chǔ)C/C++文檔，使用CDT對(duì)C代碼進(jìn)行解析得到的抽象語(yǔ)法樹(shù)，而MISRAC是一種安全編碼的規(guī)范，其屬性已包含在源碼中，即也包含在抽象語(yǔ)法樹(shù)中.圖3給出了一個(gè)CDTDOM解析的例子，下面對(duì)抽象語(yǔ)法樹(shù)3個(gè)層次進(jìn)行說(shuō)明，即程序組織結(jié)構(gòu)、單文件結(jié)構(gòu)和函數(shù)模塊.

1)程序組織結(jié)構(gòu)：抽象語(yǔ)法樹(shù)中最頂層元素ICModel表示整個(gè)環(huán)境的workspace；ICModel包含ICContainer和ICProject，分別表示workspace中的工程和文件組；ICProject包含一個(gè)或多個(gè)ISourceRoot表示工程空間中的文件組織結(jié)構(gòu)；每個(gè)ISourceRoot中可以包含一個(gè)或多個(gè)ITranslationUnit，表示單個(gè)C程序文件.ITranslationUnit是DOM模型中最重要的元素，每一個(gè)ITranslationUnit都包含源文件中的多種程序組成，如宏定義、聲明、實(shí)現(xiàn)等；

2)單文件結(jié)構(gòu)：在ITranslationUnit中包含一個(gè)或多個(gè)IASTDeclaration，IASTDeclaration可以是函數(shù)的頭部聲明，例如IInclude、IUsing和INamespace等，也可以是對(duì)程序文件內(nèi)的函數(shù)、變量等的聲明，例如IASTFunctionDefinition和IASTSimpleDeclaration等；

3)函數(shù)模塊：函數(shù)聲明IASTFunctionDefinition主要有4部分：IASTDeclSpecifier、IASTFunctionDeclarator和IASTCompoundStatement.IASTDeclSpecifier表示函數(shù)返回值類型；IASTFunctionDeclarator包含IASTName和IASTParameterDeclaration，分別表示函數(shù)名和函數(shù)參數(shù)；IASTCompoundStatement由一組IASTStatement組成表示函數(shù)的具體內(nèi)容，IASTStatement可以是多種Statement的實(shí)現(xiàn)，例如IASTIfStatement、IASTForStatement、IASTSwitchStatement、IASTWhileStatement和IASTReturnStatement等.

圖3 CDT DOM 解析Fig.3 CDT DOM parsing

3.2 轉(zhuǎn)換規(guī)則

在源碼分析的基礎(chǔ)上，本節(jié)給出源代碼到AADL模型轉(zhuǎn)換的轉(zhuǎn)換規(guī)則.轉(zhuǎn)換規(guī)則為C到AADL的逆向構(gòu)造提供了映射關(guān)系，而中間模型是C到AADL實(shí)現(xiàn)的橋梁.源碼結(jié)構(gòu)的轉(zhuǎn)換規(guī)則包括：全局變量、局部變量、復(fù)合數(shù)據(jù)類型、線程和函數(shù)結(jié)構(gòu)；源碼行為的轉(zhuǎn)換規(guī)則包括：賦值語(yǔ)句、分支語(yǔ)句、循環(huán)語(yǔ)句以及函數(shù)調(diào)用；源碼運(yùn)行時(shí)性質(zhì)轉(zhuǎn)換規(guī)則包括：多線程通信、多線程同步、多線程調(diào)度以及安全編碼規(guī)范.

3.2.1 結(jié)構(gòu)轉(zhuǎn)換規(guī)則

結(jié)構(gòu)方面的轉(zhuǎn)換規(guī)則主要包括：基本數(shù)據(jù)類型和復(fù)合數(shù)據(jù)類型的變量到AADLData組件的轉(zhuǎn)換、函數(shù)模塊到AADLSubprogram組件的轉(zhuǎn)換、任務(wù)模塊到AADLThread組件的轉(zhuǎn)換.

由于C語(yǔ)言中的變量和AADL中的數(shù)據(jù)組件對(duì)數(shù)據(jù)類型的描述相似，因此我們將變量映射到數(shù)據(jù)組件.為了使AADL的結(jié)構(gòu)更清晰，我們將數(shù)據(jù)組件封裝為兩種類型的包：一個(gè)包表示名為Base_Types的基本數(shù)據(jù)類型，另一個(gè)包表示名為User_Define的擴(kuò)展數(shù)據(jù)類型(復(fù)合數(shù)據(jù)類型).通常，對(duì)于基本數(shù)據(jù)類型，使用數(shù)據(jù)聲明(Data)對(duì)應(yīng)用程序數(shù)據(jù)建模就足夠了，并且不必聲明數(shù)據(jù)實(shí)現(xiàn)(Data Implementation).對(duì)于具有內(nèi)部實(shí)現(xiàn)的擴(kuò)展數(shù)據(jù)類型，擴(kuò)展數(shù)據(jù)的元素映射到數(shù)據(jù)實(shí)現(xiàn)中聲明的子組件.C語(yǔ)言的函數(shù)和任務(wù)模塊分別映射到AADLsubprogram和thread組件.具體的轉(zhuǎn)換規(guī)則如表2所示.

表2 結(jié)構(gòu)轉(zhuǎn)換規(guī)則Table 2 Transformation rules of structure

由于本文篇幅所限，表2中僅列出了一部分?jǐn)?shù)據(jù)類型.例如，它不包括由unsigned和signed聲明的數(shù)據(jù)類型.映射規(guī)則應(yīng)考慮在標(biāo)準(zhǔn)C和Code Composer Studio(CCS)中定義的所有數(shù)據(jù)類型.如表2所示，對(duì)于沒(méi)有內(nèi)部元素的基本數(shù)據(jù)類型，相應(yīng)的數(shù)據(jù)組件僅具有數(shù)據(jù)類型；對(duì)于具有內(nèi)部元素的擴(kuò)展數(shù)據(jù)類型，相應(yīng)的數(shù)據(jù)組件具有數(shù)據(jù)聲明以及數(shù)據(jù)實(shí)現(xiàn).C語(yǔ)言定義了一種特殊的類型，稱為“指針”.對(duì)于表2中所示的指針數(shù)據(jù)類型，我們將指針指向的數(shù)據(jù)類型視為數(shù)據(jù)組件類型.

在CCS中，多任務(wù)(TASK)代表執(zhí)行的并發(fā)路徑，而AADL中的線程組件是順序執(zhí)行的并發(fā)可調(diào)度單元.多個(gè)線程代表并發(fā)執(zhí)行路徑.可以將各種執(zhí)行屬性分配給線程，包括定時(shí)(例如，最壞情況下的執(zhí)行時(shí)間)，調(diào)度協(xié)議(例如，周期性，非周期性等)，內(nèi)存大小和處理器綁定.因此我們將任務(wù)(TASK)映射到AADLthread組件.除任務(wù)外，常規(guī)功能在CCS中使用函數(shù)定義.函數(shù)表示順序執(zhí)行，可以由多個(gè)任務(wù)調(diào)用，并且它們應(yīng)該是可重用的.AADL中的subprogram組件表示順序可執(zhí)行的源文本，該組件是一個(gè)帶有(不帶有)參數(shù)的可調(diào)用組件，為調(diào)用它的組件提供服務(wù)功能.基于函數(shù)和子程序組件之間的相似語(yǔ)義，我們將函數(shù)映射到子程序組件.

3.2.2 行為轉(zhuǎn)換規(guī)則

函數(shù)和線程執(zhí)行行為主要由一系列語(yǔ)句(例如，順序語(yǔ)句、分支語(yǔ)句、循環(huán)語(yǔ)句等)按照特定的順序執(zhí)行實(shí)現(xiàn)，關(guān)于行為的轉(zhuǎn)換規(guī)則主要介紹順序語(yǔ)句、if條件語(yǔ)句、switch分支語(yǔ)句、for循環(huán)語(yǔ)句、while循環(huán)語(yǔ)句，函數(shù)調(diào)用語(yǔ)句等到AADL行為附件的轉(zhuǎn)換.

AADL行為附件對(duì)于行為的描述如圖4上方所示，其中states表示執(zhí)行過(guò)程所需的所有狀態(tài)，transitions中si表示源狀態(tài)，sj表示目的狀態(tài)，guard表示狀態(tài)轉(zhuǎn)移的條件，action表示狀態(tài)轉(zhuǎn)移時(shí)執(zhí)行的動(dòng)作.為了更好的展示轉(zhuǎn)換規(guī)則，我們將AADL行為附件的描述內(nèi)容顯示為狀態(tài)機(jī)，狀態(tài)轉(zhuǎn)移線上表示守衛(wèi)條件，線下表示執(zhí)行動(dòng)作.具體的轉(zhuǎn)換規(guī)則如圖4所示.

圖4 行為轉(zhuǎn)換規(guī)則Fig.4 Transformation rules of behavior

源語(yǔ)言中順序語(yǔ)句一般由操作數(shù)和操作符組成.源語(yǔ)言操作數(shù)的名稱對(duì)應(yīng)于AADL行為附件動(dòng)作中的數(shù)據(jù)名稱；源語(yǔ)言操作符轉(zhuǎn)換到AADL模型操作符號(hào)，例如：“=”轉(zhuǎn)換為“：=”、“！”轉(zhuǎn)換為“not”等.

源語(yǔ)言的If條件語(yǔ)句在轉(zhuǎn)換到AADL模型時(shí)的關(guān)鍵信息是：If語(yǔ)句的判斷條件和判斷滿足后的執(zhí)行內(nèi)容.其中If判斷條件轉(zhuǎn)換到AADL行為附件中狀態(tài)遷移的守衛(wèi)條件，執(zhí)行內(nèi)容轉(zhuǎn)換到AADL狀態(tài)轉(zhuǎn)移守衛(wèi)條件滿足后的動(dòng)作.

源語(yǔ)言Switch-Case語(yǔ)句的關(guān)鍵信息包括3部分：Switch中的控制表達(dá)式、Case中的表達(dá)式以及每個(gè)Case后的動(dòng)作.Switch中的控制表達(dá)式和Case中的表達(dá)式使用等號(hào)連接成一個(gè)AADL狀態(tài)轉(zhuǎn)移的守衛(wèi)條件，每個(gè)Case后的動(dòng)作對(duì)應(yīng)每個(gè)AADL狀態(tài)遷移時(shí)的執(zhí)行內(nèi)容.源語(yǔ)言Switch-Case語(yǔ)句對(duì)應(yīng)的所有AADL狀態(tài)轉(zhuǎn)移的起始狀態(tài)相同，終止?fàn)顟B(tài)也相同.

源語(yǔ)言的for循環(huán)語(yǔ)句主要關(guān)注4個(gè)點(diǎn)：初始化表達(dá)式、循環(huán)條件、迭代表達(dá)式以及循環(huán)內(nèi)容.其中源語(yǔ)言初始化表達(dá)式對(duì)應(yīng)AADL行為附件循環(huán)前的一個(gè)狀態(tài)轉(zhuǎn)移的動(dòng)作；循環(huán)條件對(duì)應(yīng)AADL行為附件循環(huán)狀態(tài)遷移的守衛(wèi)條件；循環(huán)內(nèi)容對(duì)應(yīng)于AADL循環(huán)狀態(tài)遷移的動(dòng)作；迭代表達(dá)式對(duì)應(yīng)行為附件執(zhí)行動(dòng)作最后的動(dòng)作.

源語(yǔ)言的While循環(huán)關(guān)鍵信息是循環(huán)判斷條件，While循環(huán)語(yǔ)句轉(zhuǎn)換到AADL行為附件中的狀態(tài)遷移，其中該狀態(tài)遷移的起始狀態(tài)和目的狀態(tài)相同，狀態(tài)遷移條件是While循環(huán)判斷條件.

函數(shù)調(diào)用語(yǔ)句的關(guān)鍵信息分為3部分：函數(shù)名稱，輸入?yún)?shù)名稱和接收返回值的變量名稱.源語(yǔ)言的函數(shù)名稱轉(zhuǎn)換到AADL子程序名稱，注意AADL子程序名稱后需要加！，表示子程序調(diào)用；源語(yǔ)言的輸入?yún)?shù)名稱按順序?qū)?yīng)于AADL子程序調(diào)用的輸入?yún)?shù)名稱；源語(yǔ)言接收返回值的變量對(duì)應(yīng)AADL子程序調(diào)用括號(hào)最后的參數(shù).

3.2.3 運(yùn)行時(shí)轉(zhuǎn)換規(guī)則

運(yùn)行時(shí)的轉(zhuǎn)換規(guī)則主要考慮所使用平臺(tái)的API和安全編碼規(guī)范到AADL模型的轉(zhuǎn)換，因此轉(zhuǎn)換規(guī)則會(huì)展示一部分平臺(tái)的API.運(yùn)行時(shí)的轉(zhuǎn)換規(guī)則主要包括：多線程通信、多線程調(diào)度、多線程同步以及安全編碼規(guī)范.為了方便展示轉(zhuǎn)換規(guī)則，圖5頂部展示了在osate工具中AADL文本模型對(duì)應(yīng)的可視化圖形，具體轉(zhuǎn)換規(guī)則如圖5所示.

圖5 運(yùn)行時(shí)性質(zhì)轉(zhuǎn)換規(guī)則Fig.5 Transformation rules of runtime

線程間通信主要包含3種方式：共享數(shù)據(jù)、數(shù)據(jù)傳輸和事件(信號(hào)).共享數(shù)據(jù)是使用全局變量實(shí)現(xiàn)的，線程通過(guò)讀取和寫(xiě)入全局變量進(jìn)行通信；數(shù)據(jù)傳輸是通過(guò)郵箱隊(duì)列實(shí)現(xiàn)，數(shù)據(jù)發(fā)送者可以將數(shù)據(jù)發(fā)送到隊(duì)列，而數(shù)據(jù)接收者可以從隊(duì)列中獲取數(shù)據(jù)；事件通知通過(guò)發(fā)送信號(hào)量來(lái)實(shí)現(xiàn)，信號(hào)量是二進(jìn)制數(shù)據(jù).圖5所示的3種通信方式轉(zhuǎn)換規(guī)則：a)表示共享數(shù)據(jù)轉(zhuǎn)換規(guī)則，源代碼中進(jìn)出隊(duì)函數(shù)通過(guò)共享變量操作隊(duì)列數(shù)據(jù)，其中隊(duì)列數(shù)據(jù)為全局變量，對(duì)應(yīng)生成的AADL模型在進(jìn)程中包含這兩個(gè)函數(shù)和全局變量，并通過(guò)Data Access將全局變量與兩個(gè)函數(shù)進(jìn)行連接；b)表示通知信號(hào)轉(zhuǎn)換規(guī)則，源代碼中兩個(gè)線程通過(guò)發(fā)送和接收signal信號(hào)實(shí)現(xiàn)通信，對(duì)應(yīng)生成的AADL模型在進(jìn)程包含這兩個(gè)線程，并通過(guò)端口連接將兩個(gè)線程的信號(hào)收發(fā)端口連接，二進(jìn)制信號(hào)對(duì)應(yīng)AADL模型Event端口；c)表示數(shù)據(jù)傳輸轉(zhuǎn)轉(zhuǎn)換規(guī)則，源代碼中消息發(fā)送線程通過(guò)郵箱機(jī)制將數(shù)據(jù)發(fā)送接受任務(wù)，生成的AADL模型中進(jìn)程包含兩個(gè)線程，并使用端口連接將發(fā)送端口與接收端口連接，該端口為Data端口.

在CCS SYS/BIOS中使用信號(hào)量和郵箱機(jī)制實(shí)現(xiàn)線程之間的調(diào)度，信號(hào)量轉(zhuǎn)換規(guī)則如圖5中(d)所示，源代碼線程在等待信號(hào)量時(shí)，則線程掛起，收到信號(hào)量后恢復(fù)執(zhí)行，在AADL中對(duì)應(yīng)于On Dispatch從Complete狀態(tài)(圖中虛線橢圓狀態(tài))轉(zhuǎn)移到執(zhí)行狀態(tài).郵箱機(jī)制轉(zhuǎn)換規(guī)則中源代碼線程在等待郵箱數(shù)據(jù)時(shí)線程掛機(jī)，等待數(shù)據(jù)到來(lái)后，線程恢復(fù)執(zhí)行，對(duì)應(yīng)于AADL模型中On Dispatch從Complete狀態(tài)到執(zhí)行狀態(tài)的轉(zhuǎn)換，并在狀態(tài)轉(zhuǎn)移時(shí)讀出端口數(shù)據(jù).

表3 編碼規(guī)范轉(zhuǎn)換規(guī)則Table 3 Transformation rules of coding standards

安全編碼規(guī)范通過(guò)AADL屬性集表達(dá)，屬于執(zhí)行模型的一部分.表3中的安全編碼規(guī)范與源碼屬性相關(guān)，指定函數(shù)/變量性質(zhì)的規(guī)范轉(zhuǎn)換為AADL屬性集，并和相應(yīng)的構(gòu)件進(jìn)行綁定.關(guān)于安全編碼規(guī)范的轉(zhuǎn)換規(guī)則與上述轉(zhuǎn)換規(guī)則有所不同，首先給出MISRA C中規(guī)范的定義，然后給出該規(guī)范對(duì)應(yīng)的AADL屬性集，最后給出案例中使用到該規(guī)范的源碼，并給出轉(zhuǎn)換到AADL構(gòu)件時(shí)的屬性綁定.

4 原型工具

本節(jié)首先介紹便于C代碼信息提取和AADL模型生成的中間模型，然后介紹原型工具C2AADL設(shè)計(jì)實(shí)現(xiàn).

4.1 中間模型

在處理C程序的過(guò)程中，程序多種元素往往耦合緊密，為了能夠在轉(zhuǎn)換到AADL模型前將模型盡可能簡(jiǎn)化，屏蔽轉(zhuǎn)換過(guò)程中不關(guān)心的組成成分，本小節(jié)基于C代碼和AADL模型特征提出一個(gè)C到AADL轉(zhuǎn)換的中間模型-CAInterM，如圖6所示.中間模型的結(jié)構(gòu)與C語(yǔ)言項(xiàng)目結(jié)構(gòu)一致，一個(gè)C語(yǔ)言工程包含若干個(gè)源文件，每個(gè)源文件包含全局變量和函數(shù)，每個(gè)函數(shù)包含自己的局部變量和函數(shù)行為等.圖6中CProjectModel存儲(chǔ)了項(xiàng)目名稱信息(Name)、項(xiàng)目文件結(jié)構(gòu)信息(CModules)和項(xiàng)目用到的編碼規(guī)范(properties)，其中CModules包含了全部的程序文件信息(SingleCModel).SingleCModel是單個(gè)文件的存儲(chǔ)體，包含了一個(gè)相同文件名的.c和.h文件定義的全局變量(GlobalVars)、函數(shù)(Functions)、數(shù)據(jù)類型(Datas)和引用的文件(Includes).FunctionModel是對(duì)函數(shù)內(nèi)容的記載，它包含函數(shù)名稱(Name)、輸入?yún)?shù)(Paras)、返回值(ReturnValue)、局部變量(LocalVars)、引用的變量(Data Access)和函數(shù)行為(StateList).DataModel是對(duì)定義的復(fù)合數(shù)據(jù)類型信息的存儲(chǔ)，它包含定義的復(fù)合數(shù)據(jù)類型的名稱(Name)、復(fù)合數(shù)據(jù)類型內(nèi)部變量(Vars)和函數(shù)(Subs).考慮AADL模型特征設(shè)計(jì)中間模型的具體內(nèi)容，Statement是對(duì)源碼函數(shù)行為的記載，包括AADL行為附件中狀態(tài)遷移所需的初始狀態(tài)、目的狀態(tài)、守衛(wèi)條件和執(zhí)行內(nèi)容；VarModel是對(duì)源碼局部變量和復(fù)合數(shù)據(jù)類型成員變量的記載，包括AADL數(shù)據(jù)構(gòu)件所需的變量名稱、變量類型、變量來(lái)源以及變量初始值；ConnectionModel記錄源碼線程/函數(shù)間使用全局變量或端口的通信，包括了AADL構(gòu)件連接所需的源、目的和數(shù)據(jù)/端口名；MISRACModel記錄了安全編碼規(guī)范對(duì)應(yīng)的屬性名稱，屬性類型以及屬性綁定的組件.

圖6 中間模型：CAInterMFig.6 Intermediate model： CAInterM

設(shè)計(jì)該中間模型的意義在于：1)減少轉(zhuǎn)換過(guò)程中需要考慮的信息量；2)將C程序模型保存成層次化結(jié)構(gòu)，易于轉(zhuǎn)換；3)保證了本文所提轉(zhuǎn)轉(zhuǎn)換方法的可擴(kuò)展性.表4給出C語(yǔ)言抽象語(yǔ)法樹(shù)到中間模型的映射關(guān)系.

表4 抽象語(yǔ)法樹(shù)到中間模型映射Table 4 Mapping from AST to intermediate model

4.2 工具實(shí)現(xiàn)

C2AADL模型逆向構(gòu)造工具是基于Java編程實(shí)現(xiàn)的.整個(gè)模型逆向構(gòu)造工具框架如圖7所示，工具采用模塊化思想，包括源代碼到中間模型抽取、安全編碼規(guī)范到中間模型的抽取和AADL模型生成.本節(jié)主要介紹C2AADL模型逆向構(gòu)造工具的實(shí)現(xiàn).

圖7 C2AADL工具框架Fig.7 Framework of C2AADL tool

模型逆向構(gòu)造工具功能模塊的主要步驟及其對(duì)應(yīng)的Java代碼數(shù)量統(tǒng)計(jì)見(jiàn)表5.

表5 C2AADL模型逆向構(gòu)造工具主要步驟Table 5 Main steps of the model reverse construction tool

工具開(kāi)發(fā)環(huán)境為基于Eclipse平臺(tái)的Osate插件環(huán)境.將需要進(jìn)行逆向轉(zhuǎn)換的項(xiàng)目導(dǎo)入工具后，右擊導(dǎo)入的項(xiàng)目啟動(dòng)逆向轉(zhuǎn)換功能，可以在工具內(nèi)對(duì)導(dǎo)入的項(xiàng)目文件內(nèi)容進(jìn)行修改調(diào)整，并查看生成的AADL模型.

5 案例研究

針對(duì)雷達(dá)信息處理子系統(tǒng)案例，首先使用本文實(shí)現(xiàn)的工具對(duì)該案例進(jìn)行逆向模型構(gòu)造，并對(duì)逆向結(jié)果進(jìn)行分析，其次將本文實(shí)現(xiàn)的方法和相關(guān)MDRE方法進(jìn)行分析比較得出結(jié)論，最后分析C2AADL方法的效性.

5.1 案例介紹

雷達(dá)信息處理子系統(tǒng)是指使用調(diào)制的波形和定向天線向空間中的特定空域發(fā)射電磁波，從接收的回波中提取制導(dǎo)信息的系統(tǒng).雷達(dá)信息處理子系統(tǒng)功能分解，主要包括3層：DSP平臺(tái)層、系統(tǒng)控制層和SAR(Synthetic Aperture Radar)實(shí)現(xiàn)層.DSP平臺(tái)層主要采用多核DSP處理器，包括UART通信、1553B總線通信、以太網(wǎng)通信、AD采集、SRIO通信和核間通信模塊；系統(tǒng)控制層主要是模式轉(zhuǎn)換和任務(wù)調(diào)度，包括：前端分機(jī)控制、任務(wù)控制和參數(shù)裝定模塊；SAR實(shí)現(xiàn)層利用合成孔徑原理實(shí)現(xiàn)高分辨的微波成像，包括：信號(hào)預(yù)處理模塊、圖像處理模塊和匹配處理模塊.

雷達(dá)信息處理子系統(tǒng)使用在機(jī)載SAR雷達(dá)中，該系統(tǒng)利用飛機(jī)平臺(tái)的飛行路徑，合成一個(gè)等效的“大天線”，并生成高分辨率的遙感影像.在每個(gè)發(fā)送/接收周期，對(duì)來(lái)自合成孔徑元件上連續(xù)脈沖信號(hào)的幅度和相位進(jìn)行處理，獲取的數(shù)據(jù)存儲(chǔ)在存儲(chǔ)器中.在給定周期數(shù)后，將存儲(chǔ)的數(shù)據(jù)重新組合，以創(chuàng)建正在飛越地形的高分辨率圖像.

雷達(dá)信息處理子系統(tǒng)主要包括3層的主要功能如下：

·DSP平臺(tái)層主要功能：不同DSP之間的板間通信和多核DSP中的核間通信、以太網(wǎng)和異步收發(fā)器與系統(tǒng)層之間的通信、串行多路數(shù)據(jù)總線通信和從AD芯片上采集需要量化的信號(hào)；

·系統(tǒng)實(shí)現(xiàn)層主要功能：根據(jù)指令選擇SAR工作模型，控制各分機(jī)工作(任務(wù)控制功能)；各分機(jī)啟動(dòng)自檢開(kāi)始信號(hào)采集工作(前端分機(jī)控制)；將收集的數(shù)據(jù)重新組合裝定完成量化處理(參數(shù)裝定)；

·SAR實(shí)現(xiàn)層主要功能：處理從位置A到D時(shí)間段T內(nèi)所有雷達(dá)所返回的信號(hào)(信號(hào)預(yù)處理)；合成預(yù)處理信號(hào)，從而延長(zhǎng)天線長(zhǎng)度，實(shí)現(xiàn)更高分辨率(圖像處理)；當(dāng)目標(biāo)進(jìn)入雷達(dá)波束，將目標(biāo)與雷達(dá)圖像相結(jié)合，完成目標(biāo)匹配(匹配處理).

圖8 任務(wù)控制功能分解Fig.8 Functional decomposition of task control

本文主要考慮系統(tǒng)控制層的任務(wù)控制功能里12個(gè)任務(wù)間相互調(diào)度和通信.具體任務(wù)的主要功能流程如圖8所示：Task1接收到1553中斷后解析1553消息，然后將控制指令發(fā)送給主控任務(wù)Task0；Task0根據(jù)控制指令后進(jìn)行判斷，將系統(tǒng)參數(shù)發(fā)送給Task4，啟動(dòng)前端分機(jī)自檢，或者將子圖分發(fā)給Task8～Task14，啟動(dòng)子圖處理；Task8-14處理完畢后將子圖發(fā)送給Task3，其中Task8同時(shí)兼有編排遙測(cè)數(shù)據(jù)，啟動(dòng)遙測(cè)數(shù)據(jù)傳輸任務(wù)的功能；Task3接收Task8-14發(fā)送的子圖后進(jìn)行拼接，并完成量化處理.

5.2 案例分析

本文的案例分析旨在回答以下兩個(gè)研究問(wèn)題：

1)RQ1.本文方法的有效性如何？RQ1旨在調(diào)查本文方法在應(yīng)用到大型工業(yè)界案例時(shí)是否具有實(shí)際的價(jià)值，我們通過(guò)一個(gè)雷達(dá)信息處理子系統(tǒng)對(duì)此進(jìn)行評(píng)估.

2)RQ2.與其他工具相比，本文所提出的工具有哪些優(yōu)勢(shì)？RQ2通過(guò)由現(xiàn)有其他逆向構(gòu)造方法的轉(zhuǎn)換進(jìn)行比較，我們可以得出本文所提方法的優(yōu)點(diǎn).

本文從系統(tǒng)層面，單構(gòu)件行為層面和多構(gòu)件同步調(diào)度層面對(duì)生成的雷達(dá)AADL模型進(jìn)行分析：

系統(tǒng)層：逆向構(gòu)造的AADL模型中，整個(gè)任務(wù)控制功能對(duì)應(yīng)一個(gè)頂層系統(tǒng)構(gòu)件System.該功能中的其他內(nèi)容對(duì)應(yīng)相應(yīng)的Subprogram，Process，Data，Thread等構(gòu)件，其中一個(gè)比較特殊的函數(shù)是Main函數(shù)，它對(duì)應(yīng)一個(gè)Process構(gòu)件，程序的執(zhí)行順序通過(guò)函數(shù)調(diào)用和線程調(diào)度表達(dá).如圖9(a)所示是構(gòu)造的任務(wù)控制功能的頂層框架：一個(gè)系統(tǒng)中的主進(jìn)程；主進(jìn)程中包含主控系統(tǒng)的所有線程、全局變量以及數(shù)據(jù)連接和端口連接.所生成的AADL模型框架架構(gòu)與案例介紹時(shí)圖11的框架一致.

圖9 逆向生成的AADL模型Fig.9 Generated AADL models

單構(gòu)件行為層：在結(jié)構(gòu)和行為的分析中，以任務(wù)控制功能中通信時(shí)消息隊(duì)列出隊(duì)模塊為例.圖9(b)所示的代碼中InterCoreDequeue函數(shù)轉(zhuǎn)換到AADL模型對(duì)應(yīng)Subprogram構(gòu)件，其中函數(shù)輸入?yún)?shù)轉(zhuǎn)換成了Subprogram構(gòu)件的In Parameter，安全編碼的屬性集也與Out Parameter進(jìn)行了綁定，函數(shù)的執(zhí)行內(nèi)容構(gòu)造在子程序的行為附件里，其中包含了共享數(shù)據(jù)訪問(wèn)、順序表達(dá)式、If條件句和Return語(yǔ)句等.

多構(gòu)件同步調(diào)度層：多線程的運(yùn)行時(shí)重點(diǎn)在于線程的運(yùn)行狀態(tài)，線程在狀態(tài)遷移時(shí)Complete狀態(tài)用于表示線程掛起等待被調(diào)度.當(dāng)線程等待的端口接收到信息后，轉(zhuǎn)換到執(zhí)行狀態(tài).由于有端口的存在，線程構(gòu)件也有用于通信的端口連接.圖9(c)所示任務(wù)控制功能中Task0檢查為例，該任務(wù)初始狀態(tài)為Complete狀態(tài)等待信號(hào)Sync的到來(lái)，接收信號(hào)后調(diào)度執(zhí)行，運(yùn)行過(guò)程中會(huì)等待1553信號(hào)解析后的數(shù)據(jù)，并根據(jù)數(shù)據(jù)內(nèi)容判斷啟動(dòng)自檢、設(shè)置時(shí)間、雷達(dá)掃描功能.

生成的AADL模型減少了相關(guān)研究人員理解項(xiàng)目所需的時(shí)間，可以補(bǔ)充因長(zhǎng)時(shí)間開(kāi)發(fā)所造成的文檔缺失，并為進(jìn)一步基于模型驅(qū)動(dòng)的開(kāi)發(fā)提供了源模型.

RQ1：通過(guò)完整的代碼分析以及AADL模型逆向構(gòu)造，我們可以看出，本方法對(duì)于復(fù)雜結(jié)構(gòu)的工業(yè)級(jí)系統(tǒng)有良好的支持，模型構(gòu)造過(guò)程自動(dòng)化.

表6為雷達(dá)信息處理子系統(tǒng)的AADL模型數(shù)據(jù)統(tǒng)計(jì)，AADL模型元素分為3個(gè)部分：

表6 AADL模型統(tǒng)計(jì)Table 6 AADL model statistics

1)描述靜態(tài)功能架構(gòu)的模型元素，涉及整個(gè)系統(tǒng)中的System、Process、Thread、Subprogram和Data元素；

2)描述系統(tǒng)動(dòng)態(tài)行為的元素，涉及線程函數(shù)中的Subprogram Implementation、Thread Implementation和BA；

3)描述非功能屬性的元素，涉及源碼編碼規(guī)范的Property Set.

RQ2：我們將C2AADL與MDRE領(lǐng)域中的方法進(jìn)行了比較，表7中利用4個(gè)參數(shù)進(jìn)行此比較，即輸入、輸出、可以分析的類型(結(jié)構(gòu)、行為、執(zhí)行模型)和工具.

評(píng)估結(jié)果如表7所示.在MDRE方法[9，10，25，26，28]中，研究人員僅關(guān)注源代碼的結(jié)構(gòu)；在文獻(xiàn)[23，24，27，29]中相比上述方法更關(guān)注了源碼的行為信息.而C2AADL比較完整地支持處理遺留系統(tǒng)的結(jié)構(gòu)、行為和運(yùn)行時(shí)性質(zhì)的逆向構(gòu)造，并且在模型中綁定屬性集表示編碼規(guī)范使AADL模型更加精確.

表7 MDRE工具和方法評(píng)價(jià)Table 7 Evaluation of MDRE tools and methods

6 結(jié)束語(yǔ)

安全關(guān)鍵系統(tǒng)開(kāi)發(fā)過(guò)程中，源代碼中所包含的部分設(shè)計(jì)信息未能及時(shí)補(bǔ)充到設(shè)計(jì)模型，如何將源碼信息自動(dòng)構(gòu)造到設(shè)計(jì)模型中是該領(lǐng)域的研究熱點(diǎn).本文提出了一種基于源代碼的AADL模型自動(dòng)逆向構(gòu)造方法和工具.首先將C語(yǔ)言程序轉(zhuǎn)換為抽象語(yǔ)法樹(shù)，獲取源碼中的設(shè)計(jì)信息；然后將源碼使用到的編碼規(guī)范和抽象語(yǔ)法樹(shù)作為輸入，并按照轉(zhuǎn)換規(guī)則所需的信息生成逆向轉(zhuǎn)換的中間模型；最后將中間模型按照轉(zhuǎn)換規(guī)則生成AADL基本構(gòu)件、行為附件和屬性集.通過(guò)對(duì)使用多任務(wù)的雷達(dá)信息控制子系統(tǒng)的逆向構(gòu)造驗(yàn)證了本方法的有效性.

在未來(lái)的工作中，我們將進(jìn)一步開(kāi)展以下幾個(gè)方面的研究工作：

1)源代碼中無(wú)法顯式表達(dá)軟件系統(tǒng)的非功能屬性(例如周期、執(zhí)行時(shí)間、資源分配等).目前我們正在基于第三方工具(例如WCET分析工具)，測(cè)出軟件執(zhí)行時(shí)間和周期等信息，并將這些屬性添加到相應(yīng)的AADL模型中；

2)在軟件開(kāi)發(fā)過(guò)程中，Assertion是一種經(jīng)典的調(diào)試和測(cè)試方法.在編程中是指對(duì)某種假設(shè)條件進(jìn)行檢測(cè)，如果條件成立就不進(jìn)行任何操作，如果條件不成立就捕捉到這種錯(cuò)誤，并打印出錯(cuò)誤信息，終止程序執(zhí)行.目前我們正在考慮將帶Assertion的C語(yǔ)言轉(zhuǎn)換到AADL Bless Annex[30]，目的是為了對(duì)行為附件進(jìn)行驗(yàn)證；

3)模型轉(zhuǎn)換的正確性是模型驅(qū)動(dòng)開(kāi)發(fā)方法成功的關(guān)鍵，目前我們正在基于模型檢測(cè)工具UPPAAL和組合驗(yàn)證工具 AGREE對(duì)逆向構(gòu)造的AADL模型進(jìn)行形式化驗(yàn)證.