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

基于信息流分析的安全系统验证

作　者: 陈波
导　师: 赵??
学　校: 中国科学技术大学
专　业: 计算机软件与理论
关键词: 非干扰信息流分析弱互拟安全协议部分模型检查
分类号: TP393.08
类　型: 博士论文
年　份: 2007年
下　载: 523次
引　用: 1次
阅　读: 论文下载

内容摘要

计算机和网络技术的迅猛发展，导致对计算机系统和开放式的网络系统的攻击日益增多。系统和网络之所以会受到各种各样的攻击，究其原因，最根本的是系统和网络内部存在各种安全缺陷。为此，人们设计了各种各样的安全策略、安全模型来确保系统的安全性，并使用密码协议来保证网络通信的安全。在这些安全策略应用到系统之前，我们必须验证它们是否能够满足其“声称”的安全目标；同样，我们也要对密码协议进行分析，检验其是否存在潜在的、未知的安全漏洞。不管是直接的或间接的机密数据泄露，都可以看作是信息的非法流动，因此可以采用信息流分析的方法，找出系统或网络中潜在的各种安全问题。信息流分析方法是信息安全领域较为本质的一种方法。本文首先介绍了非干扰信息流分析的一般方法，即非确定系统中的信息流非干扰分析技术；然后研究了概率系统和安全协议中的信息流性质，以及这些安全性质的验证方法；本文的主要创新工作如下：1．基于非干扰信息流分析的概率系统安全验证方法实际系统中，攻击者可以通过对系统行为观察进行统计，然后根据统计的概率数据构建概率隐蔽通道，导致机密数据的间接泄露。因此，本文在概率配置下研究了系统的安全性。首先本文对非确定系统中的分析工具SPA进行扩展，得到PSPA，用以描述概率系统的行为。本文提出了P_PBNDC性质，并讨论了其在动态概率环境下的适用性，也给出了其不同语义等价下的特征描述，以及基于展开条件的特征描述。本文在P_PBNDC性质的基础上，提出了S_PBNDC和CP_PBNDC性质，这些都是PBNDC性质的充分条件。本文还给出了这些PBNDC类性质之间的关系。这些分析是很有意义的，因为本文提出的这些概率系统中的信息流安全性质能够暴露出那些非确定系统信息流安全性质无法暴露出的系统安全缺陷。2．基于环境敏感信息流分析的安全协议验证方法为了能够描述安全协议的行为，我们对SPA进行扩展，形成了CryptoSPA。本文在CryptoSPA的环境敏感标记转换系统语义模型下，定义了环境敏感的路径等价和弱互拟等价关系，并提出了基于环境知识的一般组合上不可演绎的性质框架ESGNDC_?^α。在此框架下，讨论了NDC^σ、BNDC^σ以及P_PBNDC_σ性质。本文还在ESGNDC_?^α框架下，讨论了安全协议中的机密性，认证性和公平性，并指出了此框架也适合安全协议的活性分析。3．通过模型检查验证信息流性质BNDC类性质的定义中都有全程量词，因此验证一个系统具有这些性质是非常困难的。本文使用部分模型检查的方法来对BNDC类性质进行验证。首先通过SPA来描述系统的行为，对于某一特定的BNDC类性质，通过一些处理手段，将其定义转换为（E|Top_E）＼H≈E＼H。这样，我们首先求出进程E＼H的特征公式φ，其中φ是模态μ演算的公式；那么证明进程满足BNDC性质就变为验证（E|Top_E）＼H是否满足特征公式φ。同时本文还提出了安全协议分析中信息流性质的一般化分析，基于这种分析，我们使用的模型检查的方法完全适用于安全协议信息流性质的验证中。

全文目录

摘要  5-7
Abstract  7-12
图目录  12-13
表目录  13-14
第一章绪论  14-28
  1.1 研究背景  14-18
    1.1.1 信息系统面临的安全威胁  15-18
      1.1.1.1 操作系统面临的安全威胁  15-16
      1.1.1.2 网络系统面临的安全威胁  16-18
  1.2 研究现状  18-25
    1.2.1 访问控制策略  19-22
      1.2.1.1 自主访问控制策略  19-20
      1.2.1.2 强制访问控制策略  20-22
    1.2.2 安全模型  22-23
      1.2.2.1 Bell-Lapadula模型  22-23
      1.2.2.2 Biba模型  23
      1.2.2.3 其他模型  23
    1.2.3 安全协议形式化分析方法  23-24
    1.2.4 基于非干扰的信息流分析方法  24-25
  1.3 研究目的和方案  25-26
  1.4 论文结构  26-28
