QQ客服 官方微博 反馈留言

题名	密码模块API形式化分析技术研究
作者	刘波
学位类别	硕士
答辩日期	2013-05
授予单位	中国科学院大学
授予地点	北京
导师	陈华
学位专业	信息安全
中文摘要	由于信息安全需求的不断增加，密码模块得到了越来越广泛的应用，对密码模块的安全性分析也越来越受到人们的重视。密码模块API作为密码模块对外提供密码服务的唯一接口，它的安全性关系着整个密码模块，乃至整个信息系统的安全性。密码模块API的安全性分析在过去十多年间逐渐受到人们的重视。早期，人们主要通过单纯的手工分析来判别密码模块API中的安全漏洞。但是手工分析的方法复杂、繁琐且容易出错。后来，人们将安全协议的形式化分析方法引入到对密码模块的安全性分析当中，出现了众多自动化分析方法和技术，形式化方法也逐渐成为分析密码模块API安全性的重要方法。形式化分析方法的主要思想是，首先对密码模块API建立对应的形式化模型，然后利用定理证明或者模型检测等算法来判断建立的模型是否满足安全目标。形式化模型的正确建立直接影响分析的效率及最后的结果。模型检测作为形式化分析方法的一种，较之其他方法，自动化程度更高，攻击结果更直观。本文的研究重点集中于基于项重写的密码模块API形式化建模方法，所作工作主要分为两个部分： 1. 基于项重写形式化模型的建模方法、检测算法研究。针对密码模块API的形式化建模存在众多方法，而基于项重写的形式化模型有着独到的优势，它结合了API的特点，模型简洁易懂，建模方法简单，克服了模型中存在全局易变状态的问题，并在理论上给出了可判定性证明。本文针对密码模块API的形式化验证，提出了一种基于项重写形式化模型的检测算法，该算法利用符号化及广度优先搜索方法，使用项重写规则对敌手的初始知识集不断进行匹配和扩展，直到找到攻击路径或者搜索完状态空间。该算法在搜索攻击的过程中利用匹配的规则动态生成新项及状态节点，在搜索攻击的效率上相比使用模型检测工具NuSMV的方法大大提高。同时，该算法直接以建立的API命令的项重写规则为输入，不用将其转化为其他的输入模型，大大简化了建模分析的过程。 2. 基于提出的检测算法实现了检测分析工具，并对密码模块API标准PKCS#11进行了形式化验证。PKCS#11是目前在密码模块中广泛使用的一种API标准，直接应用于智能卡、智能密码钥匙等密码模块中。本文的验证实验主要涉及PKCS#11的密钥管理部分的API命令。实验中我们通过修改PKCS#11的初始化配置来寻找针对PKCS#11的API攻击或者安全配置。实验结果表明，本文的检测工具能够有效检测到针对PKCS#11的攻击，并找到一个新的攻击序列，搜索攻击的效率大大提高。
英文摘要	Due to  increasing requirements for information security, cryptographic modules have been  widely used, and more and more attention has been paid to the security analysis of cryptographic modules. The cryptographic module API is the only interface through which cryptographic modules provide cryptographic services. Its security  is important   for cryptographic modules, and even for  whole information system.The  security analysis of cryptographic module APIs has been paid  much attention gradually in the past few years. In  early days, the security analysis of cryptographic module APIs was mostly completed by conducting a detailed inspection of all instructions by hand. But the manual inspection is complicated, cumbersome and error-prone. Later on,  formal analysis of security protocols was introduced to the security analysis of cryptographic module APIs. There are many formal methods for the security analysis of  cryptographic module APIs, and formal methods  also become more and more  important and useful. The main idea of  formal analysis is that we first build  corresponding formal models for cryptographic module APIs, and then use theorem provers or model checking tools to verify whether  the model satisfies  security objectives. The established formal model  for cryptographic module APIs has a direct impact on the efficiency of analysis and final results. Model checking  is of higher degree of automation compared to other methods, and   results of attacks are intuitive. Our research of this paper focuses on the term rewriting formal model for cryptographic  module APIs. Our work  is divided into two main parts as following: 1. The modeling and the verification algorithm for  cryptographic module APIs using term rewriting formal model. There are a number of methods for the formal modeling of cryptographic module APIs, but  term rewriting formal model have unique advantages. It uses  features of  cryptographic module APIs, and  is simple and easy for  modeling and understanding. Furthermore, it solves  the non-monotonic global state  problem and proves the decidability of the model. In this paper, we propose a new verification algorithm which  is   especially designed for  the  term  rewriting  formal  model. The main idea is to  search  all  the  API commands sequence  with   symbolic  method and  breath-first  search. The search will not stop until an attack path has been found or all the finite state space has been searched. The algorithm generates terms dynamically during the search, which greatly improves the efficiency of searching attacks compared to the way of using NuSMV. Furthermore, the algorithm uses rewriting rules of  APIs as inputs, simplifying the process of modeling without conversion to other input models. 2. We implement a verification tool for security analysis of cryptographic module APIs based on our algorithm,  and use the tool verify the cryptographic module API standard PKCS#11. PKCS#11 is a widely used cryptographic module API standard, and is directly used in smart cards, USB tokens, etc. The experiments  mainly involves  the formal verification of PKCS#11 key management APIs. In the experiments, we change the initial configuration to find different attacks or secure  configurations. The experimental results show that, our tool can find  attacks against PKCS#11  effectively, and a new attack sequence is discovered. Furthermore, the efficiency  for searching attacks  is significantly improved.
公开日期	2013-05-27
内容类型	学位论文
源URL	[http://ir.iscas.ac.cn/handle/311060/14770]
专题	软件研究所_信息安全国家重点实验室_学位论文
推荐引用方式 GB/T 7714	刘波. 密码模块API形式化分析技术研究[D]. 北京. 中国科学院大学. 2013.

个性服务

查看访问统计

相关权益政策

暂无数据

收藏/分享

除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。