基于时态逻辑的迁移实例运行时安全研究

摘要

迁移工作流是将移动Agent技术引入传统的工作流管理系统而得到的一种新的计算模式，是近年来工作流管理研究的一个新方向，具有很好的应用前景。 在基于移动计算范型的迁移工作流管理系统中，迁移实例（Migrating Instance，MI）是任务的执行主体。它由工作流引擎生成，可以在工作位置之间迁移，并利用工作位置提供的本地资源和本地服务执行所携带的任务，在当前工作位置不能满足其执行任务的需求时，可以迁移到另一个能满足其要求的工作位置上继续执行。 通过利用代码在网络节点间自主搜集和处理信息，移动Agent技术具有减少网络流量、适合于移动用户、有利于数据集成、具有并行机制等优点。基于移动Agent技术实现的迁移工作流系统可以在一定的程度上解决传统工作流系统目前在性能及应用上的不足。但以移动Agent为范型构造的迁移实例所具有的可迁移性带来的安全隐患也为迁移工作流系统安全提出了更大的挑战。因此，建立相应的安全机制以尽量减少安全隐患，成为迫切需要解决的问题。 在迁移工作流系统中，由于迁移实例的迁移所引发的安全问题可分为工作位置安全问题和迁移实例安全问题两类。其中，迁移实例的运行时安全保护技术是目前研究的热点和难点。在迁移工作流系统中，作为任务执行体的迁移实例无论是在迁移过程中还是在异地工作位置上的执行过程中都存在着代码、数据及状态被窃取或篡改的安全威胁。 基于以上研究背景，本文主要研究了迁移实例安全问题。分析了现有的迁移实例安全保护技术，建立了迁移实例业务过程中任务依赖和迁移实例生命周期的Petri网模型，研究了迁移实例运行过程中状态、事件、行为之间存在的时态逻辑约束规范；在此基础上，提出了一种基于LTL和AOP技术（AspectJ）的迁移实例运行时安全检测方案，并进一步构造了迁移实例运行时安全监控框架。运用该安全监控机制，迁移实例在运行过程中可自动检测出针对自身代码、数据或状态的篡改行为，实时上报迁移工作流管理引擎，针对不同情况，迁移实例可以自主采取应急动作，也可在迁移工作流管理引擎的指示下执行相应动作。该方法不仅提高了迁移工作流管理系统的安全性，还可通过状态、事件、行为的发生序列，还原程序的运行踪迹，进一步增强了迁移实例运行过程的可追踪性。 由于目前迁移工作流技术尚未成熟，其管理、通信机制、迁移以及安全等诸多方面需要进一步研究。随着研究的不断深入，迁移工作流管理系统的安全性问题也将逐步得到解决。

目录

文摘

英文文摘

声明

第1章绪 论

1.1课题研究背景和意义

1.2本文的工作与创新

1.2.1本文的研究工作

1.2.2本文的创新

1.3本文的组织结构

第2章时态逻辑与Petri网

2.1模态逻辑与时态逻辑

2.1.1模态逻辑

2.1.2时态逻辑

2.2线性时态逻辑

2.2.1线性时态逻辑操作符

2.2.2线性时态逻辑语义

2.2.3线性时态逻辑的应用

2.3 Petri网

2.3.1 Petri网的静态结构

2.3.2 Petri网的动态特征

2.4本章小结

第3章迁移工作流系统

3.1工作流管理系统

3.1.1工作流管理系统概念

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

3.2移动Agent技术

3.2.1移动Agent概念

3.2.2移动Agent在工作流系统中的应用

3.3迁移工作流的概念模型

3.3.1迁移工作流的定义

3.3.2迁移工作流系统框架

3.4迁移工作流系统安全

3.4.1迁移工作流系统中的安全问题

3.4.2迁移实例的安全需求

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

3.5本章小结

第4章迁移实例安全的时态逻辑描述

4.1 Petri网与时态逻辑结合的过程描述方法

4.2迁移实例业务过程的Petri网模型

4.3业务过程Petri网模型需求的时态逻辑描述

4.4迁移实例生命周期的Petri网建模及时态逻辑约束

4.5网上购书实例

4.6本章小结

第5章迁移实例运行时安全监控框架

5.1软件运行时验证与运行时监控

5.1.1软件运行时验证与模型检查

5.1.2软件运行时监控与运行时验证

5.2基于时态逻辑的迁移实例运行时安全监控框架

5.3基于时态逻辑的迁移实例运行时安全检测的实现技术

5.3.1 AspectJ的基本概念和语法

5.3.2 AspectJ语言的一个实验验证例

5.4本章小结

第6章结束语

参考文献

致谢

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