基于时态断言的迁移工作流实例安全研究

摘要

迁移工作流是近年来工作流管理研究的一个新方向。基于移动计算范型的迁移工作流管理系统包括工作流引擎、迁移实例和工作位置三个要素。工作流引擎完成工作流过程定义、迁移实例生成和多迁移实例协调等工作；工作位置包括停靠站服务器及其管理的工作机网络，是迁移实例的运行场所；迁移实例被定义为任务的执行体，它由工作流引擎生成，可以在工作位置之间迁移，并通过工作位置提供的本地资源和服务执行一项或多项任务，当它发现当前工作位置不能满足其执行任务的要求时，可以迁移到另一个能满足其要求的工作位置上继续执行。 与过程调用相比，迁移实例具有更强的自治性。它很好地解决了网络通信的瓶颈问题，增加了任务处理的并行程度，增强了系统的灵活性、可扩充性及容错能力。迁移实例技术已成为计算机网络和分布式系统最具活力的发展方向之一，但在复杂的网络环境下，对迁移实例的安全性提出了特殊要求。 本文在分析现有的保护迁移实例安全技术的基础上，利用时态逻辑可以处理含有时间信息的事件的命题和谓词的特性，设计了基于LTL、Java Annotation的安全检测机制。该机制属于事后检测，可辨别出针对迁移实例代码或状态的更改行为，从而判断迁移实例是否遭受攻击。 该方案首先分析了迁移实例在迁移过程中可能遭受的各种安全威胁，如非法窃听、篡改、伪造等，根据各种安全威胁的特点设计不同的安全断言，然后根据迁移实例生命周期图分析迁移实例的运行特点，使用运行约束断言定义相应的约束条件。当定义好需要验证的安全需求后，以@LTL注释(该注释说明了程序所需验证的时态断言)标记源程序并使用J-LO工具进行验证。实验表明，该方案可以有效检测迁移实例在运行过程中的安全状态，进一步完善了迁移实例的设计，提高了迁移工作流管理系统的安全性。但是在实时检测迁移实例安全状态的同时，不可避免的带来了系统性能的下降，因此迁移工作流管理系统如何在安全性、性能和成本之间取得平衡是应用发展不可缺少的基础。 迁移工作流是一种比较新的技术，在大规模、分布式、跨平台的应用中迁移实例有其独特的优势。但是由于目前迁移工作流技术尚未成熟，其管理、通信机制、移动以及安全等诸多方面需要进一步研究。随着研究的不断深入，迁移工作流管理系统的安全性问题也将得到逐步的解决。

目录

文摘

英文文摘

声明

第1章绪论

1.1课题研究背景和意义

1.2课题研究内容与现状

1.3论文创新点

1.4本文的组织结构

第2章时态逻辑

2.1模态逻辑概念

2.2时态逻辑

2.3线性时态逻辑

2.3.1线性时态逻辑操作符

2.3.2线性时态逻辑语义

2.3.3线性时态逻辑的应用

2.4计算树逻辑

2.5CTL*

2.6传统程序断言与时态断言

2.7本章小结

第3章迁移工作流管理系统

3.1工作流管理系统

3.1.1工作流概念

3.1.2工作流管理系统

3.1.3工作流管理系统的分类

3.1.4工作流技术的现状和发展趋势

3.2 Agent技术

3.2.1软件Agent概念

3.2.2移动Agent概念

3.2.3移动Agent的主要优点

3.3迁移工作流管理系统

3.3.1迁移工作流定义

3.3.2迁移工作流系统框架

3.3.3迁移实例的工作原理

3.4本章小结

第4章迁移实例安全检测

4.1迁移工作流管理系统的安全问题

4.2迁移实例的安全需求

4.3迁移实例面临的安全威胁

4.4迁移实例中的时态性

4.4.1上次迁移和执行结果的安全断言

4.4.2迁移实例中的时态性及其描述

4.5本章小结

第5章系统仿真

5.1 J-LO介绍

5.2 J-LO原理

5.3 J-LO的使用方法

5.4 J-LO测试实例

5.5本章小结

第6章结束语

参考文献

致谢

攻读硕士期间发表的学术论文目录