1. 引言

程序靜態(tài)分析（Program Static Analysis）是指在不運(yùn)行代碼的方式下，通過(guò)詞法分析、語(yǔ)法分析、控制流、數(shù)據(jù)流分析等技術(shù)對(duì)程序代碼進(jìn)行掃描，驗(yàn)證代碼是否滿足規(guī)范性、安全性、可靠性、可維護(hù)性等指標(biāo)的一種代碼分析技術(shù)[8]。 程序靜態(tài)分析的歷史幾乎與程序的歷史一樣長(zhǎng), 自從有了程序就有了程序分析。特別是隨著編譯技術(shù)的發(fā)展，大大帶動(dòng)了程序的自動(dòng)分析技術(shù)。目前靜態(tài)分析技術(shù)向模擬執(zhí)行的技術(shù)發(fā)展以能夠發(fā)現(xiàn)更多傳統(tǒng)意義上動(dòng)態(tài)測(cè)試才能發(fā)現(xiàn)的缺陷，例如符號(hào)執(zhí)行、抽象解釋、值依賴分析等等并采用數(shù)學(xué)約束求解工具進(jìn)行路徑約減或者可達(dá)性分析以發(fā)現(xiàn)更多的問(wèn)題、減少誤報(bào)、提高效率。

隨著程序的規(guī)模和復(fù)雜度越來(lái)越高，現(xiàn)代的程序分析的具體應(yīng)用中，對(duì)一個(gè)問(wèn)題的檢查往往不是單一個(gè)使用一種技術(shù)，而是會(huì)同時(shí)使用多種分析技術(shù)，采用多次迭代，反復(fù)求精的過(guò)程。 這就要求我們?cè)谠O(shè)計(jì)的時(shí)候能統(tǒng)一規(guī)劃，策略對(duì)待不同的問(wèn)題。就好比一個(gè)大廚，做每道菜，用什么材料，先放什么，后放什么，用什么火候，放多少都要把控的恰到好處。

這里我打算把這個(gè)技術(shù)介紹做成一個(gè)系列，探討靜態(tài)分析中的各種技術(shù)，希望通過(guò)這些介紹，能夠讓更多的程序員能夠投入到程序分析的行列來(lái)，一起進(jìn)行更深層次的軟件自動(dòng)化方面的探討和研究。

2. 關(guān)于符號(hào)執(zhí)行的一個(gè)故事

大家都喜歡聽(tīng)故事，這里先講一個(gè)和符號(hào)執(zhí)行相關(guān)的故事作為一個(gè)引子。

話說(shuō)一年一度的網(wǎng)絡(luò)安全行業(yè)盛會(huì)RSA大會(huì)，每年入選的創(chuàng)新沙盒十強(qiáng)，都會(huì)成為業(yè)界投資者的追捧，同時(shí)從這些項(xiàng)目中，我們也可以推斷出網(wǎng)絡(luò)安全技術(shù)創(chuàng)新的熱點(diǎn)方向。

今年的十強(qiáng)中有一個(gè)叫做Mayhem的產(chǎn)品，對(duì)于Mayhem這個(gè)名字，搞符號(hào)執(zhí)行的人恐怕并不陌生。

首先這個(gè)名字Mayhem讓人影響深刻，中文翻譯過(guò)來(lái)就是“混亂”，本來(lái)世界就夠亂的了，還把工具叫成“混亂”，真是"Complete mayhem"（全亂了）。

把和Mayhem有關(guān)的信息，按時(shí)間順序編排一下，就可以看到故事的主線：

