项目名称: 面向新一代互联网协议的基于模型检测的协议安全性测试研究
项目编号: No.61202357
项目类型: 青年科学基金项目
立项/批准年度: 2013
项目学科: 计算机科学学科
项目作者: 王之梁
作者单位: 清华大学
项目金额: 24万元
中文摘要: 协议安全性测试的目的在于发掘协议实现潜在的缺陷或漏洞,考察协议实现对已知攻击的防御能力,尽可能发现协议的安全问题。新一代互联网对于协议的安全性要求更高,在新一代互联网协议研究的大背景下研究协议安全性测试具有重要的意义。模型检测是一种形式化的模型自动验证技术,基于模型检测的协议测试技术是很有前景的研究方向。本项目基于模型检测技术研究网络协议安全性测试,实现了整个测试过程的形式化和自动化。主要研究内容包括:(1) 研究基于模型检测的网络协议安全性测试的一般性框架;(2) 面向模型检测和安全性测试研究网络协议建模,集成协议行为描述、网络拓扑模型和攻击者模型,得到可用于模型检测的模型;(3) 研究模型检测序列到抽象测试例的转换方法,采用标准测试描述语言TTCN-3作为测试例描述语言,生成分布式TTCN-3测试例;(4) 对新一代互联网协议进行安全性测试,通过实例研究进一步证明理论方法的正确有效性。
中文关键词: 协议测试;安全性测试;模型检测;测试生成;新一代互联网协议
英文摘要: Protocol security testing aims to ensure the security of communication protocols, and can be used to detect vulnerabilities of protocol specifications and implementations, or to study the resistance ability of protocols against the well-known network attacks or malicious injections. Protocols in next generation Internet have more security requirements, so it is very important to study protocol security testing in the context of next generation Internet protocol. Model checking is a formal automatic verification technique, and protocol testing based on model checking is becoming a promising research direction. This project will study network protocol security testing based on model checking, formalizing and automating the whole testing process. In this project we will (1) study the generic framework of network protocol security testing based on model checking; (2) study protocol modeling methdology for model checking based security testing, by integrating protocol behavior description, network topology model and attacking model; (3) study the transformation from model checking sequences to abstract test cases, and generate distributed test cases by using standard testing language TTCN-3; (4) apply the method in real-life protocol security testing of next generation Internet protocol in order to demonstrate the co
英文关键词: Protocol Testing;Security Testing;Model Checking;Test Generation;Next generation Internet protocol