基于D3S的在線程序分析技術(shù)的研究.pdf

1、分布式系統(tǒng)的復(fù)雜性使人們在調(diào)試以及驗(yàn)證分布式系統(tǒng)時(shí)遇到了很多困難。雖然人們在測試和調(diào)試分布式系統(tǒng)方面付出了巨大的努力，然而一旦系統(tǒng)實(shí)際部署后，又會(huì)暴露出很多未能檢測出的系統(tǒng)異常行為。D3S系統(tǒng)是針對已部署的分布式系統(tǒng)的一個(gè)在線謂詞檢測系統(tǒng)。調(diào)試人員可以通過謂詞來描述分布式應(yīng)用程序需要滿足的屬性。當(dāng)分布式應(yīng)用程序?qū)嶋H運(yùn)行時(shí)，如果某些系統(tǒng)特性被違反，D3S能夠立即報(bào)告該漏洞的產(chǎn)生，同時(shí)提供相應(yīng)的信息以便于調(diào)試人員發(fā)現(xiàn)漏洞的根源。然而，通過對

2、微軟D3S系統(tǒng)的分析，本研究發(fā)現(xiàn)該系統(tǒng)有以下幾點(diǎn)不足：首先，手工輸入的謂詞檢測代碼相對繁瑣，且容易出錯(cuò)。其次，D3S的謂詞不具備高層的邏輯表達(dá)能力，尤其是難以表達(dá)應(yīng)用程序的時(shí)態(tài)特性。最后，D3S的謂詞檢測方法不能有效檢測系統(tǒng)的活性。該系統(tǒng)中的謂詞判斷基于有限數(shù)量的連續(xù)快照，因此在判斷系統(tǒng)活性時(shí)需要輔助信息才能有利于調(diào)試人員判斷漏洞的具體情況。因此，針對上述提到的3點(diǎn)不足，本文研究基于D3S的在線程序分析技術(shù)，在D3S系統(tǒng)的系統(tǒng)框架內(nèi)實(shí)現(xiàn)

3、了能夠監(jiān)控程序的時(shí)態(tài)特性的分布式程序監(jiān)控系統(tǒng)。監(jiān)控系統(tǒng)對D3S系統(tǒng)的改進(jìn)主要體現(xiàn)在以下幾個(gè)方面：首先，監(jiān)控系統(tǒng)采用的形式化方法有效彌補(bǔ)了D3S系統(tǒng)中復(fù)雜而且容易出錯(cuò)的謂詞檢測方式，同時(shí)形式化方法嚴(yán)格的數(shù)學(xué)推理增加了驗(yàn)證工作的可靠性。其次，監(jiān)控系統(tǒng)采用線性時(shí)態(tài)邏輯表達(dá)應(yīng)用程序的時(shí)態(tài)屬性，這能夠有效彌補(bǔ)D3S系統(tǒng)在描述程序時(shí)態(tài)屬性方面的不足。最后，監(jiān)控系統(tǒng)采用的有限路徑上的時(shí)態(tài)邏輯檢測算法使得監(jiān)控系統(tǒng)可以暴露出分布式應(yīng)用程序潛在的活性錯(cuò)誤，

4、這使得調(diào)試人員對于程序漏洞的檢測變得更加深入。 本文的創(chuàng)新主要集中在以下幾個(gè)方面：首先，利用D3S提供的能夠建立帶全局時(shí)間戳的全局狀態(tài)的功能，避免了計(jì)算分布式系統(tǒng)的計(jì)算格，因而將LTL 應(yīng)用到分布式系統(tǒng)的場景。其次，利用形式化變換，提出了一個(gè)有限自動(dòng)機(jī)模型以判定有限路徑語義下LTL公式的正確性。同時(shí)給出了嚴(yán)格的理論證明。最后，為D3S系統(tǒng)帶來了時(shí)態(tài)邏輯方面的高層次邏輯表達(dá)能力，同時(shí)通過對于Paxos協(xié)議時(shí)態(tài)特性的分析，利用監(jiān)控系

5、統(tǒng)找出了Paxos協(xié)議實(shí)現(xiàn)中一個(gè)非常重要的系統(tǒng)漏洞，進(jìn)一步證明了監(jiān)控系統(tǒng)的有用性。 本文主要介紹監(jiān)控系統(tǒng)的設(shè)計(jì)與實(shí)現(xiàn)。首先，介紹監(jiān)控系統(tǒng)的理論模型。其次，介紹監(jiān)控系統(tǒng)的構(gòu)架與實(shí)現(xiàn)。最后，通過案例和實(shí)驗(yàn)，闡明了監(jiān)控系統(tǒng)的應(yīng)用價(jià)值和實(shí)際效果。在監(jiān)控系統(tǒng)的設(shè)計(jì)中，將整個(gè)分布式系統(tǒng)建模成一個(gè)帶全局時(shí)間戳的一致性全局狀態(tài)序列。監(jiān)控系統(tǒng)采用線性時(shí)態(tài)邏輯作為系統(tǒng)規(guī)約的描述語言。為了在有限路徑上監(jiān)控程序的運(yùn)行，定義了有限路徑LTL的語法和語義，

6、并且利用形式化變換構(gòu)造了有限自動(dòng)機(jī)模型去判定有限路徑LTL語義下LTL公式的正確性。經(jīng)過嚴(yán)格的分析，證明了本文提出的有限自動(dòng)機(jī)恰好接收所有在有限路徑LTL語義下滿足相應(yīng)的LTL公式的路徑序列。監(jiān)控系統(tǒng)由前段的狀態(tài)發(fā)送器和后端的LTL驗(yàn)證引擎構(gòu)成，采用二進(jìn)制注入技術(shù)，狀態(tài)發(fā)送器被注入到應(yīng)用程序中以收集系統(tǒng)的運(yùn)行信息，LTL驗(yàn)證引擎按照系統(tǒng)的規(guī)約能夠?qū)斎氲南到y(tǒng)快照序列進(jìn)行時(shí)態(tài)邏輯判定。文中詳細(xì)介紹了系統(tǒng)的構(gòu)架以及各部分組件的實(shí)現(xiàn)細(xì)節(jié)。