軟件學(xué)報安全攸關(guān)軟件系統(tǒng)建模與驗證專題

1、軟件學(xué)報安全攸關(guān)軟件系統(tǒng)建模與驗證專題文章整體分類1基于形式化方法的航空電子系統(tǒng)檢測 方法：模型檢測 質(zhì)量：一致性系統(tǒng)結(jié)構(gòu)設(shè)計的資源是否滿足需求中性能指標(biāo)的配置要求，即：系統(tǒng)結(jié)構(gòu)對應(yīng)的資源能否滿足配置（靜態(tài)檢測）；可用性系統(tǒng)的執(zhí)行環(huán)境是否能保證系統(tǒng)任務(wù)的正常執(zhí)行（動態(tài)檢測）。 模型：系統(tǒng)結(jié)構(gòu)、資源、任務(wù)的形式化建模 檢測標(biāo)準(zhǔn)：一致性a.配置文件一致性：軟件配置項是否滿足需求（不同級別配置文件是否一致）；b.系統(tǒng)環(huán)境狀態(tài)適配性（環(huán)境即資源，當(dāng)前狀態(tài)能否滿足性能指標(biāo)）。可用性生成的“檢測用例”。 實例：航空電子系統(tǒng)仿真平臺基于形式化方法的航空電子系統(tǒng)檢測航空電子系統(tǒng)靜態(tài)建模1. API：輸入/輸出

2、+約束；2. 性能指標(biāo)PI：資源屬性名+數(shù)量；3. 配置文件CONF：文件屬性+屬性值；4. 軟件配置項CSCI：1+2+3；5. 分系統(tǒng)SS：1+2+3+4；6. 航空電子系統(tǒng)ES：1+2+3+5.功能建模組件關(guān)系建?；谛问交椒ǖ暮娇针娮酉到y(tǒng)檢測 動態(tài)建模：窗口樹、任務(wù)執(zhí)行過程狀態(tài)圖基于形式化方法的航空電子系統(tǒng)檢測 檢測過程2基于時間抽象狀態(tài)機的AADL模型驗證 方法：模型檢測 實際工作：AADL（系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言）TASM（時間抽象狀態(tài)機） 質(zhì)量：依賴于TASM Toolset和UPPAAL 模型：AADL圖形化模型 檢測標(biāo)準(zhǔn)：任務(wù)的參數(shù)描述（表格） 實例：導(dǎo)航、制導(dǎo)與控制系

3、統(tǒng)GNC的AOCS子系統(tǒng)（控制計算機/姿勢與軌道控制系統(tǒng)） 工具：AADL2TASM基于時間抽象狀態(tài)機的AADL模型驗證 思路：1.分別對AADL和TASM語法進(jìn)行抽象，然后給出映射關(guān)系，并基于ML的元語言形式定義2者的轉(zhuǎn)換語義規(guī)則；2.系統(tǒng)AADL建模AADL2TASMTASM ToolSet分析完整性、一致性、時間行為和資源行為仿真UPPAAL檢測死鎖、安全性、活性、實時性。3基于時間STM的軟件形式化建模與驗證方法 方法：模型檢測 質(zhì)量：可信性（時間和邏輯屬性） 模型：TSTM給STM加了時間和語義約束（STM狀態(tài)遷移矩陣，一種基于表結(jié)構(gòu)的狀態(tài)機建模方法，前端為表格形式，后端是嚴(yán)格的形式

4、化定義） 檢測標(biāo)準(zhǔn)：用時序邏輯語言TCLT定義的所需滿足的性質(zhì)。 實例：列車控制系統(tǒng)3基于時間STM的軟件形式化建模與驗證方法 本文方法：1.軟件TSTM建模，刻畫軟件的行為特征；2.屬性的TCTL描述3.檢測方法：基于界限模型檢測（BMC）技術(shù)的時間計算樹邏輯（TCTL）模型檢測方法模型和待驗證屬性的否定形式進(jìn)行合取，構(gòu)建BMC公式，BMC公式的求解問題歸約為邏輯公式的可滿足性判定，即：SAT/SMT實例。4設(shè)備驅(qū)動程序可靠性和正確性保障方法與技術(shù)研究進(jìn)展 綜述性論文 質(zhì)量：驅(qū)動程序的可靠性和正確性。 程序故障隔離與恢復(fù)、正確性分析和驗證、設(shè)計建模與復(fù)雜性控制。5基于數(shù)據(jù)鏈的軟件故障定位方法

