亚洲免费av电影一区二区三区,日韩爱爱视频,51精品视频一区二区三区,91视频爱爱,日韩欧美在线播放视频,中文字幕少妇AV,亚洲电影中文字幕,久久久久亚洲av成人网址,久久综合视频网站,国产在线不卡免费播放

        ?

        網(wǎng)絡(luò)系統(tǒng)實時性模型的驗證方法綜述

        2018-09-26 11:43:10杜澤民王曉玲陳宜成
        網(wǎng)絡(luò)空間安全 2018年3期
        關(guān)鍵詞:實時性網(wǎng)絡(luò)安全

        杜澤民 王曉玲 陳宜成

        摘 要:互聯(lián)網(wǎng)技術(shù)的發(fā)展和應(yīng)用在各個生產(chǎn)領(lǐng)域中發(fā)揮著越來越積極的作用,但隨著網(wǎng)絡(luò)技術(shù)應(yīng)用的深入,網(wǎng)絡(luò)系統(tǒng)的實時性成為影響網(wǎng)絡(luò)安全的一大因素,因此對網(wǎng)絡(luò)模型的通信實時性、威脅分析實時性的驗證成為網(wǎng)絡(luò)安全的重要保障。目前,國內(nèi)外在實時性驗證方面有諸多研究,形成了不同的方法體系。文章把主要的模型實時性驗證方法,從理論和工具角度加以介紹分析,并對各個方法進行了比較。

        關(guān)鍵詞:網(wǎng)絡(luò)安全;實時性;模型驗證;實時性驗證

        中圖分類號:TP393.0 文獻標識碼:A

        1 引言

        在互聯(lián)網(wǎng)時代,網(wǎng)絡(luò)安全問題是互聯(lián)網(wǎng)建設(shè)的重要議題,而網(wǎng)絡(luò)系統(tǒng)的實時性是網(wǎng)絡(luò)安全的重要保證[1]。其中,包括通信的實時性以及威脅分析的實時性等。當網(wǎng)絡(luò)受到外界攻擊時,系統(tǒng)應(yīng)該對相應(yīng)的問題快速做出反應(yīng)并處理措施。問題處理完畢后,還應(yīng)將處理結(jié)果在規(guī)定的時間內(nèi)反饋給系統(tǒng)。實時網(wǎng)絡(luò)系統(tǒng)的每一個運行過程都是為了能夠保證整個網(wǎng)絡(luò)系統(tǒng)各項工作的協(xié)調(diào)進行。

        模型驅(qū)動方法面對復(fù)雜度、集成性更高的大型系統(tǒng)有著安全性高、開發(fā)成本低等優(yōu)勢。當前的航空、航天控制系統(tǒng)、軍事指揮自動化系統(tǒng),也逐漸采用基于模型的開發(fā)方式,而這類系統(tǒng)對軟件有著應(yīng)實時性要求,反應(yīng)時間要控制在幾毫秒以內(nèi),而通常還要求保留一定的反應(yīng)余量。因此,模型驗證在網(wǎng)絡(luò)系統(tǒng)的實時性驗證上具有先天優(yōu)勢。

        目前,國內(nèi)外對模型的功能與正確性驗證研究比較豐富,但是實時性驗證研究并不廣泛。因此,本文將介紹當前實時性驗證所面臨的問題,并重點介紹網(wǎng)絡(luò)系統(tǒng)實時性驗證領(lǐng)域的建模方法,并結(jié)合這些方法所依托的工具,分析各種方法所面臨的問題,最后針對檢測方法面臨的挑戰(zhàn)提出一些思路。

        2 模型驗證方法及面臨的問題

        模型檢測首先要對系統(tǒng)建模,選用一種形式化描述方法,將待驗證的系統(tǒng)設(shè)計轉(zhuǎn)化為工具所能接受的模型,比如狀態(tài)遷移圖。然后,將系統(tǒng)所要驗證的性質(zhì)采用形式化的邏輯公式來描述,比如時態(tài)邏輯。它能夠描述系統(tǒng)隨著時間變化而引起的行為變化。最后是系統(tǒng)驗證,是通過模型檢測算法對系統(tǒng)模型的狀態(tài)空間進行窮盡搜索。如果未發(fā)現(xiàn)違反性質(zhì)描述的狀態(tài),則表明該模型滿足期望的性質(zhì),否則給出一個反例路徑,供設(shè)計人員參考。

        模型驗證方法應(yīng)用初期,系統(tǒng)的狀態(tài)和狀態(tài)間的遷移都是采用顯式的狀態(tài)遷移圖來表示。這種方法對那些進程數(shù)量較少的網(wǎng)絡(luò)系統(tǒng)非常實用[2]。而當網(wǎng)絡(luò)分量較多時,系統(tǒng)的全局狀態(tài)空間會隨著分量的增加,呈指數(shù)增長,即產(chǎn)生狀態(tài)爆炸問題,狀態(tài)爆炸問題是阻礙模型檢測技術(shù)應(yīng)用的瓶頸。

        3 建模方法

        3.1 最差情況執(zhí)行時間方法

        最差情況執(zhí)行時間(Worst-Case Execution Time,WCET)是驗證系統(tǒng)實時性的主要方法之一,由奧地利維也納技術(shù)大學(xué)的Puschner和Burns提出[3]。WCET剛提出時,由于當時計算機軟件需求有限,軟件代碼的執(zhí)行時間未引起人們的重視。但是,隨著軟件技術(shù)的不斷發(fā)展,代碼執(zhí)行時間的越來越復(fù)雜,WCET分析技術(shù)逐漸受到研究者的重視,目前,國內(nèi)外有許多機構(gòu)或大學(xué)開始加深對WCET的研究,從2001年開始,國際上每年召開一次WCET研討會。WCET分析技術(shù)與計算方法趨于多樣化,從早期的程序標注和語法制導(dǎo)算法發(fā)展為基于樹和路徑的計算方法。

        WCET分析是指計算給定應(yīng)用程序代碼片斷執(zhí)行時間的上限,這里的執(zhí)行時間定義為執(zhí)行代碼片斷所花費的處理器時間。在實時系統(tǒng)中,如果想保證系統(tǒng)整體的實時性得到滿足,就必須要求軟件各部分在最差情況下執(zhí)行的時間也能滿足實時性要求,這樣由部分集成到整體時,整個系統(tǒng)才會滿足實時性的要求。

        WCET分析要求安全性和精確性,安全要求不能低估最差執(zhí)行時間,精確要求能夠給出可以接受的高估值。我們假設(shè)程序P的WCET估算值為WCETc (P),P的實際WCET值為WCETA (P),安全性和精確性描述為:

        安全性:

        WCETc (P) ≥WCETA (P)

        精確性:

        (WCETc(P) -WCETA(P))/WCETA(P)≤δmax

        其中,δmax為系統(tǒng)能夠接受的最大相對誤差。

        在程序?qū)哟蔚尿炞C方面,國防科技大學(xué)張曦團隊利用WCET技術(shù)對嵌入式實時軟件的驗證進行了深入研究,提出了一種基于WCET分析的模型檢驗方法框架[4],實現(xiàn)了對源程序的一種實時性驗證方法。

        該框架首先對源程序進行WCET分析,其中包括對程序的靜態(tài)分析,劃分出程序代碼的路徑集,然后利用WCET工具進行分析程序執(zhí)行時間上限,分析過程如圖1所示。

        利用WCET分析結(jié)果對原有的實時約束進行修正,建立系統(tǒng)的實時性模型,同時在系統(tǒng)需求中提取時態(tài)邏輯作為系統(tǒng)的性質(zhì)描述,其中時態(tài)邏輯反映了程序應(yīng)該遵循的先后順序。結(jié)合實時性模型與時態(tài)邏輯公式通過驗證工具UPPAAL對模型的實時性進行驗證,如果實時性驗證不通過,則返回修改源程序。如圖2所示。

        本方法做到了對實時系統(tǒng)的程序?qū)哟蔚尿炞C,較好地解決了狀態(tài)爆炸問題,其中源程序的WCET分析是驗證環(huán)節(jié)的重要一環(huán),但是當前WCET分析能力有限,比如復(fù)雜程序運算時間估算、估值精確度、誤差控制等問題。另外,對源程序的修正可能會引入新的錯誤,并且修正內(nèi)容無法反映到生成代碼的上層模型中。

        3.2 時間自動機建模

        為了描述實時系統(tǒng)的時間約束關(guān)系,Alur等人提出了時間自動機(Timed Automata,TA)[5]。時間自動機是一類帶有時鐘變量的有限狀態(tài)自動機,其數(shù)學(xué)模型可表述為一個六元組:

        Ta= (L,L0,C,A,E,I )

        其中:L是位置的有限集合;l0∈L,為初始位置;C是時鐘有限集合;A是行為的有限集合;"EL×B(C)×A×2c×L是邊的集合,用于描述位置之間的轉(zhuǎn)移;B(C)是使能條件集合,用于描述發(fā)生轉(zhuǎn)移的時間約束,2c為轉(zhuǎn)移發(fā)生時的時鐘集合;映射I:"L→ B(C)" 用于給每個位置指定一個時鐘約束。

        用時間自動機網(wǎng)對實時系統(tǒng)建模,首先要對系統(tǒng)進行抽象和簡化,子系統(tǒng)要簡化為有限控制結(jié)構(gòu)、時鐘和變量構(gòu)成的時間自動機,子系統(tǒng)之間通過通道進行通訊。然后要分析實時系統(tǒng)的信息處理過程,提煉重要的信息處理狀態(tài)和事件進行建模。子系統(tǒng)的行為抽象為時間自動機,它們之間的信息交互通過通道來完成,各個時間自動機就組成網(wǎng)絡(luò)進而描述整個實時系統(tǒng)的信息處理過程。

        時間自動機是一種反映了時間約束的有限狀態(tài)轉(zhuǎn)換圖,通過使用有限的真值時鐘變量表示時間約束,實時系統(tǒng)行為可以通過時間自動機來刻畫,在對實時系統(tǒng)建模后,可以利用時間自動機來驗證系統(tǒng)的實時性。在實時性約束下檢驗狀態(tài)是否可達,因此對狀態(tài)可達性的研究是時間自動機的驗證技術(shù)的關(guān)鍵。

        時間自動機技術(shù)也有不足:構(gòu)造時間自動機方法很復(fù)雜,如果發(fā)生錯誤,將導(dǎo)致最終驗證結(jié)果的不準確。另外,時間自動機的時間無限制,會導(dǎo)致狀態(tài)空間的無限性,隨著系統(tǒng)的復(fù)雜程度和進程數(shù)量的增加,將無可避免的發(fā)生狀態(tài)空間爆炸。狀態(tài)空間爆炸也是困擾實時系統(tǒng)驗證的最大問題。

        但是,典型的時間自動機組成的平面網(wǎng)絡(luò)作為模型不易于模擬和調(diào)試大規(guī)模的工業(yè)系統(tǒng)。AIexandre David和Wang Yi提出了一種層疊時間自動機(Hierarchical Timed Automata,HTA)模型,它的狀態(tài)既可以是簡單狀態(tài)也可以是組合狀態(tài),組合狀態(tài)本身就是一個時間自動機。

        層疊時間自動機的允許用戶在模擬時,將系統(tǒng)模型的內(nèi)部結(jié)構(gòu)隱藏或者抽象,并且更容易調(diào)試,在處理多層次復(fù)雜系統(tǒng)建模時有較大優(yōu)勢。

        3.3 RTCTL模型檢測方法

        計算樹邏輯(Computation Tree Logic,CTL)是時序邏輯的一個分支,時序邏輯非常適合于對并發(fā)系統(tǒng)進行驗證與刻畫,即使對于復(fù)雜的并發(fā)系統(tǒng)而言,其刻畫性質(zhì)依然很強。時序邏輯用于描述系統(tǒng)中的狀態(tài)變遷序列,不顯示地表示時間,而是通過語義隱式表達時間。時序邏輯定義時序運算符與邏輯連接詞來表達復(fù)雜的時序性質(zhì)。CTL作為時序邏輯的一個分支主要用來描述計算樹的性質(zhì)[8]。

        CTL公式由路徑量詞與時序運算符組成。路徑量詞用于描述計算樹的分支結(jié)構(gòu),有兩種路徑量詞:A(對于所有計算路徑)和E(對于某些計算路徑),分別表示從某狀態(tài)開始的所有路徑和某些路徑所具有的性質(zhì)。時序運算符描述某條路徑的具體性質(zhì)。有5個基本運算符,意義如下:X(下一個狀態(tài))F(將來某狀態(tài))G(將來全局狀態(tài))U(直到……都滿足)R(直到……才滿足)。

        CTL有兩種公式:狀態(tài)公式與路徑公式。令A(yù)P為原子命題集合,狀態(tài)公式語法為:

        1) 如果p∈AP,則p是一個狀態(tài)公式;

        2) 如果f和g是狀態(tài)公式,則f和f∧g,f∨g是狀態(tài)公式;

        3) 如果f是一個路徑公式,則Ef和Af是狀態(tài)公式。

        路徑公式的語法為:

        如果f是一狀態(tài)公式,則f也是一路徑公式;

        如果f和g是路徑公式,則f,f∧g,f∨g,Xf,F(xiàn)f,Gf,fUg和飛fRg是路徑公式[9]。

        檢測實時系統(tǒng)的時間約束的有效方法就是擴充CTL運算符,Emerson等人將CTL邏輯擴充為RTCTL?;镜腞TCTL運算符是受限的直到運算符U[a,b]這里[a,b]表示時間間隔,在此間隔內(nèi)這個性質(zhì)必須是真的。fU[a,b]g關(guān)于某條路徑π=s0,s1…為真,僅當g在此路徑上將來的某個狀態(tài)s上滿足,那么f在s0到s上所有狀態(tài)都為真,并且s0到s的距離在間隔[a,b]之間。同樣的,CTL中的其他運算符可以增加時間限制來擴展。[a,b]作為一個時間間隔,可以看做是實時性的約束。

        RTCTL模型在CTL的基礎(chǔ)上進行了擴充,繼承了CTL模型的精確性,解決了狀態(tài)空間爆炸問題,同時加入了時間性約束,可以高效地表達實時性要求。目前有很多工具可以完成基于CTL的模型驗證,RTCTL在實時性驗證中的有很好的應(yīng)用前景。

        通過對時間進行量化分析,可以得到系統(tǒng)的最大、最小時延,完成實時性驗證。

        4 模型驗證常用工具

        4.1 UPPAAL

        UPPAAL是丹麥Aalborg和瑞士Uppsala大學(xué)聯(lián)合開發(fā)[10],高效實用的基于時間自動機的實時系統(tǒng)模型驗證工具。UPPAAL特別適用于實時系統(tǒng)的安全性和活性的自動驗證。它將每個進程都描述為有限控制結(jié)構(gòu)、時鐘和變量組成的時間自動機,進程之間通過管道共享數(shù)據(jù)變量進行通信,管道用于保證不同自動機中的兩個轉(zhuǎn)換同時執(zhí)行。UPPAAL通過快速搜索機制來驗證時鐘約束和可達性,不僅可以有效地發(fā)現(xiàn)設(shè)計中出現(xiàn)的錯誤,而且可以清楚地顯示導(dǎo)致錯誤的判定路徑。

        UPPAAL擁有圖形用戶界面,主要包括三個部分:編輯器(Editor)、模擬器(Simulator)和驗證器(Verifier)。編輯器用于創(chuàng)建和編輯所要分析的系統(tǒng);模擬器用于模擬系統(tǒng)模型執(zhí)行過程可能出現(xiàn)的錯誤,以便在驗證前發(fā)現(xiàn)潛在的錯誤;驗證器通過快速搜索機制搜索系統(tǒng)的狀態(tài)空間、檢查時鐘約束和響應(yīng)限制性質(zhì)。

        UPPAAL體系結(jié)構(gòu)如圖3所示。

        UPPAAL的引入,簡化了實時系統(tǒng)驗證的工作量,并且增加了驗證系統(tǒng)的可靠性。首先,UPPAAL中時間自動機網(wǎng)絡(luò)中每個時間自動機都是相對獨立的,又是可以互相通信的,不需要構(gòu)造時間自動機的積,避免了構(gòu)造模型的繁雜。另外,UPPAAL中的模擬器從直觀上可以看到系統(tǒng)的運行過程,發(fā)現(xiàn)存在的問題,而驗證器又嚴格的從語義上保證了系統(tǒng)的安全性。UPPAAL在時間和空間上的性能顯著高于其他的實時驗證工具,能夠處理較為復(fù)雜的系統(tǒng)。

        4.2 NuSMV

        1987年左右,卡內(nèi)基梅隆大學(xué)在讀博士生McMillan開發(fā)出一個符號模型驗證器SMV(Symbolic Model Verifier),首次使用二叉決策圖(Binary Decision Diagram,BDD)來緩解狀態(tài)爆炸問題,實現(xiàn)了符號模型檢測技術(shù),SMV是第一個基于BDD的符號模型驗證工具[11]。2001年,Carnegie Mellon University(CMU)和Istitutoperla Ricerca Scientificae Techolgica(IRST)聯(lián)合開發(fā)出NuSMV( New Symbolic Model Verifier)[12],NuSMV支持計算樹邏輯(Computation Tree Logic,CTL)和線性時序邏輯(Linear Temporal Logic,LTL)描述的所有規(guī)范,作為一款比較成熟的模型檢測工具已經(jīng)發(fā)展到2.6.0版,NuSMV是開源工具,其源代碼和二進制文件可以在官網(wǎng)上獲取。

        作為一種通用的模型驗證器,NuSMV的基本運行原理:用戶使用NuSMV提供的輸入語言描述待驗證實時系統(tǒng)和約束性規(guī)范,通過NuSMV自動進行,驗證確定模型在規(guī)范中是否成立,若不成立輸出No,并給出反例,解析為什么規(guī)范在模型中不成立。NuSMV的運行原理如圖4所示。

        在功能上,NuSMV支持CTL描述規(guī)范,所以RTCTL同樣可以在NuSMV上得到驗證,NuSMV在實時驗證領(lǐng)域占有一席之地。

        在結(jié)構(gòu)上,NuSMV定義了一個良好的軟件系統(tǒng)架構(gòu),做到了模塊化和開放性,用戶可以自由定制模塊。

        在支持性上,NuSMV有豐富的文檔和開放的源碼,作為一種模型檢測的通用平臺,用戶可以在官網(wǎng)和開源社區(qū)獲得幫助。

        NuSMV的引入,明顯地簡化了實時系統(tǒng)驗證的工作量,研究者提供了更廣闊的研究空間[13]。

        4.3 PAT

        PAT[14]是由新加坡國立大學(xué)PAT研究小組自主開發(fā)的一套模型檢測工具,支持并發(fā)、網(wǎng)絡(luò)實時系統(tǒng)的建模驗證,能夠?qū)Χ喾N語言進行模擬驗證和反例生成。PAT是一個可擴展、模塊化的通用架構(gòu),其系統(tǒng)框架如圖5所示。

        框架分為四層,方便了模塊的擴展,建模驗證過程分為三步:編譯、抽象和驗證。PAT工具具有良好的擴展性,因此可以利用建模層的抽象功能對建模語言進行抽象,避免狀態(tài)爆炸。擴展PAT的并行模塊可以方便網(wǎng)絡(luò)系統(tǒng)的實時性的建模與驗證。抽象后的語言模塊能夠自動轉(zhuǎn)化為PAT已經(jīng)支持的語言,從而簡化系統(tǒng)描述和實現(xiàn)過程,使得建模過程更人性化、更易使用。借助PAT工具良好的擴展性,可方便對網(wǎng)絡(luò)系統(tǒng)進行實時性建模。

        4 結(jié)束語

        本文首先介紹了模型驗證的概念與當前的問題,并總結(jié)了三種網(wǎng)絡(luò)實時性模型的驗證方法和主流的實時性驗證工具,對其優(yōu)缺點進行了比較,為今后的研究提供有益參考。網(wǎng)絡(luò)安全領(lǐng)域的模型檢測技術(shù)應(yīng)用越來越廣泛。保障日益復(fù)雜的網(wǎng)絡(luò)空間的安全性,是當前研究的難題,建立在嚴格數(shù)學(xué)理論基礎(chǔ)之上的模型驗證必將在其中占據(jù)一席之地。

        參考文獻

        [1] 劉權(quán),王超.勒索軟件攻擊事件或?qū)⒁l(fā)網(wǎng)絡(luò)軍備競賽升級[J].網(wǎng)絡(luò)空間安全,2018,01:1-4.

        [2] 張修康,金春華,白瑩.應(yīng)對網(wǎng)絡(luò)安全威脅的技術(shù)演變[J].網(wǎng)絡(luò)空間安全,2018,01:46-50.

        [3] PETER PUSCHNER and A.Burns. Guest Editorial: A Review of Worst-Case Execution-Time Analysis, Real-Tim Systems, May 2000, 18(2-3): 115~128.

        [4] 張曦.基于WCET分析技術(shù)的程序?qū)崟r性模型檢驗方法研究[D].國防科學(xué)技術(shù)大學(xué),2012.

        [5] Alur R, Dill DL. A theory of t imed automat a[J] . Theoretical Computer Science, 1994, 126( 2) : 183- 235.

        [6] David A , Yi W . Hierarchical Timed Automat a for UPPAAL [ A ] .10th Nordic Workshop on Programming Theory ( NWPT) 98) [ C] .Turku Cent re f or Computer Science (T UCS) , Finland, 1998.

        [7] Michael Huth and Mark Ryan.Logic in Computer Science:Modelling and Reasoning about System,Second Edition.Cambridge University Press,2004.

        [8] E.M.Clarke and E.A.Emerson.Synthesis of synchronization skeletons for branching time temporal logic.In Logic of Programs:Workshop,Yorktown,Heights NY May 1981,volume 131 of LNCS.Springer-Verlag,1981.

        [9] Emerson E.A..Branching time temporal logic and the design of correct concurrent programs[Ph.D.dissertation].Harvard University,Cambridge,MA,1981

        [10] Behrmann G, David A, Larsen KG. A tutorial on UPPAAL. In: Bernardo M, ed. Proc. of the Formal Methods for the Design of Real-Time Systems. Springer-Verlag, 2004. 200?236. [doi: 10.1007/978-3-540-30080-9_7]

        [11] 張軍林,張治國.NuSMV模型驗證器實現(xiàn)與分析[D].中山大學(xué),2010.

        [12] CIMATTI A,CLARKE E,GIUNCHIGLIA F,et al.NuSMV: a new symbolic model verifier[C]Computer Aided Verification.Berlin: Springer,1999: 495-499.

        [13] 劉博,李蜀瑜.基于NuSMV的AADL行為模型驗證的探究[J].計算機技術(shù)與發(fā)展,2012,(2).

        [14] LIU Y, SUNJ, DONGJS.Developing model checkers using PAT[C]//8th International Symposium on Automated Technology for Verification and Analysis. Sydney: Springer Press, 2010:371-377.

        猜你喜歡
        實時性網(wǎng)絡(luò)安全
        網(wǎng)絡(luò)安全知多少?
        工會博覽(2023年27期)2023-10-24 11:51:28
        基于規(guī)則實時性的端云動態(tài)分配方法研究
        網(wǎng)絡(luò)安全
        網(wǎng)絡(luò)安全人才培養(yǎng)應(yīng)“實戰(zhàn)化”
        上網(wǎng)時如何注意網(wǎng)絡(luò)安全?
        基于虛擬局域網(wǎng)的智能變電站通信網(wǎng)絡(luò)實時性仿真
        航空電子AFDX與AVB傳輸實時性抗干擾對比
        一種滿足實時性需求的測發(fā)控軟件改進技術(shù)
        航天控制(2016年6期)2016-07-20 10:21:36
        網(wǎng)絡(luò)演算理論下的工業(yè)以太網(wǎng)的實時性分析
        我國擬制定網(wǎng)絡(luò)安全法
        聲屏世界(2015年7期)2015-02-28 15:20:13
        午夜影视免费| 网友自拍人妻一区二区三区三州 | 久久91精品国产91久久跳舞| 成人女同av在线观看网站| 亚洲熟妇av日韩熟妇在线| 亚洲综合网在线观看首页| 黄色三级视频中文字幕| 国产一区二区三区在线视频观看| 国产黄大片在线观看| 久久久久无码国产精品不卡| 青青青国产免A在线观看| 国产自拍91精品视频| 色偷偷亚洲第一成人综合网址| 狠狠爱无码一区二区三区| 女同成片av免费观看| 亚洲一区二区三区2021| 欧美一性一乱一交一视频| 亚洲无码专区无码| 青青草免费在线手机视频| 国产在线一区二区三精品乱码| 末发育娇小性色xxxx| 在线观看av手机网址| 青青草精品在线免费观看| 国产极品粉嫩福利姬萌白酱| 中国丰满大乳乳液| 国产杨幂AV在线播放| 精品一区二区三区婷婷| s级爆乳玩具酱国产vip皮裤| 香蕉视频毛片| 色综合久久五十路人妻| 国产无遮挡aaa片爽爽| 亚洲精品无码久久久久sm| 丰满少妇人妻无码超清 | 亚洲综合久久久中文字幕| 华人免费网站在线观看| 亚洲第一无码xxxxxx| 国产精品午夜波多野结衣性色| 亚洲美女一区二区三区三州| 久久人人爽爽爽人久久久 | 日本欧美大码a在线观看| 欧美丰满大乳高跟鞋|