• ForAllSecure成立于2012年，其技術(shù)源于卡耐基梅隆大學(xué)（CMU）研究獲得的專利技術(shù)；
•  從2012年到2017年，美國(guó)國(guó)防部(DoD)在幾乎所有正在開(kāi)發(fā)的關(guān)鍵武器系統(tǒng)中發(fā)現(xiàn)了漏洞。
• 《M國(guó)國(guó)防法》要求就加強(qiáng)關(guān)鍵系統(tǒng)的軟件安全性提出報(bào)告，建議在國(guó)防高級(jí)研究計(jì)劃局的“網(wǎng)絡(luò)大挑戰(zhàn)”下開(kāi)發(fā)二進(jìn)制分析和符號(hào)執(zhí)行工具;
• 2016年美國(guó)高等研究計(jì)劃署(DAPRA)主辦了自動(dòng)網(wǎng)絡(luò)攻防賽(CyberGrandChallenge)，旨在建立實(shí)時(shí)自動(dòng)化的網(wǎng)絡(luò)防御系統(tǒng)，并且能夠快速地應(yīng)對(duì)大量新的攻擊手法，以應(yīng)對(duì)頻發(fā)的網(wǎng)絡(luò)攻擊。符號(hào)執(zhí)行在參賽隊(duì)的自動(dòng)攻防系統(tǒng)中起到了舉足輕重的作用，被廣泛應(yīng)用在程序脆弱性的分析上?？▋?nèi)基梅隆大學(xué)ForAllSecure團(tuán)隊(duì)的Mayhem獲得了CGC的冠軍；
• 2018年，GAO-19-128號(hào)報(bào)告稱，由于武器系統(tǒng)的計(jì)算機(jī)化，武器系統(tǒng)比以往任何時(shí)候都更依賴軟件，也更加網(wǎng)絡(luò)化，為了使武器系統(tǒng)防范日益復(fù)雜的網(wǎng)絡(luò)安全攻擊，美國(guó)國(guó)防部(DoD)正在開(kāi)發(fā)更安全的武器系統(tǒng);

Mayhem是聯(lián)邦政府推薦的安全解決方案，用于連續(xù)，自動(dòng)化，準(zhǔn)確的測(cè)試;

美國(guó)國(guó)防部的多個(gè)實(shí)體都使用Mayhem，包括但不限于：空軍第96網(wǎng)絡(luò)空間測(cè)試小組，空軍第90網(wǎng)絡(luò)空間操作中隊(duì)，海軍海系統(tǒng)司令部（NAVSEA）和美國(guó)陸軍司令部，控制，通信，計(jì)算機(jī)，網(wǎng)絡(luò)，情報(bào)，監(jiān)視和偵察中心（C5ISR）。

Mayhem是ForAllSecure推出的輔助智能行為測(cè)試解決方案。它采用符號(hào)執(zhí)行自動(dòng)生成測(cè)試用例，然后通過(guò)模糊測(cè)試（fuzz）發(fā)現(xiàn)軟件缺陷。Mayhem將這兩種測(cè)試技術(shù)融合，集成在了DevOps中，持續(xù)的發(fā)現(xiàn)安全漏洞。

