论文部分内容阅读
目前,安全协议的代码实现仍然主要依赖于手工编码,但手工编码低效、易错,容易引入各种漏洞,也不利于安全协议的修订和更新。人们对安全协议的代码自动化实现还未开展广泛和深入的研究,已有的工作也存在诸多不足。针对这些问题,本文提出了一个安全协议多目标语言代码自动化实现方案。首先,设计了一个安全协议XML形式化描述方法,完成抽象协议与XML描述之间的映射。其次,提出了一个可复用的面向对象协议代码框架,为安全协议的运行提供了一个基本的支撑。最后,开发了一个解析器,将安全协议的XML描述转化为多目标语言实现。为了增强协议及生成代码的安全性和健壮性,本文从两个方面着手:(1)在协议设计方面。在代码自动化实现前,将安全协议XML描述转换为CAPSL语言描述,进而利用现有形式化验证工具分析协议安全性,以发现和避免一些协议设计方面的缺陷和攻击;(2)协议实现方面。安全协议中常见的并行会话攻击和类型攻击,在编码阶段存在切实可行的防止方法,本文在方案中提出并实现了这些方法,从而避免了这两种攻击。同手工编码实现相比,该方案可以提高协议开发效率,缩短协议开发周期,节约大量手工成本,减少编程人员的工作量,避免一些代码缺陷,提高代码的安全性和健壮性。该方案也适合分布式系统中安全协议的部署和更新。同已有的方案相比,该方案在通用性、算法可选择性、可扩展性、用户是否需要形式化知识、多目标语言支持、避免代码缺陷等方面具有明显的优势。