• <tr id="yyy80"></tr>
  • <sup id="yyy80"></sup>
  • <tfoot id="yyy80"><noscript id="yyy80"></noscript></tfoot>
  • 99热精品在线国产_美女午夜性视频免费_国产精品国产高清国产av_av欧美777_自拍偷自拍亚洲精品老妇_亚洲熟女精品中文字幕_www日本黄色视频网_国产精品野战在线观看 ?

    操作系統(tǒng)形式化驗證綜述

    2021-10-12 10:09:10錢漢偉王承毅
    關(guān)鍵詞:精化編譯器正確性

    錢漢偉,王承毅

    (1.江蘇警官學(xué)院計算機(jī)信息與網(wǎng)絡(luò)安全系,江蘇 南京 210031; 2.江蘇科技大學(xué)理學(xué)院,江蘇 鎮(zhèn)江 212003)

    計算機(jī)軟件與人們生活密切相關(guān),從網(wǎng)絡(luò)、手機(jī)等日常通信設(shè)備到能源、國防等關(guān)鍵基礎(chǔ)設(shè)施,幾乎無處不在。另一方面,由于缺少有效手段控制軟件質(zhì)量,使得軟件的漏洞或錯誤幾乎不可避免。每年由于軟件的漏洞或者錯誤導(dǎo)致的損失達(dá)上百億美元。操作系統(tǒng)是所有軟件的基礎(chǔ)平臺,嚴(yán)格保證其可靠性和安全性具有重要價值。目前已知技術(shù)中,只有形式化方法能夠保證軟件不會出錯,但是由于操作系統(tǒng)復(fù)雜度大、并發(fā)度高等問題,其形式化驗證一直以來都是一件非常困難的工作。

    隨著定理證明助手等形式化驗證工具功能更加強(qiáng)大,CertiKOS[1]形式化驗證理論和框架更加完善,操作系統(tǒng)的形式化設(shè)計和驗證工作進(jìn)入一個新階段,并且取得了一系列重要成果。如seL4等操作系統(tǒng)軟件的內(nèi)核功能正確性和無內(nèi)存泄漏等性質(zhì)均得到了有效證明。本文對近年來操作系統(tǒng)形式化驗證技術(shù)、方法和研究進(jìn)展進(jìn)行總結(jié),闡述操作系統(tǒng)形式化驗證過程中對形式化驗證新技術(shù)和方法的應(yīng)用,分析當(dāng)前操作系統(tǒng)形式化驗證存在的問題,展望操作系統(tǒng)形式化驗證未來的發(fā)展方向。

    1 形式化驗證技術(shù)

    1.1 支撐理論和框架

    目前操作系統(tǒng)的形式化驗證是用定理證明的方法對操作系統(tǒng)的性質(zhì)規(guī)約進(jìn)行驗證。其中,Hoare邏輯[2]是性質(zhì)規(guī)約描述的邏輯基礎(chǔ),當(dāng)前驗證工作廣泛使用的分離邏輯[3]、并發(fā)分離邏輯[4]和并發(fā)精化程序邏輯[5](CSL-style relational program logic,CSL-R)等均是以Hoare邏輯為基礎(chǔ)進(jìn)行的擴(kuò)展?;魻栠壿嬜C明規(guī)約用形如“{Pre}P{Post}”的Hoare三元組表示,通過前置條件和后置條件,比如某些不變量,放入程序要證明的性質(zhì),實現(xiàn)了用一組公理和一組規(guī)則描述程序代碼應(yīng)有的性質(zhì)。分離邏輯對霍爾邏輯進(jìn)行了擴(kuò)展,增加了分離合取和分離蘊含謂詞及相應(yīng)的推導(dǎo)規(guī)則,能夠以自然的方式描述計算過程中內(nèi)存的屬性和相關(guān)操作,驗證指針程序也更加方便。并發(fā)精化程序邏輯將并發(fā)分離邏輯的斷言語言擴(kuò)展為關(guān)系型斷言,更適合證明與多級中斷有關(guān)的并發(fā)程序的上下文精化關(guān)系。數(shù)據(jù)精化的概念最早由Back[6]提出,Morgan[7]發(fā)展了類似的一種精化方法。Roever等[8]詳細(xì)論述了數(shù)據(jù)精化證明方法。實際上,操作系統(tǒng)驗證問題也是精化驗證問題,操作系統(tǒng)從底層模型到高層規(guī)約之間的一致性驗證等問題都是以精化理論為基礎(chǔ)。攜帶證明代碼(proof carrying code,PCC)[9]將Hoare邏輯應(yīng)用到匯編語言的安全性質(zhì)檢驗中,可執(zhí)行代碼和證明捆綁傳遞的方式為證明連接提供了可能性?;A(chǔ)性攜帶證明的代碼(foundational proof-carrying code,F(xiàn)PCC)[10]將攜帶證明代碼與復(fù)雜的推理系統(tǒng)都形式化在一個底層的基礎(chǔ)邏輯中,推理系統(tǒng)的可靠性可以用基礎(chǔ)邏輯保證,可進(jìn)一步縮小信任基(trusted base)。在基礎(chǔ)性攜帶證明代碼的基礎(chǔ)上進(jìn)一步提出的開放邏輯框架[11](open certified assembly programming,OCAP)則可以將操作系統(tǒng)軟件不同模塊的驗證邏輯結(jié)合起來,形成完整的驗證系統(tǒng),極大地保證驗證框架的可擴(kuò)展性,為操作系統(tǒng)模塊化驗證提供了理論基礎(chǔ)。

    1.2 形式化驗證工具

    工具在降低操作系統(tǒng)自動化驗證難度、提高驗證開發(fā)的效率等方面起著重要作用。操作系統(tǒng)的驗證問題都將轉(zhuǎn)成定理證明問題,解決定理證明問題最終依賴于定理證明器。目前廣泛應(yīng)用于操作系統(tǒng)驗證的定理證明器有Z3[12]、Isabelle[13]和Coq[14]等。Z3是微軟著名的自動定理證明器,能夠?qū)︱炞C條件進(jìn)行自動證明。由于大部分證明性質(zhì)的不可判定性,自動定理證明器只能證明有限的性質(zhì),更多的證明則要依賴于人機(jī)交互式定理證明器,如Isabelle和Coq等。Isabelle是由英國劍橋大學(xué)Paulson和德國慕尼黑技術(shù)大學(xué)Nipkow于1986年共同開發(fā)的基于高階邏輯的證明器。Isabelle用函數(shù)型語言ML編寫,使用自然演繹規(guī)則進(jìn)行定理證明。證明驗證工作在元邏輯(meta-logic)提供的框架下展開,所以它能支持多種邏輯系統(tǒng)。Coq是法國國家信息研究所(INRIA)開發(fā)的一個基于高階邏輯的證明器,由OCaml語言和少量C語言編寫。最初來源于1984年Coquand等開發(fā)的一個綜合依賴類型和多態(tài)類型的系統(tǒng)[15],并命名為構(gòu)造演算(calculus of constructions,CoC)。后來經(jīng)過擴(kuò)展,增加了歸納數(shù)據(jù)類型算法公理化的一些良好性質(zhì),形成歸納構(gòu)造演算(calculus of inductive co nstructions,CiC)。歸納構(gòu)造演算賦予了Coq更強(qiáng)的表達(dá)能力。

    可信編譯器(verified compiler)是另外一類有用的工具,它嚴(yán)格保證了源代碼和編譯之后機(jī)器碼之間的語義一致性,使在源碼層驗證的定理很容易擴(kuò)展到機(jī)器碼層。如果驗證了用C語言編寫的操作系統(tǒng)源代碼,通過可信編譯器生成的相應(yīng)機(jī)器碼也可以被認(rèn)為是通過驗證了,這樣實現(xiàn)端到端的定理證明變得更加容易。法國國家信息研究所(INRIA)著名的可信編譯器CompCert C[16]可以將Clight[17]編譯成語義一致的PowerPC、ARM和x86匯編代碼。編譯器中大約90%的編譯器算法(包括所有優(yōu)化和所有代碼生成算法)已經(jīng)在Coq中被證明是正確的[18]。CompCertMC[19]和CASCompCert[20]是對CompCert的一個擴(kuò)展,前者可以保證堆棧的有限性和細(xì)粒度的堆棧權(quán)限,后者是能夠?qū)o競爭的并發(fā)Clight程序進(jìn)行認(rèn)證的單獨編譯。編程語言CakeML自帶了一個經(jīng)過驗證的正確編譯器[21]。其他的有C Parser[22]和AutoCorres[23]工具的組合使用,可以自動將C程序轉(zhuǎn)換為語義一致的更高級別的monadic表示形式,簡化了C代碼的形式化驗證。VST-Floyd能夠提供一套半自動的策略,幫助用戶使用Verifiable C構(gòu)建C程序的功能正確性證明[24]。

    1.3 形式化語言

    目前C語言是大多數(shù)操作系統(tǒng)的程序設(shè)計語言,但是C語言的操作性語義難以表達(dá)不同層次規(guī)約,特別是高層的抽象規(guī)約,驗證時必須要將C語言轉(zhuǎn)換成等價的形式化語言。驗證μC/OS-Ⅱ[25]時,先使用Coq歸納定義了C語言數(shù)據(jù)結(jié)構(gòu)和程序語句等,再將μC/OS-Ⅱ的C代碼手動轉(zhuǎn)換成對應(yīng)的Coq代碼進(jìn)行驗證。DeepSpec聯(lián)盟[26]提倡的深度規(guī)約(deep specification)具有豐富、雙邊、形式化和靈活等基本性質(zhì)。符合深度規(guī)約的編程語言與規(guī)約語言的界限不再明顯。mC2[27]的大多數(shù)內(nèi)核代碼都是用ClightX[28]編寫的,ClightX是對Clight的一個擴(kuò)展,兩者能夠支持絕大部分C語言的語法。

    Haskell[29]和COGENT[30]是純函數(shù)式語言,能夠方便地在Isabelle/HOL中定義規(guī)約進(jìn)行推理,在操作系統(tǒng)的形式化設(shè)計與驗證中使用也非常多,如seL4的性質(zhì)驗證是基于Haskell編寫的原型系統(tǒng)[31]。作為函數(shù)式程序設(shè)計模型的lambda演算與自然推理系統(tǒng)這樣的證明演算之間具有相同的結(jié)構(gòu),因此不少人機(jī)交互定理證明器內(nèi)核是用函數(shù)式語言編寫,這使得函數(shù)式語言在用定理證明器時具有更好耦合性。COGENT保持了C語言的操作性和精簡性特點,還能夠簡單地表示高層抽象規(guī)約,驗證高層抽象定理。COGENT代碼可以經(jīng)過編譯器生成相同語義的C代碼。BilbyFs文件[32]系統(tǒng)就是使用COGENT語言設(shè)計編寫完成,并生成C代碼編譯運行。Coq 編寫的代碼也可以直接抽取出語義相同Haskell、OCaml等腳本。FSCQ文件系統(tǒng)[33]和DFSCQ文件系統(tǒng)[34]就是先通過Coq設(shè)計編寫,再自動抽取Haskell編譯運行。

    2 操作系統(tǒng)驗證方法

    2.1 操作系統(tǒng)精化關(guān)系驗證

    操作系統(tǒng)的驗證很大一部分歸結(jié)為精化關(guān)系驗證,例如驗證操作系統(tǒng)進(jìn)程調(diào)度無饑餓(starving-freedom)性質(zhì)時,任何單個語句函數(shù)都不能直接推導(dǎo)出結(jié)論,需要更高抽象規(guī)約描述,具體的代碼實現(xiàn)與高層抽象規(guī)約對軟件行為的定義必須要保持一致(等價)。精化關(guān)系則是定義了不同抽象模型或者程序之間的等價關(guān)系。操作系統(tǒng)驗證要選擇合適的精化關(guān)系定義。精化關(guān)系對運行環(huán)境假設(shè)太強(qiáng)時,現(xiàn)實運行環(huán)境難以滿足假設(shè)條件,相反假設(shè)太弱時,精化關(guān)系沒有可組合性等良好性質(zhì),難以進(jìn)行有效推理。當(dāng)前應(yīng)用較多的上下文精化關(guān)系從可觀測的角度對等價關(guān)系進(jìn)行定義。它是指在任何上下文環(huán)境中A替代B不產(chǎn)生更多的行為,并且客戶程序觀察不到A與B的區(qū)別。上下文精化與線性一致性是等價的[35],并發(fā)對象的功能正確性通常定義為線性一致性,因此操作系統(tǒng)在并發(fā)環(huán)境中的功能正確性證明等價于上下文精化關(guān)系的證明。實際上,從用戶角度來看,操作系統(tǒng)可以看作是為上層的應(yīng)用提供一組API接口服務(wù)的抽象虛擬機(jī)。同時操作系統(tǒng)是運行在硬件層上,能夠提供資源管理等服務(wù)的一組中間件的總和。所以說操作系統(tǒng)的正確性就是要求無論應(yīng)用程序是運行在抽象虛擬機(jī)上,還是運行在屏蔽硬件細(xì)節(jié)的中間件上,應(yīng)用程序觀察不到兩者的區(qū)別。

    操作系統(tǒng)的驗證往往包括了從設(shè)計到實現(xiàn)等多個不同抽象層的內(nèi)容,通常在低層抽象模型進(jìn)行推理證明是困難的,通過層次之間的精化關(guān)系證明,低層抽象模型性質(zhì)證明問題可轉(zhuǎn)化為更加容易證明的高層抽象模型性質(zhì)問題。

    2.2 操作系統(tǒng)驗證路徑

    操作系統(tǒng)形式化驗證基本的假設(shè)是硬件形式化模型的正確性和驗證性質(zhì)形式化規(guī)約正確性。它們本身都是非形式化的,硬件模型正確性取決于真實芯片運行與模型模擬運行是否完全一致,規(guī)約正確性取決于人們對操作系統(tǒng)性質(zhì)的定義是否符合其本意。兩者是聯(lián)系非形式化的現(xiàn)實世界與形式化的計算機(jī)世界的一個橋梁。從最上層的規(guī)約到最底層的硬件模型之間的形式化部分是操作系統(tǒng)形式化驗證的內(nèi)容,如圖1所示。由于操作系統(tǒng)驗證工作量比較大,有時會選擇擴(kuò)大上層或者底層的信任基,比如假設(shè)編譯器是正確的,以減少實際驗證工作量。

    圖1 驗證路徑示意圖Fig.1 Schematic map of verification path

    從操作系統(tǒng)規(guī)約開始自頂向下驗證操作系統(tǒng),是將頂層用戶非形式化需求變成系統(tǒng)形式化規(guī)約,對系統(tǒng)的功能需求進(jìn)行定義。對形式化規(guī)約建立抽象模型,通過定理證明驗證抽象模型的性質(zhì)。從CPU機(jī)器碼模型開始自底向上驗證操作系統(tǒng),根據(jù)CPU硬件指令構(gòu)造機(jī)器碼形式化模型,再通過建立逐步精化的模型不斷向上層抽象,最終證明系統(tǒng)滿足某些性質(zhì)。安全性(safety)是指“不好”的事情(如多個進(jìn)程進(jìn)入臨界區(qū))從不發(fā)生,活性(liveness)是指“好”的事情(如進(jìn)程申請進(jìn)入臨界區(qū))最終一定會發(fā)生,Alpern等[36]證明了任何性質(zhì)均可以表示成2種性質(zhì)的交。功能正確性是指代碼正確實現(xiàn)了規(guī)約的功能。這幾種性質(zhì)往往是操作系統(tǒng)驗證的關(guān)鍵性質(zhì)。

    無論自頂向下還是自底向上的驗證途徑,最終目標(biāo)是驗證機(jī)器硬件的最終實現(xiàn)與用戶規(guī)約的一致性,并以此為基礎(chǔ)證明系統(tǒng)滿足某種性質(zhì),即證明定理成立。

    2.3 大規(guī)模軟件驗證

    形式化驗證的工作量非常大,整個過程需要人工參與較多,特別是在操作系統(tǒng)這樣大規(guī)模驗證中問題更加突出。seL4項目中,約8 600行C代碼的證明工作涉及20萬行Isabelle腳本代碼,花去了11人·a的工作量。與軟件工程解決大規(guī)模軟件開發(fā)問題相類比,產(chǎn)生了證明工程的概念,引入軟件工程的思想和經(jīng)驗,可以應(yīng)用于解決一部分形式化方法中大規(guī)模驗證的問題。在軟件工程的關(guān)注點分離等原則的啟發(fā)下,驗證過程中很自然地引入了分層、模塊化和復(fù)用等方法技術(shù)。

    操作系統(tǒng)內(nèi)核函數(shù)調(diào)用關(guān)系錯綜復(fù)雜,局部微小的變動可能影響整個系統(tǒng)。通過認(rèn)證的方式將操作系統(tǒng)驗證分為多個模塊,減少單個模塊驗證的難度,同時將變動帶來的影響限制在模塊內(nèi)。復(fù)用已經(jīng)證明過的結(jié)果,可以盡量減少重復(fù)勞動,將已經(jīng)驗證的模塊或者常用證明結(jié)論形成定理庫,比如Coq的Iris[37]是一個高階并發(fā)分離邏輯庫,支持推理操作系統(tǒng)并發(fā)程序的安全性。工具能夠提高驗證開發(fā)的效率,大量減少驗證腳本工作量,CSIRO的data61為操作系統(tǒng)的形式化驗證開發(fā)了一系列相關(guān)工具,覆蓋驗證工作的各個階段[38]。DeepSpec項目也在致力于開發(fā)適用于形式化驗證的一整套工具鏈。

    另外,在操作系統(tǒng)實際驗證過程中,選用微內(nèi)核操作系統(tǒng)作為驗證對象是減少驗證規(guī)模的一個重要方法。以Linux為代表的宏內(nèi)核代碼量早已突破1 000萬行,seL4等大多數(shù)微內(nèi)核代碼都不到1萬行。從信任基最大限度地縮小和系統(tǒng)安全性等角度,選擇微內(nèi)核進(jìn)行形式化驗證也有著較為明顯的優(yōu)勢。目前操作系統(tǒng)驗證工作取得一定成果的seL4、mC2、PikeOS[39]、μC/OS-Ⅱ等也都是微內(nèi)核架構(gòu)。

    3 操作系統(tǒng)形式化驗證研究現(xiàn)狀

    3.1 Verve

    2010年,微軟基于類型化匯編語言(TAL)[40]和Hoare邏輯自動化驗證了Verve的類型安全和內(nèi)存安全[41]。完整的Verve由硬件抽象層Nucleus、內(nèi)核和應(yīng)用程序組成。Nucleus由TAL編寫,提供對硬件和內(nèi)存的原語訪問,實現(xiàn)內(nèi)存分配、垃圾收集、多堆棧、中斷處理和設(shè)備訪問等功能。內(nèi)核是在Nucleus之上構(gòu)建的更完整的高級別內(nèi)核服務(wù),例如搶占線程等,內(nèi)核是用C#語言編寫并最終編譯成TAL。

    驗證過程中,所有驗證代碼最終編譯成TAL,在TAL中手工注釋(hand-annotating)前置條件、后置條件和循環(huán)不變量斷言,再由Boogie[42]驗證器根據(jù)注釋的安全性和正確性規(guī)范進(jìn)行自動驗證。Boogie驗證器底層默認(rèn)的是一個Z3求解器,檢查斷言是否可滿足。

    Verve是第一個證明了類型安全和內(nèi)存安全的操作系統(tǒng),證明的自動化程度非常高,但是類型安全和內(nèi)存安全屬于比較弱的性質(zhì)。如果希望證明結(jié)論更有價值,通常需要證明更加強(qiáng)的性質(zhì),如功能正確性的證明。

    3.2 PikeOS

    2009年,德國Verisoft XT團(tuán)隊?wèi)?yīng)用VCC[43]驗證了PikeOS系統(tǒng)內(nèi)核一個改變線程優(yōu)先級的系統(tǒng)調(diào)用p4syscall_fast_set_prio的功能正確性,該系統(tǒng)調(diào)用跨越了PikeOS內(nèi)核所有層次,從硬件相關(guān)層次到用戶接口層次[44]。VCC是微軟等研發(fā)的一個用C語言開發(fā)的工業(yè)級驗證框架,支持通過添加輔助代碼(auxiliary code)和輔助狀態(tài)(ghost states)驗證底層并發(fā)的C 程序。驗證過程中,VCC把C代碼轉(zhuǎn)換成中間驗證語言Boogie,然后再轉(zhuǎn)換成驗證條件,最后由Z3實現(xiàn)定理證明或者給出反例。

    同年,Verisoft XT團(tuán)隊?wèi)?yīng)用VCC框架形式化驗證了Microsoft的多處理器虛擬機(jī)軟件Hyper-V,Hyper-V總共包含了10萬行并發(fā)C代碼和5 000行匯編代碼。VCC對Hyper-V中20%的代碼進(jìn)行了函數(shù)合約(function contract)和類型不變量等方面的驗證[45]。

    Verisoft XT團(tuán)隊在操作系統(tǒng)驗證方面做了小規(guī)模嘗試,驗證了操作系統(tǒng)PikeOS和Hyper-V的部分代碼的部分性質(zhì)。驗證工作VCC底層使用Z3,具有相對較高的自動化程度,但是其表達(dá)和證明能力有所不足,存在一定的局限性。驗證的代碼只占整個操作系統(tǒng)很少的一部分,而且也并未驗證Hyper-V的功能正確性等重要屬性。

    3.3 seL4

    2009年,NICTA的seL4團(tuán)隊(現(xiàn)在是CSIRO的Data61部門的Trustworthy Systems團(tuán)隊)驗證了高性能操作系統(tǒng)seL4微內(nèi)核的功能正確性和安全屬性。seL4包括8 600行C代碼和600行匯編代碼。通過形式化驗證,證明了seL4不會有內(nèi)存泄漏、空指針訪問、算術(shù)異常等問題。

    驗證過程中將seL4自頂向下分為3個層次。最上層MA是抽象層規(guī)約,描述了系統(tǒng)全部行為。這一層包含了系統(tǒng)外部接口足夠多的細(xì)節(jié),定義了系統(tǒng)能做什么。中間層ME是執(zhí)行層規(guī)約,它是一個可執(zhí)行模型,也是一個實現(xiàn),包括了所有數(shù)據(jù)結(jié)構(gòu)和實現(xiàn)細(xì)節(jié)的描述。中間層是最上層的細(xì)化,進(jìn)一步描述了系統(tǒng)怎么做。最底層MC是seL4的C實現(xiàn),包含了所有具體實現(xiàn)的細(xì)節(jié)。系統(tǒng)設(shè)計和驗證中,中間層的Haskell原型是一個關(guān)鍵因素,它有效協(xié)調(diào)了形式化驗證和系統(tǒng)性能之間的矛盾。操作系統(tǒng)開發(fā)小組使用Haskell作為編程語言,形式化驗證小組將原型作為中間執(zhí)行層導(dǎo)入定理證明器進(jìn)行驗證。

    系統(tǒng)主要性質(zhì)通過精化關(guān)系來證明。將精化關(guān)系記為?,seL4的三層模型關(guān)系可以表示為MC?ME,ME?MA,根據(jù)精化的傳遞性質(zhì)推出MC?MA。進(jìn)一步說明了如果一個安全性質(zhì)在抽象層成立,精化關(guān)系保證它在代碼實現(xiàn)層仍然成立。

    這是首次用形式化方法對一個通用操作系統(tǒng)內(nèi)核進(jìn)行功能正確性的驗證。不過為了降低驗證難度,他們在驗證seL4的內(nèi)核過程中,對內(nèi)核中的IO、中斷和內(nèi)存管理做了簡化處理,比如內(nèi)核不支持帶有細(xì)粒度鎖的多核并發(fā),回避了中斷和搶占導(dǎo)致的內(nèi)核并發(fā)問題。2013年Tessin[46]將單核seL4證明結(jié)果擴(kuò)展到基于BKL鎖的集群多核情況。

    3.4 CertiKOS

    抽象化、模塊化、層次化是操作系統(tǒng)軟件設(shè)計與實現(xiàn)的重要特征,耶魯大學(xué)的Flint團(tuán)隊提出的開放邏輯框架可以將不同計算特征和跨越不同抽象級別的程序模塊驗證組合,解決了難以設(shè)計單一類型的系統(tǒng)或程序邏輯來驗證整個操作系統(tǒng)的問題。

    2015年,F(xiàn)lint團(tuán)隊基于深度規(guī)約和認(rèn)證抽象層(certified abstraction layer)概念,通過分層的方法(將mCertiKOS分解成37層),完成了對操作系統(tǒng)mCertiKOS單核的驗證工作。一般接口的實現(xiàn)者很好地為調(diào)用者隱藏了自己內(nèi)部實現(xiàn)的細(xì)節(jié),與通常這種“淺規(guī)約”(shallow specification)不同,深度規(guī)約需要調(diào)用者了解所有有關(guān)實現(xiàn)的信息,這些信息是調(diào)用者的上下文環(huán)境重要的組成部分。每個認(rèn)證抽象層有足夠的信息使得性質(zhì)的證明不再關(guān)心已被抽象的C語言或者匯編語言實現(xiàn),可以更好進(jìn)行逐層精化的證明。每個抽象層都可以證明相應(yīng)的性質(zhì),并且在mCertiKOS將各個證明連接起來,復(fù)用了相同的證明。

    2016年,以深度規(guī)約技術(shù)為基礎(chǔ),F(xiàn)lint團(tuán)隊利用CertiKOS構(gòu)建并且驗證了一個細(xì)粒度并發(fā)多核操作系統(tǒng)mC2。CertiKOS是一個構(gòu)建認(rèn)證并發(fā)操作系統(tǒng)內(nèi)核的可擴(kuò)展框架,分為多個認(rèn)證抽象層,將困難的驗證任務(wù)分解為多個簡單、可自動化的小任務(wù)。mC2包含了6 100行C代碼和400行x86匯編代碼,目前已經(jīng)應(yīng)用于地面無人車輛系統(tǒng)的虛擬機(jī)(hypervisor)。

    相對seL4的證明,CertiKOS框架在于對細(xì)粒度鎖、真正并發(fā)的操作系統(tǒng)內(nèi)核功能正確性驗證取得了進(jìn)一步的突破,而通常認(rèn)為并發(fā)程序的驗證比順序程序要困難得多。雖然mC2是細(xì)粒度鎖,但是在鎖期間,系統(tǒng)是在關(guān)中斷的環(huán)境下運行的,還不是搶占式操作系統(tǒng)。另外CertiKOS與mC2高耦合,使得CertiKOS不適用于已有操作系統(tǒng)內(nèi)核的驗證。

    3.5 μC/OS-Ⅱ

    為了解決并發(fā)環(huán)境精化關(guān)系可組合性等問題,中科大-耶魯高可信軟件聯(lián)合研究中心2012年提出一種基于依賴-保證的模擬關(guān)系(rely-guarantee-based simulation,RGSim)作為通用的并發(fā)程序驗證手段,并對并發(fā)的垃圾收集(GC)等算法進(jìn)行了驗證[47]。依賴-保證模擬關(guān)系僅僅保證2個外部程序外部可觀測行為之間的包含關(guān)系,不要求程序執(zhí)行路徑集合之間具有包含關(guān)系。

    2016年,他們基于依賴-保證模擬關(guān)系提出一個并發(fā)分離邏輯風(fēng)格的并發(fā)精化程序邏輯(CSL-R),構(gòu)造了一個并發(fā)的上下文精化驗證框架,驗證了μC/OS-Ⅱ的中斷處理、任務(wù)調(diào)度、消息隊列、信號量和互斥鎖等模塊,證明了該系統(tǒng)互斥鎖不會發(fā)生優(yōu)先級反轉(zhuǎn)(priority-inversion-freedom,PIF)。一共驗證了1 400行左右的C代碼,同時將涉及的匯編代碼封裝為原語的方式完成底層內(nèi)核代碼的建模,驗證的函數(shù)覆蓋了μC/OS-Ⅱ中68%的常用函數(shù)。他們的驗證框架同樣也通過分層的方法,分別定義了底層機(jī)器模型和高層機(jī)器模型,并驗證了底層和高層之間的精化關(guān)系。驗證框架中開發(fā)了一系列自動證明策略,大幅度減少了證明腳本量。

    這是首次構(gòu)造了一個可以支持嵌套中斷和搶占操作系統(tǒng)內(nèi)核的驗證框架,并驗證了商用操作系統(tǒng)部分內(nèi)核模塊。目前驗證工作還未實現(xiàn)對μC/OS-Ⅱ內(nèi)核代碼全覆蓋。匯編代碼部分封裝成原語,因此沒有驗證任何匯編代碼,相對CertiKOS對匯編代碼的驗證工作,缺少了端到端的相關(guān)性質(zhì)定理的驗證。幾項主要的操作系統(tǒng)驗證工作比較見表1。

    表1 操作系統(tǒng)驗證工作比較

    3.6 其他相關(guān)工作

    2008年Myreen[48]基于Hoare邏輯和VCG(verification condition generation)在機(jī)器碼層對LISP語言解析器(interpreters)進(jìn)行了驗證。Hou等[49]基于LEON3 CPU指令集建立了一個形式化模型。Zhao等[50]定義了一個安全模型,通過驗證不變量,發(fā)現(xiàn)了ARINC653標(biāo)準(zhǔn)存在端口ID泄露、進(jìn)程ID泄露等6個安全問題。ARINC653是國際航空電子工程委員會起草的航空應(yīng)用標(biāo)準(zhǔn)軟件接口,定義了隔離微內(nèi)核的標(biāo)準(zhǔn)規(guī)約。Nelson等[51]使用Z3求解器,實現(xiàn)了Hyperkernel內(nèi)核全部自動化驗證,不過所有循環(huán)語句都被移出了內(nèi)核,大大降低了內(nèi)核的復(fù)雜度。2018年,他們使用Z3求解器實現(xiàn)了Nickel框架,可以用來設(shè)計驗證內(nèi)核接口無隱蔽信道[52]。

    作為操作系統(tǒng)最重要的組成部分,文件系統(tǒng)的驗證工作也有不少研究。Amani等[32]用COGENT分別寫了Linux兩個文件系統(tǒng)的實現(xiàn),并進(jìn)行了驗證。Chen等[34]驗證了FSCQ文件系統(tǒng),并證明了FSCQ在系統(tǒng)任何時候都可以重啟,恢復(fù)數(shù)據(jù)后保證不會丟失數(shù)據(jù)。

    4 操作系統(tǒng)形式化驗證存在的問題

    4.1 軟件復(fù)雜度高

    操作系統(tǒng)是最復(fù)雜的軟件之一,它大多用C語言內(nèi)嵌匯編語言實現(xiàn),還包含許多難以分解的相互依賴的組件和程序模塊。C語言中混合匯編語言還需要進(jìn)行寄存器和棧的操作,導(dǎo)致語義非常復(fù)雜。從代碼量上看,應(yīng)用最為廣泛的Linux操作系統(tǒng)內(nèi)核代碼量早已突破千萬行。微內(nèi)核與宏內(nèi)核相比,雖然最大程度地減小了內(nèi)核代碼量,但是內(nèi)核不同部分之間相互依賴性卻提高了很多。

    內(nèi)核的并發(fā)使得代碼執(zhí)行具有了不確定性。當(dāng)用戶和I /O并發(fā)執(zhí)行時,涉及控制權(quán)從一個線程轉(zhuǎn)移到另一個線程的控制機(jī)制。細(xì)粒度鎖的多核并發(fā)需要復(fù)雜的自旋鎖實現(xiàn)。這些并發(fā)機(jī)制的構(gòu)造都很復(fù)雜,執(zhí)行結(jié)果不確定,更難進(jìn)行推理驗證。與此同時,用戶關(guān)心的常常是整個系統(tǒng)在運行過程中一直保持的全局性質(zhì),因此驗證過程很可能要涉及操作系統(tǒng)的全部代碼。

    內(nèi)核功能復(fù)雜性、并發(fā)的不確定性和驗證性質(zhì)的全局性的結(jié)合使得對操作系統(tǒng)功能正確性等性質(zhì)的形式化驗證變得十分困難。

    4.2 驗證工作成本高

    一方面,雖然通過各種方法降低了操作形式化驗證的工作量,但是總體來說仍然居高不下,驗證1行C代碼平均需要25行左右的證明代碼。操作系統(tǒng)軟件本身代碼量比較大,需要進(jìn)行驗證的工作量更大。以μC/OS-Ⅱ 系統(tǒng)內(nèi)核的驗證為例,1 400行C代碼用了22萬行Coq腳本代碼,其中包括驗證框架約6萬行,證明庫約11萬行,代碼證明約4萬行,證明策略約1.5萬行,共約6人·a的工作量。而這樣的工作量在操作系統(tǒng)形式化驗證項目中并不少見。

    另外一方面軟件工程實踐對形式化接受度不高,一般項目很少通過形式化規(guī)約定義軟件,因此形式化驗證工作只有全部依賴于非常專業(yè)的人員。專業(yè)人員除了需要具有深厚的形式化理論功底,豐富的證明工具使用經(jīng)驗,還要對驗證的軟件有深刻的了解,過高的門檻使得這樣的專業(yè)人員非常稀缺。

    此外,操作系統(tǒng)需要不斷升級以支持適應(yīng)新的硬件平臺和應(yīng)用程序,版本升級帶來部分源代碼的改動有可能會導(dǎo)致重新驗證系統(tǒng)的巨大工作量。

    4.3 驗證工具局限性

    操作系統(tǒng)形式化驗證過程中,大量證明工作需要專業(yè)人員通過形式化工具完成。研究人員希望工具能夠自動化完成大部分證明工作,也希望工具能有強(qiáng)大的表達(dá)能力,能夠描述操作系統(tǒng)復(fù)雜的性質(zhì),但是工具的自動化程度與表達(dá)能力強(qiáng)弱往往成反比。如Z3等約束求解器可以對驗證條件自動求解,具有較高的自動化程度,但是它很難完成操作系統(tǒng)復(fù)雜數(shù)據(jù)結(jié)構(gòu)和軟件功能正確性的全部驗證。Coq和Isabelle/HOL等人機(jī)交互定理證明助手能夠使用表達(dá)更為豐富的高階邏輯,但是需要手工輸入腳本的工作量比較大。一階以上的高階邏輯公式有效性和可證性都是不可判定的,即定理在證明出來之前是無法知道是否可證,更無法找出通用的方法進(jìn)行自動證明。不可判定性在理論上決定了定理證明工具在自動化方面的局限性。

    可信編譯器等工具為實現(xiàn)操作系統(tǒng)從抽象規(guī)約到執(zhí)行代碼一致性的證明發(fā)揮了重要作用。這類工具既要保證源代碼和生成代碼的語義一致性,還要盡可能考慮優(yōu)化生成代碼執(zhí)行效率,往往兩者難以兼顧。另一方面,編譯器優(yōu)化太復(fù)雜,算法很難被認(rèn)證,其他非形式化的部分也難以驗證。認(rèn)可度較高的可信編譯器CompCert編譯生成的代碼運行速度平均比GCC編譯生成的代碼要慢15%左右。通過CompCert編譯產(chǎn)生的目標(biāo)機(jī)器碼,因為性能問題就很難被工業(yè)界實際廣泛使用。函數(shù)式語言COGENT能夠較好地描述操作系統(tǒng)高層抽象性質(zhì),但是COGENT編譯器在生成C代碼時幾乎沒有進(jìn)行優(yōu)化,其實用性還有待檢驗。

    5 結(jié) 語

    操作系統(tǒng)形式化驗證從最基本的類型安全等較弱的屬性到現(xiàn)在驗證功能正確性,高層抽象規(guī)約與底層代碼精化關(guān)系證明,其巨大進(jìn)步得益于形式化驗證技術(shù)和工具的發(fā)展。同時,軟件的形式化驗證技術(shù)和工具的局限性也在制約著操作系統(tǒng)形式化驗證工作走向最終的工業(yè)實用和普及。對這些技術(shù)和工具的研究創(chuàng)新,將在未來一段時間操作系統(tǒng)形式化驗證中占有重要位置。

    采用模塊化驗證,將復(fù)雜的操作系統(tǒng)分成多個更加簡單的模塊分別驗證,有助于減輕操作系統(tǒng)驗證的復(fù)雜度。構(gòu)建驗證框架和驗證定理庫,增強(qiáng)驗證成果的復(fù)用,有助于減少驗證工作的重復(fù)勞動。通過強(qiáng)化學(xué)習(xí)和規(guī)則學(xué)習(xí)算法構(gòu)建定理助手智能證明策略,可以加強(qiáng)定理助手在某些代碼和邏輯特征場景下的自動證明能力。

    隨著相關(guān)技術(shù)和工具的逐步成熟,實現(xiàn)以操作系統(tǒng)形式化驗證為代表的證明工程工業(yè)普及與應(yīng)用將成為可能,操作系統(tǒng)軟件系統(tǒng)的安全等問題也將從根本上得到解決。

    猜你喜歡
    精化編譯器正確性
    基于相異編譯器的安全計算機(jī)平臺交叉編譯環(huán)境設(shè)計
    一種基于系統(tǒng)穩(wěn)定性和正確性的定位導(dǎo)航方法研究
    n-精化與n-互模擬之間相關(guān)問題的研究
    淺談如何提高水質(zhì)檢測結(jié)果準(zhǔn)確性
    n-精化關(guān)系及其相關(guān)研究
    電子世界(2017年2期)2017-02-17 00:54:00
    雙口RAM讀寫正確性自動測試的有限狀態(tài)機(jī)控制器設(shè)計方法
    Petri網(wǎng)結(jié)點精化及其應(yīng)用
    通用NC代碼編譯器的設(shè)計與實現(xiàn)
    顧及完全球面布格異常梯度項改正的我國似大地水準(zhǔn)面精化
    編譯器無關(guān)性編碼在微控制器中的優(yōu)勢
    国内毛片毛片毛片毛片毛片| 国产 一区精品| 日日啪夜夜撸| 国产三级中文精品| 无遮挡黄片免费观看| 他把我摸到了高潮在线观看| 香蕉av资源在线| 国产高清视频在线观看网站| 日本与韩国留学比较| 赤兔流量卡办理| 大又大粗又爽又黄少妇毛片口| 精品久久久久久久人妻蜜臀av| 国内精品一区二区在线观看| 国产一级毛片七仙女欲春2| 白带黄色成豆腐渣| 欧美最黄视频在线播放免费| 天堂影院成人在线观看| 国产精品伦人一区二区| 极品教师在线视频| 亚洲avbb在线观看| 又黄又爽又刺激的免费视频.| 赤兔流量卡办理| 黄色一级大片看看| 中文亚洲av片在线观看爽| 1000部很黄的大片| 午夜福利在线在线| avwww免费| 国产国拍精品亚洲av在线观看| 91久久精品国产一区二区三区| 日本a在线网址| 在现免费观看毛片| 一进一出抽搐动态| 亚洲精华国产精华液的使用体验 | 日本欧美国产在线视频| 亚洲精品456在线播放app | 日本a在线网址| 夜夜夜夜夜久久久久| 女人被狂操c到高潮| 波多野结衣巨乳人妻| 成人永久免费在线观看视频| 三级国产精品欧美在线观看| 免费高清视频大片| 国产人妻一区二区三区在| 日韩大尺度精品在线看网址| 欧美又色又爽又黄视频| 中文字幕熟女人妻在线| 精品无人区乱码1区二区| 精品午夜福利视频在线观看一区| 日韩 亚洲 欧美在线| 国产单亲对白刺激| 蜜桃亚洲精品一区二区三区| 国产美女午夜福利| 日本欧美国产在线视频| 欧美色欧美亚洲另类二区| 精品99又大又爽又粗少妇毛片 | 丰满人妻一区二区三区视频av| 美女xxoo啪啪120秒动态图| 桃红色精品国产亚洲av| 免费在线观看成人毛片| 精品久久久久久成人av| 直男gayav资源| 波多野结衣巨乳人妻| 三级男女做爰猛烈吃奶摸视频| 在线观看av片永久免费下载| av国产免费在线观看| 久久久久久久久久黄片| 欧美性感艳星| 国内精品久久久久久久电影| 免费看光身美女| 久久国产乱子免费精品| 日韩av在线大香蕉| 99久久成人亚洲精品观看| 变态另类成人亚洲欧美熟女| 久久婷婷人人爽人人干人人爱| 亚洲国产精品成人综合色| 亚洲av电影不卡..在线观看| 久久香蕉精品热| 国产精品,欧美在线| 一本久久中文字幕| 非洲黑人性xxxx精品又粗又长| 性欧美人与动物交配| 热99在线观看视频| 有码 亚洲区| 啪啪无遮挡十八禁网站| 国产亚洲av嫩草精品影院| 国产淫片久久久久久久久| 国内久久婷婷六月综合欲色啪| 国产精品电影一区二区三区| 国产精品永久免费网站| 中出人妻视频一区二区| 亚洲精品乱码久久久v下载方式| 最近最新中文字幕大全电影3| 中文字幕高清在线视频| 欧美日韩瑟瑟在线播放| 色哟哟哟哟哟哟| 91av网一区二区| 波多野结衣高清作品| 一进一出好大好爽视频| 亚洲精品日韩av片在线观看| 午夜精品一区二区三区免费看| 欧美高清性xxxxhd video| 亚洲欧美激情综合另类| 午夜激情欧美在线| 丰满乱子伦码专区| 亚洲狠狠婷婷综合久久图片| 免费搜索国产男女视频| 亚洲黑人精品在线| 久久久久国内视频| 一级黄片播放器| 亚洲欧美激情综合另类| 别揉我奶头 嗯啊视频| av专区在线播放| 99久久九九国产精品国产免费| 22中文网久久字幕| 亚洲自偷自拍三级| 日韩av在线大香蕉| 桃色一区二区三区在线观看| 亚洲在线观看片| 黄色日韩在线| 2021天堂中文幕一二区在线观| 91麻豆精品激情在线观看国产| 男女之事视频高清在线观看| 乱系列少妇在线播放| 国产大屁股一区二区在线视频| 婷婷亚洲欧美| 久久国产乱子免费精品| 琪琪午夜伦伦电影理论片6080| 亚洲av第一区精品v没综合| 女同久久另类99精品国产91| 美女被艹到高潮喷水动态| 亚洲人成网站高清观看| 中文资源天堂在线| 少妇熟女aⅴ在线视频| 麻豆久久精品国产亚洲av| 最新中文字幕久久久久| 狂野欧美激情性xxxx在线观看| 嫁个100分男人电影在线观看| 99久久成人亚洲精品观看| 午夜免费男女啪啪视频观看 | 热99在线观看视频| 国产黄色小视频在线观看| 午夜福利视频1000在线观看| 日本在线视频免费播放| 亚洲国产精品合色在线| 成年女人看的毛片在线观看| 草草在线视频免费看| 搡老妇女老女人老熟妇| 成人二区视频| 国产亚洲精品av在线| 国产高清视频在线播放一区| 免费看a级黄色片| 五月伊人婷婷丁香| 亚洲av五月六月丁香网| 身体一侧抽搐| 无遮挡黄片免费观看| 美女高潮喷水抽搐中文字幕| 69人妻影院| 日韩av在线大香蕉| 乱系列少妇在线播放| 日韩欧美国产在线观看| 欧美激情国产日韩精品一区| 网址你懂的国产日韩在线| 国产一级毛片七仙女欲春2| 日本与韩国留学比较| 成年女人永久免费观看视频| 亚洲va在线va天堂va国产| 校园春色视频在线观看| 亚洲性久久影院| 欧美+亚洲+日韩+国产| 天堂√8在线中文| 国产成人影院久久av| 亚洲精品乱码久久久v下载方式| 欧美日韩瑟瑟在线播放| 国产 一区精品| 日韩欧美免费精品| 免费在线观看成人毛片| 波多野结衣巨乳人妻| 国内少妇人妻偷人精品xxx网站| 九色成人免费人妻av| 国产欧美日韩一区二区精品| 国产高清三级在线| 99久久九九国产精品国产免费| 伦理电影大哥的女人| 尤物成人国产欧美一区二区三区| 亚洲av中文字字幕乱码综合| 国产免费一级a男人的天堂| 色噜噜av男人的天堂激情| 日韩强制内射视频| 国产精品三级大全| 精品一区二区三区视频在线| 中文字幕免费在线视频6| 亚洲国产日韩欧美精品在线观看| 91久久精品电影网| 天堂√8在线中文| 亚洲四区av| 免费观看精品视频网站| 999久久久精品免费观看国产| 国产精品免费一区二区三区在线| 桃红色精品国产亚洲av| 九色国产91popny在线| 熟女电影av网| 丰满的人妻完整版| 欧美成人a在线观看| 精品久久久久久成人av| 婷婷亚洲欧美| 在线观看一区二区三区| 亚洲精华国产精华精| 欧美高清性xxxxhd video| 国产精品98久久久久久宅男小说| 久久久久久久久久黄片| 少妇高潮的动态图| 午夜精品在线福利| 亚洲人成伊人成综合网2020| 中文字幕久久专区| 免费无遮挡裸体视频| 18禁黄网站禁片免费观看直播| 国内毛片毛片毛片毛片毛片| 在线看三级毛片| 亚洲精华国产精华液的使用体验 | 很黄的视频免费| 亚洲中文日韩欧美视频| 日韩人妻高清精品专区| 国产精品三级大全| 中文字幕精品亚洲无线码一区| 亚洲av中文字字幕乱码综合| 人人妻,人人澡人人爽秒播| 亚洲av日韩精品久久久久久密| 午夜激情福利司机影院| 欧美日本视频| 美女免费视频网站| 能在线免费观看的黄片| 在线天堂最新版资源| 亚洲av一区综合| 日本一本二区三区精品| 草草在线视频免费看| 一级黄片播放器| 亚洲中文字幕日韩| 岛国在线免费视频观看| 亚洲国产日韩欧美精品在线观看| 国产精品三级大全| 亚洲在线观看片| 久久精品久久久久久噜噜老黄 | 3wmmmm亚洲av在线观看| 国产日本99.免费观看| 日本黄色视频三级网站网址| 性插视频无遮挡在线免费观看| 亚洲午夜理论影院| 麻豆国产97在线/欧美| 亚洲国产精品久久男人天堂| 亚洲精品成人久久久久久| 国产淫片久久久久久久久| 婷婷精品国产亚洲av| 日韩强制内射视频| 美女被艹到高潮喷水动态| 男女做爰动态图高潮gif福利片| 美女 人体艺术 gogo| 在线观看免费视频日本深夜| 免费人成视频x8x8入口观看| 久久久久久久久久成人| 亚洲无线在线观看| 日日夜夜操网爽| 亚洲av.av天堂| 亚洲精品456在线播放app | 简卡轻食公司| 亚洲性久久影院| 国内少妇人妻偷人精品xxx网站| 免费一级毛片在线播放高清视频| 色综合色国产| 日本与韩国留学比较| 性插视频无遮挡在线免费观看| 国产精品久久电影中文字幕| 白带黄色成豆腐渣| 热99在线观看视频| 日韩欧美免费精品| 国产麻豆成人av免费视频| 亚洲性夜色夜夜综合| 午夜福利在线观看吧| 日本撒尿小便嘘嘘汇集6| 搞女人的毛片| 五月伊人婷婷丁香| 免费看美女性在线毛片视频| 一级黄片播放器| 免费一级毛片在线播放高清视频| 国产高清视频在线播放一区| 男女边吃奶边做爰视频| 简卡轻食公司| 欧美日本视频| 色噜噜av男人的天堂激情| 一边摸一边抽搐一进一小说| 亚洲欧美日韩高清在线视频| 成人国产一区最新在线观看| 观看美女的网站| 国产精品永久免费网站| 身体一侧抽搐| 亚洲国产欧美人成| 91精品国产九色| 国产精品亚洲一级av第二区| 免费高清视频大片| 亚洲久久久久久中文字幕| 欧美又色又爽又黄视频| 非洲黑人性xxxx精品又粗又长| 999久久久精品免费观看国产| 欧美成人一区二区免费高清观看| 白带黄色成豆腐渣| 少妇猛男粗大的猛烈进出视频 | 久久久国产成人精品二区| 日韩人妻高清精品专区| 亚洲成人久久爱视频| 精品一区二区三区视频在线观看免费| 亚洲va在线va天堂va国产| 看十八女毛片水多多多| 久久亚洲真实| 亚洲精品一卡2卡三卡4卡5卡| 少妇裸体淫交视频免费看高清| 中文字幕av在线有码专区| 哪里可以看免费的av片| 成人美女网站在线观看视频| 亚洲国产欧洲综合997久久,| 午夜精品一区二区三区免费看| 日日撸夜夜添| 午夜久久久久精精品| 国内揄拍国产精品人妻在线| 日本三级黄在线观看| 亚洲成人精品中文字幕电影| 欧美3d第一页| 国产真实伦视频高清在线观看 | 一区福利在线观看| 精品日产1卡2卡| 欧美日本亚洲视频在线播放| 欧美色欧美亚洲另类二区| 成人国产一区最新在线观看| 午夜激情欧美在线| 波多野结衣高清无吗| 午夜爱爱视频在线播放| 国产高潮美女av| 日本欧美国产在线视频| 免费在线观看影片大全网站| 简卡轻食公司| 91午夜精品亚洲一区二区三区 | av国产免费在线观看| 在线看三级毛片| 男人舔奶头视频| 高清毛片免费观看视频网站| 欧美高清成人免费视频www| 国产精品99久久久久久久久| 欧美最黄视频在线播放免费| 国产免费一级a男人的天堂| 舔av片在线| 国产精品久久电影中文字幕| 免费在线观看影片大全网站| 亚洲av第一区精品v没综合| 国产色婷婷99| 少妇人妻一区二区三区视频| 午夜免费激情av| 美女被艹到高潮喷水动态| 精品久久久久久,| 黄色女人牲交| 国产真实乱freesex| 欧美激情久久久久久爽电影| 免费不卡的大黄色大毛片视频在线观看 | 在线观看午夜福利视频| 99九九线精品视频在线观看视频| 国产日本99.免费观看| 亚洲经典国产精华液单| 久久久久久久久久黄片| 国产亚洲av嫩草精品影院| 欧美+日韩+精品| 99热网站在线观看| 亚洲av第一区精品v没综合| 蜜桃亚洲精品一区二区三区| 免费观看在线日韩| 男女之事视频高清在线观看| 亚洲在线观看片| 午夜影院日韩av| 日本欧美国产在线视频| 黄色配什么色好看| 长腿黑丝高跟| 国产v大片淫在线免费观看| 99视频精品全部免费 在线| 免费电影在线观看免费观看| 久久午夜亚洲精品久久| 不卡视频在线观看欧美| 欧美精品国产亚洲| 中文在线观看免费www的网站| 18禁黄网站禁片免费观看直播| 成人性生交大片免费视频hd| 免费观看在线日韩| 女人十人毛片免费观看3o分钟| 中文字幕高清在线视频| 亚洲精品日韩av片在线观看| 日韩高清综合在线| 日韩欧美在线乱码| 久久这里只有精品中国| 国内精品久久久久久久电影| 全区人妻精品视频| 男女之事视频高清在线观看| 免费观看精品视频网站| 国产伦精品一区二区三区视频9| 国产麻豆成人av免费视频| 91久久精品电影网| 非洲黑人性xxxx精品又粗又长| 午夜免费成人在线视频| 中出人妻视频一区二区| 久久婷婷人人爽人人干人人爱| 直男gayav资源| 亚洲av.av天堂| 国产精品一区二区免费欧美| 99在线人妻在线中文字幕| 国产伦精品一区二区三区四那| a级毛片a级免费在线| av在线亚洲专区| 少妇裸体淫交视频免费看高清| 国产精品乱码一区二三区的特点| 亚洲五月天丁香| 又紧又爽又黄一区二区| 国产亚洲精品久久久com| 欧美日韩黄片免| 久久久色成人| 波多野结衣高清无吗| 啦啦啦啦在线视频资源| 日本色播在线视频| 精品无人区乱码1区二区| 亚洲第一区二区三区不卡| 给我免费播放毛片高清在线观看| 中文亚洲av片在线观看爽| 岛国在线免费视频观看| 日韩,欧美,国产一区二区三区 | 一个人看视频在线观看www免费| 最近中文字幕高清免费大全6 | 国产精品女同一区二区软件 | 国产精品嫩草影院av在线观看 | 毛片女人毛片| 国内少妇人妻偷人精品xxx网站| 国内精品久久久久久久电影| 精品久久久久久久久亚洲 | 欧美一区二区国产精品久久精品| 久久久久久久久久成人| 精品久久久久久久末码| 99视频精品全部免费 在线| 亚洲欧美日韩高清专用| 免费看a级黄色片| 女的被弄到高潮叫床怎么办 | 波多野结衣巨乳人妻| 欧美一区二区亚洲| 亚洲精品一卡2卡三卡4卡5卡| 日本一二三区视频观看| 国产爱豆传媒在线观看| 一级av片app| 久久精品国产亚洲av香蕉五月| 久久久久久久亚洲中文字幕| 亚洲最大成人av| 国产伦一二天堂av在线观看| 国产精品久久视频播放| 午夜精品在线福利| 国产三级中文精品| 成熟少妇高潮喷水视频| 亚洲av美国av| netflix在线观看网站| 嫩草影院新地址| 麻豆成人av在线观看| 亚洲av免费高清在线观看| 成人国产一区最新在线观看| 特大巨黑吊av在线直播| 99久久中文字幕三级久久日本| 啦啦啦观看免费观看视频高清| 淫秽高清视频在线观看| 色综合色国产| 日韩亚洲欧美综合| 久久人人精品亚洲av| 欧美另类亚洲清纯唯美| 国产精品国产三级国产av玫瑰| 99久久精品一区二区三区| 美女xxoo啪啪120秒动态图| 国产白丝娇喘喷水9色精品| 国产精华一区二区三区| 此物有八面人人有两片| 精品午夜福利视频在线观看一区| 日韩欧美三级三区| 国产亚洲精品av在线| 免费搜索国产男女视频| 国产女主播在线喷水免费视频网站 | 久久久久性生活片| 色噜噜av男人的天堂激情| 国产高清三级在线| 听说在线观看完整版免费高清| 成人高潮视频无遮挡免费网站| 色精品久久人妻99蜜桃| 国产爱豆传媒在线观看| 欧美日韩亚洲国产一区二区在线观看| 国产精品人妻久久久影院| 国产精品不卡视频一区二区| 少妇猛男粗大的猛烈进出视频 | 国产精品1区2区在线观看.| 久久九九热精品免费| 免费看a级黄色片| 直男gayav资源| 丰满人妻一区二区三区视频av| 国产综合懂色| 2021天堂中文幕一二区在线观| 久久久成人免费电影| 麻豆精品久久久久久蜜桃| 国产免费一级a男人的天堂| a在线观看视频网站| 伊人久久精品亚洲午夜| 最近视频中文字幕2019在线8| 看片在线看免费视频| 免费不卡的大黄色大毛片视频在线观看 | 日本熟妇午夜| 亚洲av一区综合| 中国美白少妇内射xxxbb| 色综合站精品国产| 欧美潮喷喷水| 国产av不卡久久| 国产精品电影一区二区三区| 国产成人福利小说| 99九九线精品视频在线观看视频| 又爽又黄a免费视频| 97超视频在线观看视频| 精品久久久噜噜| 精品午夜福利在线看| 亚洲人成网站高清观看| 久久久久久久久久黄片| 国产精品永久免费网站| 91av网一区二区| 亚洲精品乱码久久久v下载方式| 一进一出好大好爽视频| 国产探花在线观看一区二区| 噜噜噜噜噜久久久久久91| 国产成人一区二区在线| 啪啪无遮挡十八禁网站| 免费观看在线日韩| 国产美女午夜福利| 2021天堂中文幕一二区在线观| 在线看三级毛片| 3wmmmm亚洲av在线观看| 欧美另类亚洲清纯唯美| 草草在线视频免费看| 久久久国产成人精品二区| 欧美日本亚洲视频在线播放| 国产单亲对白刺激| 91av网一区二区| 老司机福利观看| 男人舔女人下体高潮全视频| 免费黄网站久久成人精品| 久久精品夜夜夜夜夜久久蜜豆| 成熟少妇高潮喷水视频| 99久久精品热视频| 乱码一卡2卡4卡精品| 久久久久久久久久黄片| 成人综合一区亚洲| 极品教师在线免费播放| 黄色配什么色好看| 午夜福利成人在线免费观看| 成人美女网站在线观看视频| 国产亚洲91精品色在线| 免费观看精品视频网站| 日韩强制内射视频| 亚洲午夜理论影院| 在线免费观看的www视频| 国产精品永久免费网站| 我的女老师完整版在线观看| 国产又黄又爽又无遮挡在线| 久久婷婷人人爽人人干人人爱| 一本精品99久久精品77| 亚洲av美国av| 啦啦啦观看免费观看视频高清| 欧美性猛交黑人性爽| 国产亚洲精品av在线| 一个人免费在线观看电影| 亚洲国产精品合色在线| 一区二区三区免费毛片| 999久久久精品免费观看国产| 亚洲成人久久爱视频| 亚洲自拍偷在线| 日韩欧美在线二视频| 高清日韩中文字幕在线| 欧美最黄视频在线播放免费| 我要看日韩黄色一级片| 天天一区二区日本电影三级| 欧美xxxx黑人xx丫x性爽| 精品一区二区三区视频在线观看免费| 99精品久久久久人妻精品| 神马国产精品三级电影在线观看| 又爽又黄无遮挡网站| 草草在线视频免费看| 亚洲在线观看片| 舔av片在线| 婷婷亚洲欧美| 午夜免费激情av| 欧美一区二区精品小视频在线| 99热6这里只有精品| 国产伦精品一区二区三区视频9| 在线播放无遮挡| 国产精品嫩草影院av在线观看 | 色噜噜av男人的天堂激情| 可以在线观看毛片的网站| 一区二区三区免费毛片| av在线观看视频网站免费| 久久久久久久亚洲中文字幕| av视频在线观看入口| 亚洲精品亚洲一区二区| 久久国产精品人妻蜜桃| 91久久精品国产一区二区三区| 亚洲最大成人中文| 禁无遮挡网站| av国产免费在线观看| 久久久久久久久中文| 欧美成人一区二区免费高清观看| 身体一侧抽搐| 免费看av在线观看网站| 五月玫瑰六月丁香| 国产精品98久久久久久宅男小说| 国产69精品久久久久777片| 有码 亚洲区| 国产精品久久久久久久电影|