注: 從ForAllSecure的網(wǎng)站(https://forallsecure.com/government-and-defense)，可以得到上面的信息。

另：Mayhem[4]使用的是二進(jìn)制的符號(hào)執(zhí)行框架，屬于動(dòng)態(tài)分析的范疇，這里只是作為我們的一個(gè)引子，不必要糾結(jié)。

接下來(lái)，我們提綱絜領(lǐng)的介紹下符號(hào)執(zhí)行，讓大家明白這個(gè)技術(shù)的主要作用和面臨的挑戰(zhàn)，領(lǐng)大家入坑，更多的細(xì)節(jié)可以從后面的參考文獻(xiàn)中獲得。

3. 經(jīng)典的符號(hào)執(zhí)行技術(shù)

符號(hào)執(zhí)行[1]是一種靜態(tài)分析技術(shù)，它可以通過(guò)分析技術(shù)得到讓特定區(qū)域執(zhí)行的輸入。最初在1976年由King JC在ACM上提出。即通過(guò)使用抽象的符號(hào)代替具體值來(lái)模擬程序的執(zhí)行，當(dāng)遇到分支語(yǔ)句時(shí)，它會(huì)探索每一個(gè)分支, 將分支條件加入到相應(yīng)的路徑約束中，若約束可解，則說(shuō)明該路徑是可達(dá)的。符號(hào)執(zhí)行的目的是在給定的時(shí)間內(nèi)，盡可能的探索更多的路徑。根據(jù)運(yùn)行的目的來(lái)分，主要有兩個(gè)：

• 從測(cè)試的角度來(lái)看，它可以模擬出各個(gè)路徑的輸入值，從而創(chuàng)建高覆蓋率的測(cè)試套件。這里是靜態(tài)的分析程序得到測(cè)試需要的輸入，與動(dòng)態(tài)執(zhí)行程序的測(cè)試不同，動(dòng)態(tài)執(zhí)行程序的測(cè)試更多的是依賴完備的測(cè)試用例來(lái)提升測(cè)試的覆蓋率，達(dá)到發(fā)現(xiàn)問(wèn)題的目的。比如曾經(jīng)使用過(guò)的IBM的Purify 來(lái)檢測(cè)代碼的內(nèi)存泄露問(wèn)題。就需要人工的看代碼，編制大量的測(cè)試用例，然后通過(guò)讓程序執(zhí)行分別執(zhí)行這些輸入，來(lái)提高代碼的覆蓋率，從而盡可能的發(fā)現(xiàn)內(nèi)存泄漏的問(wèn)題。
• 從缺陷查找的角度來(lái)看，它為開(kāi)發(fā)人員提供了觸發(fā)的缺陷的具體輸入，利用該輸入，程序可用于缺陷的確認(rèn)或調(diào)試。符號(hào)執(zhí)行不僅限于查找諸如緩沖區(qū)溢出之類的問(wèn)題，而且可以通過(guò)根據(jù)缺陷發(fā)現(xiàn)的條件，生成復(fù)雜的斷言，來(lái)判斷缺陷發(fā)生的可能性。

這里舉一個(gè)經(jīng)典的例子[2]，來(lái)說(shuō)明符號(hào)執(zhí)行的具體過(guò)程。

int twice(int v){
       return 2*v;
   }

   void testme(int x, int y){
       z = twice(y);
       if (z == x){
           if (x > y+10)
               ERROR;
       }
   }

   int main(){
      x = sym_input();
      y = sym_input();
      testme(x, y);
      return 0;
   }

這段代碼中的函數(shù)testme()有三條執(zhí)行路徑。符號(hào)執(zhí)行的目的，就是在給定的時(shí)間預(yù)算內(nèi)，生成一組輸入，并通過(guò)這些輸入盡可能多的探索執(zhí)行路徑。

執(zhí)行路徑(execution path)：一個(gè)true和false的序列seq ={p0, p1, …, pn}。其中，如果是一個(gè)條件語(yǔ)句，那么pi=ture則表示條件語(yǔ)句的取值為：true，否則取false；

執(zhí)行樹(shù)(execution tree)：一個(gè)程序的所有執(zhí)行路徑則可表征成一棵執(zhí)行樹(shù)。

下圖是樣例代碼的執(zhí)行樹(shù)：

符號(hào)執(zhí)行通過(guò)維護(hù)符號(hào)狀態(tài)和路徑約束，以便在運(yùn)行過(guò)程中傳遞信息。

符號(hào)狀態(tài)(symbolic state)：符號(hào)執(zhí)行維護(hù)一個(gè)符號(hào)狀態(tài)σ，將變量映射到符號(hào)表達(dá)式。

符號(hào)路徑約束(symbolic path constraint)：符號(hào)路徑約束PC，它是符號(hào)表達(dá)式上無(wú)量詞的一階公式。

在執(zhí)行開(kāi)始時(shí)，將σ初始化為一個(gè)空映射，將PC初始化為true；

在符號(hào)執(zhí)行過(guò)程中，σ和PC都會(huì)更新。

在沿著程序執(zhí)行路徑的符號(hào)執(zhí)行結(jié)束時(shí)，使用約束求解器對(duì)PC進(jìn)行求解，以生成具體的輸入值。 如果程序在這些具體的輸入值上執(zhí)行，它將采用與符號(hào)執(zhí)行完全相同的路徑，并以相同的方式終止。

對(duì)于樣例代碼，具體的過(guò)程如下

初始化：初始化符號(hào)狀態(tài)σ為空，符號(hào)路徑約束PC為true；

在每個(gè)賦值v = e處，符號(hào)執(zhí)行都通過(guò)將 v 映射到σ(e)來(lái)更新σ，該映射是通過(guò)對(duì)當(dāng)前符號(hào)狀態(tài)求值, 而獲得的符號(hào)表達(dá)式。

例如：main（）函數(shù)的前兩行（第16-17行）的符號(hào)執(zhí)行導(dǎo)致σ= {x ->x0，y -> y0}，其中x0，y0是兩個(gè)初始不受約束的符號(hào)值；在執(zhí)行第6行之后，σ = {x ->x0，y ->y0，z -> 2y0}。對(duì)于每個(gè)條件語(yǔ)句：if（e） then S1 else S2。在第7行之后，分別創(chuàng)建了兩個(gè)符號(hào)執(zhí)行實(shí)例，分別具有路徑約束x0 = 2y0和x ≠ 2y0;在第8行之后，分別創(chuàng)建兩個(gè)具有路徑約束的符號(hào)執(zhí)行實(shí)例（x0 = 2y0）∧（x0 > y0 + 10）和（x0 = 2y0）∧（x0 ≤ y0 + 10）。“then”分支： PC被更新為PC ∧ σ(e)；“else”分支：生成一個(gè)新的PC', PC'被初始化為：PC∧¬ σ(e)；如果分支的狀態(tài)σ的PC可滿足，則符號(hào)執(zhí)行沿著分支繼續(xù)，否則路徑終止。
例如:如果一個(gè)符號(hào)執(zhí)行實(shí)例碰到了exit或error時(shí)，當(dāng)前符號(hào)執(zhí)行實(shí)例就會(huì)被終止，并利用一個(gè)現(xiàn)成的約束求解器來(lái)生成一個(gè)可滿足當(dāng)前路徑約束的賦值。三條路徑按照約束求解后，分別得到我們期望的三組輸入：{x=0, y=1}，{x=2, y=1}和{x=30,y=15}。若代碼中包含循環(huán)或遞歸結(jié)構(gòu)，且它們的終止條件是符號(hào)化的，則可能導(dǎo)致有無(wú)窮多條路徑。在實(shí)踐過(guò)程中，需要對(duì)路徑搜索設(shè)置一個(gè)限制，例如timeout，限制路徑數(shù)量，循環(huán)迭代次數(shù)或探測(cè)深度。

經(jīng)典的符號(hào)執(zhí)行有一個(gè)關(guān)鍵的缺點(diǎn)，若符合執(zhí)行路徑的符號(hào)路徑約束無(wú)法使用約束求解器進(jìn)行有效的求解，則無(wú)法生成輸入。

4. 現(xiàn)代符號(hào)執(zhí)行技術(shù)

經(jīng)典的符號(hào)執(zhí)行，過(guò)度的依賴了符號(hào)執(zhí)行的約束求解能力，這就限制了傳統(tǒng)符號(hào)執(zhí)行的能力發(fā)揮。很快大家發(fā)現(xiàn)在分析過(guò)程中，如果能加入具體值進(jìn)行分析，將大大簡(jiǎn)化分析過(guò)程，降低分析的難度和提升效率；但分析過(guò)程中，仍不可避免的還是需要將各種條件表達(dá)式，進(jìn)行符號(hào)化抽象后變成約束條件參與執(zhí)行。將程序語(yǔ)句轉(zhuǎn)換為符號(hào)約束的精度，對(duì)符號(hào)執(zhí)行所達(dá)到的覆蓋率以及約束求解的可伸縮性會(huì)產(chǎn)生重大影響。所以如何做好混合具體(Concrete)執(zhí)行和符號(hào)(Symbolic)執(zhí)行的能力的平衡，就成為現(xiàn)代符號(hào)執(zhí)行的關(guān)鍵點(diǎn)。

混合執(zhí)行測(cè)試（Concolic testing)[5][6]和執(zhí)行生成測(cè)試（Execution-Generated Testing (EGT)）[7]這兩種現(xiàn)代符號(hào)執(zhí)行的代表都是基于這個(gè)思想發(fā)展而來(lái)的。下面以混合執(zhí)行測(cè)試（Concolic testing)為例說(shuō)明下現(xiàn)代符號(hào)執(zhí)行的主要過(guò)程。

