学位论文 > 优秀研究生学位论文题录展示

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

作　者: 杨志财
导　师: 郑晓娟
学　校: 东北师范大学
专　业: 计算机软件与理论
关键词: 移动代码携带模型代码手机开发平台形式验证
分类号: TP309.1
类　型: 硕士论文
年　份: 2011年
下　载: 16次
引　用: 0次
阅　读: 论文下载

内容摘要

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

全文目录

摘要  4-5
Abstract  5-6
目录  6-7
第一章绪论  7-13
  1.1 移动代码研究的背景和意义  7-8
  1.2 移动代码的国内外研究现状及存在问题  8-12
  1.3 本文的内容  12-13
第二章 MCC 方法和环境介绍  13-19
  2.1 携带模型代码 MCC 方法  13-15
  2.2 J2ME 简介  15-16
  2.3 手机的环境配置  16-19
第三章安全策略定义与 EFSA 模型  19-23
  3.1 安全策略规范描述  19-21
    3.1.1 事件  19-20
    3.1.2 模式  20
    3.1.3 响应措施 Action  20
    3.1.4 安全策略例子  20-21
  3.2 扩展有限状态自动机(EFSA)  21-23
第四章安全策略的验证  23-35
  4.1 程序行为模型(EPDA)  23-28
  4.2 关于 EFSA 与 EPDA 具备相同描述能力的证明  28-31
  4.3 验证算法  31-35
第五章系统实现  35-38
  5.1 系统结构图  35
  5.2 各部分功能介绍  35-38
第六章总结与不足  38-39
参考文献  39-41

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

内容摘要

全文目录

相似论文