基于時態(tài)斷言的遷移工作流實例安全研究.pdf

1、遷移工作流是近年來工作流管理研究的一個新方向?；谝苿佑嬎惴缎偷倪w移工作流管理系統(tǒng)包括工作流引擎、遷移實例和工作位置三個要素。工作流引擎完成工作流過程定義、遷移實例生成和多遷移實例協(xié)調(diào)等工作；工作位置包括?？空痉?wù)器及其管理的工作機(jī)網(wǎng)絡(luò)，是遷移實例的運(yùn)行場所；遷移實例被定義為任務(wù)的執(zhí)行體，它由工作流引擎生成，可以在工作位置之間遷移，并通過工作位置提供的本地資源和服務(wù)執(zhí)行一項或多項任務(wù)，當(dāng)它發(fā)現(xiàn)當(dāng)前工作位置不能滿足其執(zhí)行任務(wù)的要求時，可以

2、遷移到另一個能滿足其要求的工作位置上繼續(xù)執(zhí)行。 與過程調(diào)用相比，遷移實例具有更強(qiáng)的自治性。它很好地解決了網(wǎng)絡(luò)通信的瓶頸問題，增加了任務(wù)處理的并行程度，增強(qiáng)了系統(tǒng)的靈活性、可擴(kuò)充性及容錯能力。遷移實例技術(shù)已成為計算機(jī)網(wǎng)絡(luò)和分布式系統(tǒng)最具活力的發(fā)展方向之一，但在復(fù)雜的網(wǎng)絡(luò)環(huán)境下，對遷移實例的安全性提出了特殊要求。 本文在分析現(xiàn)有的保護(hù)遷移實例安全技術(shù)的基礎(chǔ)上，利用時態(tài)邏輯可以處理含有時間信息的事件的命題和謂詞的特性，設(shè)計了基

3、于LTL、Java Annotation的安全檢測機(jī)制。該機(jī)制屬于事后檢測，可辨別出針對遷移實例代碼或狀態(tài)的更改行為，從而判斷遷移實例是否遭受攻擊。 該方案首先分析了遷移實例在遷移過程中可能遭受的各種安全威脅，如非法竊聽、篡改、偽造等，根據(jù)各種安全威脅的特點設(shè)計不同的安全斷言，然后根據(jù)遷移實例生命周期圖分析遷移實例的運(yùn)行特點，使用運(yùn)行約束斷言定義相應(yīng)的約束條件。當(dāng)定義好需要驗證的安全需求后，以@LTL注釋(該注釋說明了程序所需驗

4、證的時態(tài)斷言)標(biāo)記源程序并使用J-LO工具進(jìn)行驗證。實驗表明，該方案可以有效檢測遷移實例在運(yùn)行過程中的安全狀態(tài)，進(jìn)一步完善了遷移實例的設(shè)計，提高了遷移工作流管理系統(tǒng)的安全性。但是在實時檢測遷移實例安全狀態(tài)的同時，不可避免的帶來了系統(tǒng)性能的下降，因此遷移工作流管理系統(tǒng)如何在安全性、性能和成本之間取得平衡是應(yīng)用發(fā)展不可缺少的基礎(chǔ)。 遷移工作流是一種比較新的技術(shù)，在大規(guī)模、分布式、跨平臺的應(yīng)用中遷移實例有其獨特的優(yōu)勢。但是由于目前遷移