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

论文摘要

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

论文目录

• 摘要
• ABSTRACT
• 第一章 引言
• 1.1 研究背景
• 1.2 论文主要工作
• 1.3 论文组织
• 第二章 SOCKET通信机制分析
• 2.1 TCP/IP协议
• 2.1.1 TCP/IP协议层次结构
• 2.1.2 socket通信系统调用
• 2.1.3 socket API功能介绍
• 2.2 SOCKET API形式化分析
• 2.2.1 定义
• 2.2.2 socket通信软件语义规则
• 第三章 模型检测技术及SOCKET通信程序性质规约
• 3.1 模型检测基本概念
• 3.1.1 基本术语
• 3.1.2 基本原理
• 3.2 模型检测工具SPIN
• 3.2.1 SPIN工作机理
• 3.2.2 Promela语言
• 3.2.3 线性时态逻辑（LTL）
• 3.3 模型检测使用例子
• 3.4 使用LTL描述SOCKET通信程序性质
• 第四章 从SOCKET通信程序抽取PROMELA验证模型
• 4.1 模型抽取过程概述
• 4.2 SOCKET函数调用序列抽取算法描述
• 4.2.1 解析器算法
• 4.2.2 解析器算法输出结果样例
• 4.3 模板定义
• 4.3.1 消息数据结构和通道定义
• 4.3.2 socket函数的Promela建模
• 4.3.3 socket函数到Promela语言的映射
• 4.4 目标模型生成器算法描述
• 4.4.1 模型生成器算法
• 4.4.2 目标模型样例
• 第五章 SOCKET通信程序分析系统及优化策略
• 5.1 系统概述
• 5.1.1 系统整体框架
• 5.1.2 系统功能
• 5.1.3 系统特点
• 5.2 SOCKET程序可靠性实例分析
• 5.2.1 死锁检测
• 5.3 系统优化策略
• 5.3.1 atomic
• 5.3.2 偏序规约
• 5.3.3 Bit-state hashing
• 5.3.4 验证效率
• 第六章 总结与展望
• 6.1 总结
• 6.2 进一步工作方向
• 致谢
• 参考文献
• 攻读学位期间发表的论文