與經(jīng)典的符號(hào)執(zhí)行不同，由于混合執(zhí)行在整個(gè)執(zhí)行過(guò)程中，需要維護(hù)程序的具體狀態(tài)，因此其輸入需要初始具體值。 混合執(zhí)行測(cè)試從一個(gè)給定的輸入或隨機(jī)輸入開(kāi)始執(zhí)行程序，沿著執(zhí)行的條件語(yǔ)句在輸入上收集符號(hào)約束，然后使用約束求解推斷先前輸入的變化，以便引導(dǎo)程序接下來(lái)的執(zhí)行該走向哪一個(gè)執(zhí)行路徑。重復(fù)此過(guò)程，直到探索了所有執(zhí)行路徑，或者滿足用戶定義的覆蓋標(biāo)準(zhǔn)、時(shí)間設(shè)置到期為止。

混合執(zhí)行測(cè)試會(huì)同時(shí)維護(hù)兩個(gè)狀態(tài)：

• 具體狀態(tài)：映射所有有具體值的變量；
• 符號(hào)狀態(tài)：僅映射沒(méi)有具體值的變量。

對(duì)于樣例代碼，執(zhí)行過(guò)程如下：

• 混合執(zhí)行會(huì)生成一些隨機(jī)的輸入值，比如{x=22, y=7}，然后符號(hào)化和具體化地一起來(lái)執(zhí)行程序。
• 依據(jù){x=22, y=7}，程序在第7行，這個(gè)具體的執(zhí)行會(huì)走向else分支；符號(hào)執(zhí)行沿著執(zhí)行路徑會(huì)生成x ≠ 2y0的路徑約束；
• 混合測(cè)試將路徑約束中的連接（x ≠ 2y0）取反，生成一個(gè)新的約束x0=2y0，并求解得到測(cè)試輸入{x=2, y=1}。這個(gè)新的輸入會(huì)強(qiáng)制讓程序執(zhí)行then路徑。
• 依據(jù){x=2, y=1}，程序在第8行執(zhí)行else分支?；旌蠝y(cè)試會(huì)沿著具體執(zhí)行來(lái)進(jìn)行符號(hào)執(zhí)行，并生成路徑約束（x0 = 2y0）∧（x0 > y0 + 10）；
• 混合測(cè)試將路徑約束中的連接（（x0 > y0 + 10））取反，會(huì)生成一個(gè)新約束（x0 = 2y0）∧（x0 ≤ y0 + 10）的測(cè)試，求解得到測(cè)試輸入{x=30, y=15}。在這個(gè)輸入下程序走到ERROR語(yǔ)句。
• 混合測(cè)試報(bào)告所有被探索的執(zhí)行路徑，并終止測(cè)試輸入的生成。