5、 方法：代碼分析 質(zhì)量：程序的數(shù)據(jù)流相關(guān)的邏輯故障定位（程序設(shè)計邏輯故障，定位到方法內(nèi)的代碼） 模型：數(shù)據(jù)鏈每個變量上的定義操作狀態(tài)軌跡及其之間的依賴關(guān)系。 分析對象：程序代碼 檢測方法：1.先用現(xiàn)有方法將邏輯故障定位到方法；2.再用本文方法中方法內(nèi)定為變量故障疑似度分析：a.對故障疑似方法建立數(shù)據(jù)鏈；b.用a的數(shù)據(jù)鏈構(gòu)建概率數(shù)據(jù)鏈模型。c.疑似度排序 實驗對比6一種面向列車控制系統(tǒng)中安全攸關(guān)場景的測試用例自動生成方法 本文工作：擴展了活動圖，加入了a.事件驅(qū)動機制；b.時間約束. 覆蓋準(zhǔn)則：a.循環(huán)只執(zhí)行一次；b.不同的并發(fā)分支并發(fā)執(zhí)行（同時向前執(zhí)行一步）；c.所有簡單路徑被覆蓋（從a、b兩

6、條準(zhǔn)則得到的活動圖執(zhí)行路徑）。 本文測試用例生成方法：1.擴展活動圖建模，并找出其中的簡單路徑；2.明確被測系統(tǒng)的邊界；3.執(zhí)行簡單路徑，并沿路收集外部環(huán)境向被測系統(tǒng)發(fā)送的事件，作為測試輸入，被測系統(tǒng)向外部環(huán)境的輸出作為結(jié)果序列。4.測試用例=環(huán)境傳給被測系統(tǒng)的信息（特定時間）+被測系統(tǒng)的觀察結(jié)果+時間上需滿足的約束。 實例：地鐵列車控制系統(tǒng)7多處理器實時系統(tǒng)可調(diào)度分析的UPPAAL模型 方法:模型檢測 （偏硬件，主要數(shù)UPPAAL的使用） 質(zhì)量：可調(diào)度性系統(tǒng)必須滿足的時間要求。 模型：UPPAAL模型 性質(zhì)：時間自動機建?？烧{(diào)度性相關(guān)的模塊（實時任務(wù)、運行平臺、調(diào)度管理） 檢測：UPPAAL

7、檢測 實驗：對象智能手機GSM系統(tǒng)的21個任務(wù) 本文貢獻(xiàn)：給出了多處理器實時系統(tǒng)可調(diào)度分析的模板8多分支單變量循環(huán)程序的終止性分析 方法：代碼分析 質(zhì)量：帶多個分支的單變量循環(huán)程序的終止性問題（系統(tǒng)中有無死循環(huán)，是正確性的基礎(chǔ)）（可信計算） 主要結(jié)果： 稱由迭代函數(shù) F 和循環(huán)條件形成的區(qū)域 I 所構(gòu)成的循環(huán)程序 P(F,I)在實數(shù)域是不可終止的,如果存在一點 x0,使得 ( ) F x I i 0 0 i+ = .這里,Fi=FDFDDF 表示函數(shù)的復(fù)合.如果那樣的 x0 不存在,則稱循環(huán)P(F,I)在實數(shù)域上可終止. 定理 1. 令 f :R6R 為一維連續(xù)映射.I 為一閉區(qū)間.循環(huán)程序P

8、1 While xI dox:=f(x)是不可終止的充分必要條件為迭代映射是不可終止的充分必要條件為迭代映射 f 在閉區(qū)間在閉區(qū)間 I 上有不動點上有不動點. 實例實例 應(yīng)用應(yīng)用： 對多分支單變量多項式循環(huán)程序，可通過實代數(shù)工具驗證定理中條件是否成立；對多分支單變量多項式循環(huán)程序，可通過實代數(shù)工具驗證定理中條件是否成立； 判定不動點是否落入到循環(huán)條件形成的區(qū)域問題，可轉(zhuǎn)為半代數(shù)系統(tǒng)，通過實代數(shù)工具求解。判定不動點是否落入到循環(huán)條件形成的區(qū)域問題，可轉(zhuǎn)為半代數(shù)系統(tǒng)，通過實代數(shù)工具求解。9面向安全攸關(guān)系統(tǒng)中小概率事件的統(tǒng)計模型檢測 方法：基于機器學(xué)習(xí)的統(tǒng)計模型檢測算法統(tǒng)計模型檢測SMC評估系統(tǒng)模型

9、滿足屬性約束的概率區(qū)間機器學(xué)習(xí)（用于生成更多樣本） 質(zhì)量：可靠性（在相對較少的樣本數(shù)量下，預(yù)測、評估小概率事件的發(fā)生概率） 本文框架：輸入：a.目標(biāo)系統(tǒng)的可執(zhí)行模型（隨機混成自動機模型SHA）；b.屬性約束的概率有界線性時態(tài)邏輯（PBLTL公式）；c.統(tǒng)計精度參數(shù)。輸出：在有限的資源約束下，系統(tǒng)模型a滿足屬性約束b的概率區(qū)間。2個模塊：學(xué)習(xí)型模型檢測器+自適應(yīng)統(tǒng)計分析器 實例：基于通信的列車控制系統(tǒng)學(xué)習(xí)型模型檢測器學(xué)習(xí)型模型檢測器輸入：系統(tǒng)模型a+有界線性時態(tài)邏輯公式輸出：用經(jīng)典模型檢測算法判斷單個樣本trace是否滿足屬性約束，得到統(tǒng)計分析樣本Trace分割與特征提取分割與特征提取目的：找到

10、一個合適的時間點,使其前段 Trace 在盡可能短的條件下最大程度地包含對預(yù)測有用的信息,以便 SVM 預(yù)測后段 Trace 的信息.思想：條件概率。假設(shè)在 A 事件發(fā)生的情況下,B 事件更有可能發(fā)生,如果 P(A)P(B),則先在模擬Trace 的過程中找到 A 事件的發(fā)生點,在此前提下向后進(jìn)行多次模擬,以提高捕獲到 B 事件的可能性.基于屬性約束和隨機行為的特征提取方法：1.確定需要提取的特征變量;2.根據(jù)特征變量提取訓(xùn)練集中 Trace 的具體特征.SVM:機器學(xué)習(xí)模型，用于預(yù)測生成新的樣本。如果樣本可信，則使用預(yù)測結(jié)果，并開始下一次模擬；不可信，則進(jìn)入后段仿真器，模擬出完整的Trace

11、，檢測其結(jié)果。自適應(yīng)統(tǒng)計分析器自適應(yīng)統(tǒng)計分析器將的結(jié)果作為統(tǒng)計分析樣本，執(zhí)行統(tǒng)計模型檢測，判定現(xiàn)有樣本是否滿足精度要求，滿足這結(jié)束，否則返回生成更多樣本trace.SPRT順序概率比檢驗；BHT貝葉斯假設(shè)檢驗；BIET貝葉斯區(qū)間估計檢驗。10面向航天嵌入式軟件的形式化建模方法 研究對象：周期性控制系統(tǒng)的需求獲取、表示、分析驗證 方法：模型檢測（分析所建的需求模型） 本文思路：1.航天需求描述語言SPARDL形式化建模方法用一系列模式來體現(xiàn)嵌入式控制系統(tǒng)的行為特征，每個模式可以周期性地執(zhí)行一系列過程。核心是模式圖，描述模式和模式間的變遷。2.時序性表示給出了ITL（基于區(qū)間邏輯的性質(zhì)規(guī)范語言）性

12、質(zhì)模板。3.從SPARDL自動生成C代碼（給了原理），并快速仿真。 實例：某深空探測信號軟件，用于鉆探取土（沒有給出任何數(shù)據(jù)）個人：SPARDL數(shù)用于描述需求的2層語言，上層是模式圖，下層是對應(yīng)的形式化描述。概率模型檢測概率模型檢測概率模型檢查把性質(zhì) p 在模型的一次執(zhí)行(一條路徑)上是否成立視為一個服從兩項分布的隨機變量.概率模型檢查主要考慮以下兩個問題:給定模型 M 和性質(zhì) p,1) 估算在模型 M 的任意一條路徑 t 上,p 成立的可能性,即參數(shù)估計;2) 判斷上述可能性是否大于給定的閾值,即假設(shè)檢驗.11同步數(shù)據(jù)流語言高價運算消去的可信翻譯兩種語言差距較大：Luster*有時鐘同步、數(shù)

