基于安全属性建模的协议安全性测试理论与方法研究

This project will study the theory and method of protocol security testing. First, we mainly focus on the formalization of security attributes of protocols and study the mechanism of security attribute modeling based on Finite State Machine. Moreover, based on the fruit of research on semantics theory, the project will also study the semantics modeling of protocol behaviors and combine it with the security attributes formalization to set up a new modeling theory which could model the protocol time and behaviors characteristics simultaneously. Second, under the direction of this new modeling theory, taking advantage of inherent features of model checking, we will carry out a research on setting up constrained rules and guiding policies to meet highly variable security requirements, and then design the algorithms of generating experimental data for protocol security testing. Finally, in accordance with the different security requirements and protocol faults, the project will propose a new abstract method to represent testing results symbolically and set up the mapping relation between testing results and threat levels, and then build a unified and quantitative criterion for testing results assessment and a method for evaluation of security situation in order to make the testing results measurable and able to be controled, and strength the impact of security testing on the protection of protocol systems. We hope to make an important breakthrough in the field of protocol security testing and establish a more comprehensive and systemic theory and method to test security protocols efficiently and correctly.

本项目主要研究协议的安全性测试理论与方法。首先，重点关注协议"安全属性"的形式化方法，研究基于状态机理论模型的安全属性扩展建模机制；借鉴搜索领域的语义研究成果，研究协议行为的语义建模方法，并将两者有机结合，进一步研究安全属性扩展下的协议状态时序与行为语义的混合建模理论与方法；其次，在该混合建模理论的指导下，结合模型检测技术，建立适应于安全性测试需求动态变化的逻辑约束公式和检测规则，研究动态安全性测试例生成算法；最后，研究测试结果的抽象化方法，及其与安全威胁等级的关联方法，设计统一、定量的测试结果评价标准和安全态势评估方法，实现测试结果的可度量性和可控性，增强安全性测试结果对协议系统安全防护的指导功能。我们希望在协议的安全性测试理论和方法上有一定的突破，为高效、准确和可靠的协议安全性测试与评估探索和开拓系统的理论基础和指导方法。

作为网络和分布式系统的基石，协议的正确性决定了整个计算机网络及系统的稳固与安全。但协议实现因其固有的复杂性，必然会引入实现的不一致、漏洞或错误，这迫切需要能适应安全需求动态变化的测试方法来进一步验证协议。因此，本项目主要研究协议的安全性测试理论与方法。项目取得的主要成果包括：.1）提出了一种密码学可证明安全的且高效的数据所有权证明协议与测试方案，实现了对安全协议的安全属性进行了形式化建模，并实现了对模型化后的安全协议测试，结果表明效果良好。该成果发表在SCI检索源期刊上。.2）提出了一个新的基于客户端加密文件的去重复删除安全协议与测试方案，该方案基于扩展逻辑规则系统，建立新协议的动态安全需求和检查规则，支持多客户端加密文件的去重复删除场景。成果发表在SCI检索源期刊上，并申请了国家发明专利。.3）提出了一种新的基于语义的安全协议测试方法，并进行了实际系统测试将安全协议的语义进行形式化并与逻辑规则结合，并利用该方法发现了2个国内著名互联网公司新浪公司的“新浪微博APP”和“腾讯移动QQ”APP的在线认证协议的漏洞，也是首次将理论成果结合实际的安全协议测试获得的成果。该成果发表在国内最好的学术期刊之一《计算机学报》上，并申请了国家发明专利。.4）提出了协议认证性安全属性测试方法，设计了一种形式化安全属性的有限状态机扩展模型SPG-EFSM，精确定义了协议认证安全属性，实现了协议认证性攻击算法，结果表明：发现了广泛存在于Woo-lam协议及其各种更新版本当中的漏洞，以及μTESLA协议的认证漂移问题，并指出了它们潜在的安全性问题。该成果在安全协议的属性建模与安全性测试取得了实质性的突破，并将相关成果发表在了国内最好的学术期刊之一《电子学报》上，并正在申请国家发明专利。. 本项目在协议的安全性测试理论和方法上有一定的突破，为高效、准确和可靠的协议安全性测试与评估探索和开拓系统的理论基础和指导方法。