比較混合執(zhí)行測(cè)試和傳統(tǒng)的符號(hào)執(zhí)行，不難發(fā)現(xiàn)由于具體值的引入，簡(jiǎn)化了約束求解的難度。

5. 主要挑戰(zhàn)和解決方案

符號(hào)執(zhí)行技術(shù)已經(jīng)有了40多年的發(fā)展，在2017年8月Google學(xué)術(shù)中，標(biāo)題中帶有“符號(hào)執(zhí)行”的文章有742篇[3]，到2020.11月，文章數(shù)上升到1490, 可見(jiàn)符號(hào)執(zhí)行有了飛速的發(fā)展。但程序的復(fù)雜性和規(guī)模也在飛速的發(fā)展，符號(hào)執(zhí)行仍然存在路徑爆炸（代碼規(guī)模、復(fù)雜度）、約束求解（計(jì)算算法）、內(nèi)存模型（工具設(shè)計(jì)）等挑戰(zhàn)。

5.1. 路徑爆炸(Path Explosion)

符號(hào)執(zhí)行在過(guò)程處理中默認(rèn)已經(jīng)過(guò)濾了以下兩種路徑：

不依賴于符號(hào)輸入的路徑；

對(duì)于當(dāng)前的路徑約束，不可解的路徑。 但是，盡管符號(hào)執(zhí)行已經(jīng)做了這些過(guò)濾，路徑爆炸依舊是符號(hào)執(zhí)行的最大挑戰(zhàn)。路徑爆炸不是符號(hào)執(zhí)行特有的挑戰(zhàn)，是整個(gè)程序分析都需要考慮的最大的問(wèn)題。

解決路徑爆炸的方案，可以從以下兩個(gè)角度來(lái)考慮：

減少路徑總數(shù)（優(yōu)先的考慮最有希望的路徑， 路徑合并，剪枝）；

相似的路徑不再分析（函數(shù)摘要，緩存）；

依據(jù)這個(gè)思路業(yè)界提出了兩種解決方案。

啟發(fā)式（Heuristic)： 大多數(shù)啟發(fā)式方法側(cè)重于實(shí)現(xiàn)較高的語(yǔ)句和分支覆蓋率。

1. 特別有效的方法是使用靜態(tài)控制流圖（CFG）來(lái)指導(dǎo)探索，向最接近的路徑或優(yōu)先選擇先前執(zhí)行次數(shù)最少的語(yǔ)句；

