• 
    

    
    

      99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看

      ?

      代碼生成器形式化驗(yàn)證技術(shù)研究

      2021-04-19 01:53:26侯榮彬
      儀器儀表用戶 2021年4期
      關(guān)鍵詞:代碼生成編譯器正確性

      侯榮彬,馬 權(quán),蘭 林,蔣 維,楊 斐,李 昂,李 丹

      (中國(guó)核動(dòng)力研究設(shè)計(jì)院 核反應(yīng)堆系統(tǒng)設(shè)計(jì)技術(shù)重點(diǎn)實(shí)驗(yàn)室,成都 610213)

      0 引言

      在安全關(guān)鍵嵌入式實(shí)時(shí)系統(tǒng)中,軟件可靠性方面的問題越來越突出。為了保證系統(tǒng)的安全,認(rèn)證機(jī)構(gòu)制定系統(tǒng)(系統(tǒng)認(rèn)證)和系統(tǒng)開發(fā)工具(系統(tǒng)開發(fā)工具認(rèn)證資質(zhì))開發(fā)的指導(dǎo)原則。為了降低系統(tǒng)在驗(yàn)證規(guī)范和設(shè)計(jì)方面的成本,開發(fā)過程中通常使用自動(dòng)代碼生成器,以便從規(guī)范和設(shè)計(jì)模型自動(dòng)生成源代碼,然后從源代碼(傳統(tǒng)編譯器)中生成二進(jìn)制可執(zhí)行文件。另外,模型驅(qū)動(dòng)工程技術(shù)的發(fā)展也需要使用代碼生成器,實(shí)現(xiàn)從模型語言到通用編程語言的轉(zhuǎn)化。然而,許多有錯(cuò)誤的代碼生成器,特別是編譯器,它可以把一個(gè)正確的安全程序變成一個(gè)不正確的不安全的可執(zhí)行代碼。因此,應(yīng)該給予代碼生成器的V&V 以更多的關(guān)注。認(rèn)證機(jī)構(gòu)通常要求代碼生成器必須與它生成系統(tǒng)的部分有相同的安全級(jí)別。

      編譯器要求在語義上是透明的:編譯后的代碼應(yīng)該按照源程序的語義所規(guī)定的方式運(yùn)行。然而,編譯器尤其是優(yōu)化編譯器是執(zhí)行復(fù)雜符號(hào)轉(zhuǎn)換的復(fù)雜程序。編譯器中錯(cuò)誤引發(fā)的事故,它們會(huì)悄悄地把正確的源程序變成不正確的可執(zhí)行程序。對(duì)于低可靠性要求的軟件,僅通過測(cè)試驗(yàn)證,編譯器引入的錯(cuò)誤的影響可以忽略不計(jì)。測(cè)試過程驗(yàn)證的是編譯器生成的可執(zhí)行代碼,經(jīng)過嚴(yán)格的測(cè)試可發(fā)現(xiàn)源程序的錯(cuò)誤。對(duì)于高可靠性要求軟件,這一問題變得至關(guān)重要,需要使用形式化方法(模型檢查、程序驗(yàn)證等)來保證。使用形式化方法進(jìn)行驗(yàn)證幾乎都是在源代碼級(jí)別,編譯器中的漏洞會(huì)將這些經(jīng)過驗(yàn)證的源程序轉(zhuǎn)化為可執(zhí)行程序。如果編譯器中存在錯(cuò)誤,則可能使在源程序上的形式化驗(yàn)證失效。從形式化方法的角度看,編譯器是源程序與硬件處理器之間的一個(gè)薄弱環(huán)節(jié),而后者已經(jīng)被形式化驗(yàn)證。安全關(guān)鍵軟件行業(yè)意識(shí)到了這個(gè)問題,并使用了各種技術(shù)來緩解這個(gè)問題,例如在關(guān)閉所有編譯器優(yōu)化之后對(duì)生成的匯編代碼進(jìn)行手動(dòng)代碼審查。然而,這些技術(shù)并不能完全解決這個(gè)問題,并且在開發(fā)時(shí)間和程序性能方面代價(jià)高昂。更好的方法是將形式化方法應(yīng)用于編譯器本身,以確保它保留源程序的語義。顯然,更好的方法是將形式化方法應(yīng)用于編譯器本身,以確保它保留源程序的語義。目前,已經(jīng)有很多方法和相關(guān)研究,包括書面、機(jī)器上的語義保持證明[1-3]、證明攜帶代碼[4-8]、可信編譯[9-11]、翻譯確認(rèn)[12-19]。

      1 代碼生成器形式化驗(yàn)證方法

      編譯器的形式化驗(yàn)證就是證明源程序S 和目標(biāo)程序C之間滿足給定的正確性屬性Prop(S, C)。正確性屬性包括:

      I. S 和C 在可觀測(cè)行為上是等價(jià)的。

      II. 如果S 有良好定義的語義(不出錯(cuò)),那么S 和C是可觀測(cè)行為等價(jià)的。

      III. 如果S 有良好定義的語義并且滿足功能屬性Spec,那么C 滿足Spec。

      IV. 如果S 是類型和內(nèi)存安全的,那C 也是。

      V. C 是類型和內(nèi)存安全的。

      對(duì)于可信代碼生成器的正確性屬性,選擇第2 種。理由如下:完全可觀測(cè)行為等價(jià)(性質(zhì)I)太強(qiáng),它要求當(dāng)源代碼語義發(fā)生錯(cuò)誤時(shí),編譯生成的目標(biāo)代碼也會(huì)出錯(cuò)。在實(shí)踐中,編譯器可以為具有未定義行為的源程序自由地生成任意代碼。因此,這個(gè)屬性很難證明。通常情況下,如果規(guī)范Spec 依賴于程序的可觀察行為,則規(guī)范的保持性(屬性III)由屬性II 蘊(yùn)含。因此,一勞永逸地證明屬性II,可滿足很多屬性III 中的規(guī)范。屬性IV 是典型的類型保持編譯器,只是屬性III 的一個(gè)實(shí)例。最后,屬性V 是一個(gè)與源程序無關(guān)的屬性,這是一種典型的編譯器,要么直接在編譯器代碼上建立感興趣的屬性(類型安全),要么在源程序上建立感興趣的屬性,并在編譯過程中保存這一屬性。

      一個(gè)編譯器Comp 是一個(gè)從源程序到編譯生成的代碼(記作Comp(S) = Some(C))或錯(cuò)誤(記作:Comp(S) = None)的全函數(shù)。錯(cuò)誤的情況必須考慮,因?yàn)榫幾g器可能生成代碼失敗。例如,源程序有語法或類型錯(cuò)誤、編譯的程序超出了編譯器的能力。

      1)經(jīng)過驗(yàn)證的編譯器

      使用上面的定義,一個(gè)經(jīng)過驗(yàn)證的編譯器是任何完成下面定理的形式化證明的編譯器Comp:

      換句話說,要么編譯器報(bào)告錯(cuò)誤,要么生成滿足所需正確性的屬性的代碼。注意,當(dāng)Comp(S) = None 時(shí),這一規(guī)則也同樣成立。編譯器是否成功地編譯感興趣的源程序不是一個(gè)正確性問題,而是一個(gè)編譯器實(shí)現(xiàn)質(zhì)量問題,這是由諸如測(cè)試之類非形式化方法解決的。從形式化方法的觀點(diǎn)來看,重點(diǎn)是編譯器從不默默地產(chǎn)生錯(cuò)誤的代碼。

      2)攜帶證明的代碼

      攜帶證明代碼和可信編譯使用驗(yàn)證編譯器,它可以生成代碼失?。–Comp(S) = None)或返回一個(gè)編譯產(chǎn)生的C代碼和屬性Prop(S, C)的證明π(CComp(S) = Some(C,π))。證明π可以被使用者獨(dú)立檢查。這種方法沒有必要相信代碼產(chǎn)生者,也不需要驗(yàn)證代碼生成器本身。驗(yàn)證編譯器可以產(chǎn)生正確的證明π,而不是建立Prop(S, C)。

      3)翻譯確認(rèn)

      在翻譯確認(rèn)方法中,標(biāo)準(zhǔn)的編譯器Comp 還輔助于一個(gè)驗(yàn)證器:一個(gè)布爾值函數(shù)Verif(S, C)通過靜態(tài)分析S 和C來驗(yàn)證屬性Prop(S, C)。為獲得形式化保證,驗(yàn)證器自身必須被驗(yàn)證,也就是必須證明:

      然而,這種方法不需要對(duì)編譯器本身進(jìn)行形式化驗(yàn)證。因此,不能保證編譯器產(chǎn)生的代碼總是能夠通過驗(yàn)證器。

      4)混合方法:結(jié)合經(jīng)過驗(yàn)證的編譯器和驗(yàn)證編譯器

      通過重新組合,可以形式化地結(jié)合經(jīng)過驗(yàn)證的編譯器方法和驗(yàn)證編譯器。如果CComp 是一個(gè)驗(yàn)證編譯器并且Verif 是一個(gè)正確的驗(yàn)證器,那么下面的函數(shù)是一個(gè)經(jīng)過驗(yàn)證的編譯器。定理(1)可以直接從定理(2)獲得。

      Comp(S) =

      match CComp(S) with

      |None ->None

      |Some(C, A) -> if Verif(S, C, A) then Some(C)

      else None

      類似地,設(shè)Comp 是一個(gè)經(jīng)過驗(yàn)證的編譯器并且Π 是一個(gè)定理(1)的Coq 證明項(xiàng)。根據(jù)Curry-Howard 同構(gòu)機(jī)制,Π 是一個(gè)函數(shù)包括S,C 和一個(gè)Comp(S) = Some (C)的證明,并且返回一個(gè)Prop(S, C)的證明。一個(gè)驗(yàn)證編譯器定義如下:

      CComp(S) =

      match Comp(S) with

      | None -> None

      |Some(C) -> Some(C, Π S Cπeq)

      其中,πeq 是命題Comp(S) = Some(C)的證明項(xiàng)。伴隨的驗(yàn)證器是Coq 證明檢查器,就像是攜帶證明代碼方法一樣。

      5)編譯過程的組合性

      編譯器通常由很多階段組成,這些階段之間通過中間語言進(jìn)行連接。上面提到的兩種編譯器構(gòu)造方法,經(jīng)過驗(yàn)證的編譯器和驗(yàn)證編譯器都可以通過這種方式進(jìn)行分解。如 果Comp1 和Comp2 分 別 是 從L1 到L2 和L2 到L3 的 經(jīng)過驗(yàn)證的編譯器,他們的組合:

      Comp(S) =

      match Comp1(S) with

      | None -> None

      | Some(I) -> Comp2(I)

      假設(shè)屬性Prop 是可傳遞性的,那么Comp 是一個(gè)從L1到L3 的經(jīng)過驗(yàn)證的編譯器。也就是Prop(S, I)和Prop(I, C)蘊(yùn)含Prop(S, C)。

      相似地,如果CComp1 和CComp2 分別是L1 到L2 和L2 到L3 的驗(yàn)證編譯器,Verif1 和Verif2 是伴隨的驗(yàn)證器,那么一個(gè)從L1 到L3 的驗(yàn)證編譯器為:

      CComp(S) =

      match CComp1(S) with

      |None ->None

      |Some(I, A1) ->

      match CComp2(I) with

      |None->None

      |Some(C, A2)->Some(C, (A1 ,I, A2))

      Verif(S, C, (A1, I, A2)) = Verif1(S, I, A1)/Verif2(I, C, A2)

      2 代碼生成器正確性定義

      編譯階段的語義正確性是根據(jù)形式化源語言和目標(biāo)語言的模擬關(guān)系來定義。上面已經(jīng)介紹了4 種正確性屬性,其中最重要的是編譯過程的語義保持性(屬性II),這種屬性由向前模擬關(guān)系來實(shí)現(xiàn)。編譯器正確性的核心是確定計(jì)算與編譯交互的精確定義。對(duì)于一個(gè)編譯階段的源語言Src和目標(biāo)語言Tgt,可以通過向前模擬關(guān)系實(shí)現(xiàn)編譯器正確性的定義,如圖1 所示。

      其中:

      1)編譯過程Src →Tgt 沿水平方向演變,從左到右。

      2)程序執(zhí)行過程垂直方向,從上到下。

      3)兩種語言的狀態(tài)分別為σ_Src 和σ_Tgt。其中,σ_Src = (c1, m1),σ_Tgt=(c2, m2)。c1 和c2 分別是源語言和目標(biāo)語言的語句,并且這兩種語言具有獨(dú)立的內(nèi)存。

      4)過程→是程序的執(zhí)行方向,根據(jù)編程語言的小步語義關(guān)系σ→σ'或多步語義σ→nσ'確定。

      5)水平關(guān)系采用二元匹配關(guān)系的形式,它將源語言狀態(tài)與目標(biāo)語言狀態(tài)相關(guān)聯(lián),并且在執(zhí)行過程中保持這一關(guān)系。

      圖1 向前模擬關(guān)系示意圖Fig.1 Diagram of forward simulation relationship

      圖2 模擬關(guān)系傳遞組合性示意圖Fig.2 Schematic diagram of simulation relationship transfer combination

      為了更清楚地表示程序運(yùn)行的各種情況,匹配關(guān)系(c1,m1)→(c2,m2)蘊(yùn)含如下命題:

      a)如果c1, m1 →Src c1',m1',那么存在c2' 和m2' 使得c2, m2 →Tgtn c2', m2',并且(c1', m1')→(c2', m2')。

      b)如果c1 終止,那么c2 終止,并且返回值和內(nèi)存都滿足匹配關(guān)系。

      c)如果是函數(shù)調(diào)用語句c1 = (f, a1 →) , c2 = (f, a2 →),要求執(zhí)行前參數(shù)列表a1 →~ a2 →,并且m1~m2,執(zhí)行完畢后返回值和更新后內(nèi)存滿足匹配關(guān)系。

      對(duì)于真實(shí)的編譯器,編譯器的正確性證明必須沿著編譯過程的各個(gè)階段可傳遞性的組合。通過這種方式每個(gè)階段可以相互獨(dú)立地進(jìn)行證明,然后將這些證明串聯(lián)起來。這明顯比單塊地證明編譯器是正確的更加模塊化,并且簡(jiǎn)化了證明難度。

      沿著編譯過程的模擬關(guān)系的可傳遞組合性可以通過圖2 進(jìn)行表示。

      3 編程語言語法

      圖3 Lustre 和C語言抽象語法Fig.3 Lustre and C language abstract syntax

      Lustre 是一種廣泛應(yīng)用于嵌入式控制和信號(hào)處理系統(tǒng)的面向應(yīng)用的編程語言。著名的SCADE[20]和Simulink[21]都是基于Lustre,將Lustre 轉(zhuǎn)換為可執(zhí)行代碼。SCADE 廣泛應(yīng)用于航空控制和反應(yīng)堆監(jiān)視軟件開發(fā)中。Lustre 的主要特征包括:易于構(gòu)建反應(yīng)式控制;程序的執(zhí)行有靜態(tài)有界的空間和時(shí)間;具有基于數(shù)據(jù)流的良好數(shù)學(xué)語義;可追溯和模塊編譯框架;可實(shí)現(xiàn)自動(dòng)化程序驗(yàn)證。Lustre 的抽象語法如圖3 所示,這些抽象語法都是通過遞歸定義的。在表達(dá)式層,可分為一般表達(dá)式,如變量、常量、一元操作表達(dá)式、二元操作表達(dá)式、時(shí)鐘運(yùn)算表達(dá)式等;控制表達(dá)式,如條件表達(dá)式;時(shí)鐘表達(dá)式,如基本時(shí)鐘、子時(shí)鐘。在語句層,Lustre 只有等式語句,等式的類型包括一般賦值、延時(shí)賦值、函數(shù)調(diào)用。一個(gè)完整的Lustre 程序是類型聲明、函數(shù)聲明和主函數(shù)調(diào)用的集合。對(duì)于C 語言,大家都比較熟悉,其抽象語法如右半部分所示,其結(jié)構(gòu)和Lustre 很類似,不再贅述。

      4 Lustre和C語義一致性的定義

      如圖4 所示,Lustre 語言到C 語言的翻譯過程的語義保持性,實(shí)際上就是在相同的初始狀態(tài)下,接受相同的輸入,分別執(zhí)行各自程序的語義,程序執(zhí)行完畢后,最終的狀態(tài)滿足匹配關(guān)系,并且在最終狀態(tài)中查找到相同的程序輸出值。源語言Luster 和目標(biāo)語言C 之間通過一個(gè)轉(zhuǎn)換函數(shù)Comp 建立聯(lián)系。只要完成Lustre 語言到C 語言的語義保持性證明,也就間接證明源語言Lustre 和經(jīng)過Comp 處理生成的C 之間滿足語義保持性。語義保持性證明基于編程語言的操作語義和狀態(tài)的匹配關(guān)系以及程序和環(huán)境的交互。操作語義是一種基于狀態(tài)轉(zhuǎn)換關(guān)系的推理規(guī)則,匹配關(guān)系表示兩個(gè)環(huán)境中標(biāo)識(shí)符和值之間的對(duì)應(yīng)和相等關(guān)系。程序和環(huán)境的交互關(guān)系較為復(fù)雜如圖5 所示。根據(jù)程序的語法結(jié)構(gòu),程序執(zhí)行語義分為類型和函數(shù)聲明語句與主函數(shù)的調(diào)用,主函數(shù)的調(diào)用是函數(shù)調(diào)用的一個(gè)實(shí)例,函數(shù)調(diào)用又分為局部變量聲明和語句執(zhí)行,語句的執(zhí)行實(shí)際就是控制表達(dá)式的求值。其中,聲明類語句,如類型、函數(shù)聲明語句和變量聲明語句會(huì)創(chuàng)建新的環(huán)境和標(biāo)識(shí)符,申請(qǐng)新的內(nèi)存塊??刂祁愓Z句如函數(shù)調(diào)用、語句執(zhí)行、表達(dá)式求值則會(huì)更新狀態(tài),改變標(biāo)識(shí)符對(duì)應(yīng)的值或內(nèi)存空間。求值類語句,則會(huì)根據(jù)當(dāng)前的狀態(tài)來確定自身的值。

      圖4 程序執(zhí)行一致性的定義Fig.4 Definition of program execution consistency

      圖5 程序和環(huán)境的交互關(guān)系Fig.5 Interaction between program and environment

      5 結(jié)束語

      本文針對(duì)一種Lustre 到C 的代碼生成器,準(zhǔn)備采用形式化方法對(duì)其翻譯過程的語義保持性進(jìn)行證明。第一部分介紹了應(yīng)用形式化驗(yàn)證技術(shù)構(gòu)建代碼生成器的方法,包括經(jīng)過驗(yàn)證的編譯器、驗(yàn)證編譯器、翻譯確認(rèn)、混合方法,以及將翻譯階段分解組合的技術(shù);第二部分介紹了語義保持性定義的方法即單向模擬理論;第三部分介紹了源語言Lustre 和目標(biāo)語言C 的抽象語法;第四部分定義了Lustre到C 翻譯過程的語義保持性,將前面的理論應(yīng)用于實(shí)際翻譯過程的定義中,并詳細(xì)介紹了程序和語言狀態(tài)之間的交互。這是程序操作語義的基礎(chǔ),而操作語義又是語義保持性證明的基礎(chǔ)。本論文為后續(xù)實(shí)際代碼生成器的開發(fā)提供理論指導(dǎo),也是后續(xù)代碼生成器形式化語義保持性定義的依據(jù)。

      猜你喜歡
      代碼生成編譯器正確性
      Lustre語言可信代碼生成器研究進(jìn)展
      基于相異編譯器的安全計(jì)算機(jī)平臺(tái)交叉編譯環(huán)境設(shè)計(jì)
      一種基于系統(tǒng)穩(wěn)定性和正確性的定位導(dǎo)航方法研究
      淺談如何提高水質(zhì)檢測(cè)結(jié)果準(zhǔn)確性
      代碼生成技術(shù)在軟件開發(fā)中的應(yīng)用
      電子世界(2016年15期)2016-08-29 02:14:28
      基于XML的代碼自動(dòng)生成工具
      電子科技(2015年2期)2015-12-20 01:09:20
      雙口RAM讀寫正確性自動(dòng)測(cè)試的有限狀態(tài)機(jī)控制器設(shè)計(jì)方法
      通用NC代碼編譯器的設(shè)計(jì)與實(shí)現(xiàn)
      基于關(guān)系數(shù)據(jù)模型代碼生成器的設(shè)計(jì)與實(shí)現(xiàn)
      編譯器無關(guān)性編碼在微控制器中的優(yōu)勢(shì)
      曲阳县| 绵阳市| 新龙县| 永川市| 弋阳县| 古浪县| 游戏| 五莲县| 望都县| 阿图什市| 醴陵市| 锡林郭勒盟| 辽中县| 浙江省| 镶黄旗| 于田县| 临沧市| 惠州市| 宿迁市| 兴和县| 西华县| 海城市| 台北市| 平塘县| 株洲市| 常德市| 察隅县| 华坪县| 略阳县| 镇雄县| 沙坪坝区| 富川| 桂东县| 固阳县| 潼南县| 久治县| 清涧县| 民勤县| 平利县| 望江县| 杭锦后旗|