安全策略的形式化描述及其可视化实现

摘要

非信任代码的安全执行是移动代码安全的重要问题之一。携带模型代码方法同时从移动代码的生产者和使用者的角度考虑，为安全执行非信任代码提供了一个系统、全面且有效的解决方案。该方法主要包括安全策略的定义、安全行为模型的生成，以及其验证和安全策略的强制实施。
　　本文以MCC模型为依据，为避免产生虚假路径采用扩展下推自动机(EPDA)来表示程序行为模型，未减少不确定性安全策略模型用基于事件的有限自动机(REE)和扩展有限状态自动机(EFSA)来表示。同时对这两种自动机的等价性给出一个形式化的证明，以及验证算法。最后，针对手机开发平台(J2ME)研究移动代码安全行为检测的形式验证及其支持工具的开发。

目录

声明

摘要

第一章 绪论

1．1 移动代码研究的背景和意义

1．2 移动代码的国内外研究现状及存在问题

1．3 本文的内容

第二章 MCC方法和环境介绍

2．1 携带模型代码MCC方法

2．2 J2ME简介

2．3 手机的环境配置

第三章 安全策略定义与EFSA模型

3．1 安全策略规范描述

3．1．1 事件

3．1．2 模式

3．1．3 响应措施Action

3．1．4 安全策略例子

3．2 扩展有限状态自动机(EFSA)

第四章 安全策略的验证

4．1 程序行为模型(EPDA)

4．2 关于EFSA与EPDA具备相同描述能力的证明

4．3 验证算法

第五章 系统实现

5．1 系统结构图

5．2 各部分功能介绍

第六章 总结与不足

参考文献