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

1、遷移工作流是近年來工作流管理研究的一個新方向。基于移動計算范型的遷移工作流管理系統(tǒng)包括工作流引擎、遷移實例和工作位置三個要素。工作流引擎完成工作流過程定義、遷移實例生成和多遷移實例協(xié)調(diào)等工作；工作位置包括停靠站服務器及其管理的工作機網(wǎng)絡，是遷移實例的運行場所；遷移實例被定義為任務的執(zhí)行體，它由工作流引擎生成，可以在工作位置之間遷移，并通過工作位置提供的本地資源和服務執(zhí)行一項或多項任務，當它發(fā)現(xiàn)當前工作位置不能滿足其執(zhí)行任務的要求時，可以

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

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

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