第二章信息流分析的一般方法  28-51
  2.1 安全进程代数SPA  28-35
    2.1.1 SPA语法  28-30
    2.1.2 SPA的操作语义和等价关系  30-34
    2.1.3 值传递SPA  34-35
  2.2 非干扰模型  35-38
  2.3 非确定系统中的信息流安全性质  38-44
    2.3.1 基于路径等价的性质  38-40
    2.3.2 基于观察等价的性质  40-44
  2.4 BNDC性质的进一步分析  44-50
    2.4.1 坚持BNDC  44-46
    2.4.2 BNDC的一般化分析  46-48
    2.4.3 强BNDC、前进P_PBNDC  48-50
  2.5 小结  50-51
第三章概率系统中的信息流安全验证  51-75
  3.1 概率系统安全问题  51-53
  3.2 概率安全进程代数PSPA  53-58
    3.2.1 生成-反应转换系统  53-54
    3.2.2 PSPA的语法  54-56
    3.2.3 PSPA的操作语义  56-58
  3.3 概率进程间的观察等价  58-60
  3.4 概率系统的信息流安全性质  60-70
    3.4.1 概率非干扰  60-61
    3.4.2 概率互拟组合不可演绎性质  61-63
    3.4.3 持久PBNDC  63-68
      3.4.3.1 持久PBNDC的定义  63-64
      3.4.3.2 动态环境下的P_PBNDC性质  64-65
      3.4.3.3 P_PBNDC性质的讨论  65-68
    3.4.4 强PBNDC  68-69
    3.4.5 组合PBNDC  69-70
  3.5 实际系统的例子  70-74
  3.6 小结  74-75
第四章基于信息流分析的安全协议验证  75-100
  4.1 安全协议中的非干扰  75-82
    4.1.1 安全协议分析  75-77
    4.1.2 安全协议中的非干扰  77-79
    4.1.3 NDC的一般化框架  79-82
  4.2 CryptoSPA演算  82-86
    4.2.1 CryptoSPA演算的语法  82-84
    4.2.2 CryptoSPA演算的语义  84-86
  4.3 环境敏感语义  86-90
    4.3.1 环境敏感标签转换系统  86-87
    4.3.2 配置间的路径和弱互拟等价  87-88
    4.3.3 进程间的环境敏感等价  88-90
  4.4 安全协议性质分析  90-99
    4.4.1 环境敏感的GNDC  90-91
    4.4.2 组合上的不可演绎性质  91-94
    4.4.3 ESGNDC_(?)~α框架下的协议安全性质分析  94-96
      4.4.3.1 机密性分析  95
      4.4.3.2 一致性分析  95-96
      4.4.3.3 公平性分析  96
    4.4.4 一个安全协议分析的实例  96-99
  4.5 小结  99-100
第五章安全性质的证明技术  100-114
  5.1 使用模型检查技术验证安全性质  100-109
    5.1.1 模态μ演算和方程μ演算  101-105
      5.1.1.1 模态μ演算  101-104
      5.1.1.2 方程μ演算  104-105
    5.1.2 进程的特征方程系统  105-106
    5.1.3 部分模型检查  106-107
    5.1.4 验证BNDC性质  107-108
    5.1.5 一般化的特征方程系统  108-109
  5.2 ESGNDC_(?)~α性质的验证  109-113
    5.2.1 环境敏感弱互拟语义的一般化分析  110-112
    5.2.2 s_BNDC~σ性质分析  112-113
      5.2.2.1 Strong BNDC~σ性质  112
      5.2.2.2 Progressing P_PBNDC~σ性质  112-113
  5.3 小结  113-114
第六章结束语  114-118
  6.1 论文工作总结  114-116
    6.1.1 概率系统中的信息流安全性质  115
    6.1.2 基于环境敏感非干扰的安全协议分析  115-116
    6.1.3 部分模型检查验证NDC类性质  116
  6.2 进一步的工作  116-118
参考文献  118-129
读博期间发表的论文  129
读博期间参加的科研项目  129-131
致谢  131

基于信息流分析的安全系统验证

内容摘要

全文目录

相似论文