基于SPIN的SOCKET通信程序分析系统

摘要

形式化方法是验证并发系统可靠性和安全性的一种手段。模型检测是一种对有限状态并发(分布式)系统进行形式化验证的方法,已应用于软件可靠性和安全性验证。从用高级语言开发的并发软件系统中自动抽取模型,使用模型检测工具对所抽取的模型进行验证是模型检测技术领域中的一个研究热点。基于TCP/IP协议的socket(套接字)通信程序可靠性是互联网数据传输的重要基础。本文围绕socket通信程序(C语言开发)可靠性问题,研究基于模型检测工具SPIN的socket通信程序分析与验证技术,主要工作及成果有:
　　 1.分析socket通信程序中socket函数调用顺序正确性,即对已通过语法检查及编译,但由于服务和客户程序中socket函数调用顺序异常而导致的程序运行时潜在问题(死锁、内存泄漏、边界数据丢失及其它运行时错误)进行检测。
　　 2.针对socket函数调用顺序正确性问题,设计从socket程序源代码抽取模型方案。通过分析socket程序的顺序结构,提出socket通信程序中socket函数调用序列抽取算法;定义Prometa消息数据结构和通道;规约socket函数的Promela模型;定义socket函数到Promela映射规则;提出目标Promela模型生成算法,并对模型应满足的性质用线性时态逻辑(LTL)进行规约。
　　 3.采用原子序列atomic、偏序规约、Bit-statehashing等策略以提高验证效率,有效地压缩验证过程中的状态空间和存储空间。
　　 4.设计并实现socket通信程序分析系统,该系统能够对由于socket函数调用顺序不正确所产生的潜在问题进行检测,如果存在漏洞,系统能够以图形化方式再现代码执行轨迹。该系统具有抽象性、通用性、可扩展性、高效性、实用性,可作为socket通信程序设计人员的有效辅助工具。