13、據(jù)流、并發(fā)及數(shù)據(jù)流對象，其變量和表達(dá)式都表示一個流數(shù)據(jù)（給定類型的值序列+一個時鐘）；Clight有順序控制流特征。高階運算：一個對數(shù)組或輸入?yún)?shù)列表進(jìn)行循環(huán)計算的過程。12一種基于特征矩陣的軟件脆弱性代碼克隆檢測方法 方法：代碼檢測 質(zhì)量：脆弱性（如緩沖區(qū)溢出、內(nèi)存多次釋放、指針誤用等） 本文思想：建立一個已發(fā)現(xiàn)的脆弱性代碼數(shù)據(jù)庫,從代碼的相似度層面進(jìn)行檢測,查找某個軟件系統(tǒng)出現(xiàn)的脆弱性代碼在其他軟件中的分布情況,就可以檢測出更多的脆弱點.提出多類脆弱性檢測模型模型CVdetector 實驗數(shù)據(jù)對比10 維向量(stmtexp,decl,incr,cond,assign,mul,add,fun_call,fname,fpara)13一個及其檢測的Micro-Dalvik虛擬機模型 形式化虛擬機模型，對指令集和運行時狀態(tài)進(jìn)行了形式化，然后推理證明該虛擬機的正確性。14信息物理融合系統(tǒng)控制軟件的統(tǒng)計模型檢驗 方法：模型檢測 質(zhì)量：系統(tǒng)功能的正確性 本文內(nèi)容：基于時間自動機，模塊化描述實時多任務(wù)系統(tǒng)，然后提出一種利用統(tǒng)計模型檢驗技術(shù)，分析系統(tǒng)功能正確性。 模型：調(diào)度器、周期性任務(wù)、偶發(fā)任務(wù)、的時間自動機模型。 檢測標(biāo)準(zhǔn)：人工分析出的錯誤條