2. 在每個(gè)可行的符號(hào)分支，隨機(jī)選擇要探索的一側(cè)； 或者將符號(hào)檢驗(yàn)與隨機(jī)檢驗(yàn)進(jìn)行交錯(cuò)進(jìn)行；

3. 采用先驗(yàn)知識(shí)，探索以往容易出錯(cuò)的函數(shù)；目前也有研究通過(guò)AI的方式得到這些推薦的分析路徑；

利用完善的程序分析技術(shù)(Sound program analysis techniques): 這種方法主要是使用程序分析和軟件驗(yàn)證中的各種思想，以合理的方式降低路徑探索的復(fù)雜性。

1. 靜態(tài)地合并路徑，然后再求解；

2. 通過(guò)函數(shù)摘要，緩存或重用已經(jīng)計(jì)算過(guò)的信息用于后續(xù)的計(jì)算中；

3. 通過(guò)剪枝，去除無(wú)關(guān)的變量對(duì)路徑的求解的影響；

5.2. 約束求解(Constraint Solving)

盡管在過(guò)去的幾年中，約束解決方案技術(shù)取得了長(zhǎng)足的進(jìn)步，但約束求解是符號(hào)執(zhí)行的技術(shù)瓶頸。

減少不相關(guān)的約束(Irrelevant constraint elimination) 符號(hào)執(zhí)行中的絕大多數(shù)查詢是為了確定某個(gè)分支的可行性，一種有效的優(yōu)化方法是從路徑條件中刪除與當(dāng)前分支的結(jié)果無(wú)關(guān)的那些約束。

增量求解(incremental solving) 符號(hào)執(zhí)行期間生成的約束集的一個(gè)重要特征是，它們根據(jù)來(lái)自程序源代碼的一組固定的靜態(tài)分支來(lái)表示。因此，許多路徑具有相似的約束集，因此可以采用相似的解決方案。

1. 通過(guò)重用先前類似查詢的結(jié)果，來(lái)提高約束求解的速度；

2. 通過(guò)約束集的超集，減少無(wú)解的情況出現(xiàn)； 我們目前常用的符號(hào)執(zhí)行的工具KLEE，在設(shè)計(jì)中都采用了著兩種方式。

5.3. 內(nèi)存建模(Memory Modeling)

在符號(hào)執(zhí)行中我們將變量映射到了一個(gè)內(nèi)存模型，來(lái)表示這個(gè)變量的類型、值或者值域。這個(gè)對(duì)變量的抽象模式對(duì)程序語(yǔ)句轉(zhuǎn)化成符號(hào)約束的精度和對(duì)符號(hào)執(zhí)行的覆蓋率有著很大的影響。太過(guò)精確，往往容易陷入復(fù)雜的計(jì)算，而不能得到具體的解；太過(guò)籠統(tǒng)，又會(huì)造成漏報(bào)。所以精度和可擴(kuò)展性之間是需要權(quán)衡的。

目前這個(gè)權(quán)衡的主要參考依據(jù)是：

1. 具體分析問(wèn)題的性質(zhì)；

2. 采用的約束求解器的限制；

6. 符號(hào)執(zhí)行工具

下面列舉了我們常用的符號(hào)執(zhí)行工具作為大家的參考。

7. 結(jié)束語(yǔ)

目前符號(hào)執(zhí)行，在實(shí)際的應(yīng)用中還主要用于與fuzz結(jié)合使用，用于縮小fuzz的取值范圍。由于符號(hào)執(zhí)行的主要瓶頸--約束求解的性能和局限性，并未在靜態(tài)分析的商業(yè)工具中，大規(guī)模的使用。但我們有理由相信，在不久的將來(lái)隨著并行技術(shù)、計(jì)算性能的提升、以及求解器的優(yōu)化，符號(hào)執(zhí)行能夠在靜態(tài)分析中發(fā)揮越來(lái)越大的作用。

以上就是詳解靜態(tài)分析技術(shù)符號(hào)執(zhí)行的詳細(xì)內(nèi)容，更多關(guān)于靜態(tài)分析技術(shù)符號(hào)執(zhí)行的資料請(qǐng)關(guān)注腳本之家其它相關(guān)文章！

最新評(píng)論