基于CSP的网络隐蔽信道检测和分析技术研究

发布时间：2018-05-04 19:47

本文选题：网络存储隐蔽信道 + 通信顺序进程　；参考：《西安电子科技大学》2014年硕士论文

【摘要】：计算机网络技术是一把双刃剑，在给人们生活带来极大便利的同时，也带来了更多的网络安全问题。网络隐蔽信道是网络环境中一种泄露信息的入侵方式，它利用网络协议作为载体，通过把机密信息嵌入到网络协议首部特殊字段进行传输，对互联网造成极大的安全威胁。因此，分析网络协议和网络隐蔽信道的特点，，研究网络隐蔽信道的检测技术成为当前安全研究与应用领域的热点问题。目前，形式化方法和自动化验证技术在网络协议安全分析领域得到广泛应用。本文通过对网络协议和网络攻击者形式化描述，针对网络存储隐蔽信道的构建特性，提出一种基于CSP的形式化检测和分析模型。本文首先分析网络存储隐蔽信道的特点，为网络协议首部定义属性和隐蔽漏洞的概念。并根据属性定义，把网络协议首部划分为三种类型。然后提出一种基于CSP形式语言的网络存储隐蔽信道检测和分析通用模型，该模型对网络协议和攻击者进行语义描述，定义网络协议交互系统和网络存储隐蔽信道中的事件与基本进程，以及所要满足的安全约束。在网络协议的语义正确性的基础上，利用CSP中迹模型的提炼定义以及FDR检测工具，通过检测进程之间的提炼关系来对网络存储隐蔽信道进行检测和分析。最后，以TCP协议为例对模型进行建模验证，验证结果为检测到违反安全约束的反例序列，每条反例序列对应一个网络存储隐蔽信道攻击。该验证证明了CSP形式化模型的有效性和可用性。
[Abstract]:Computer network technology is a double-edged sword, which brings great convenience to people's life, but also brings more network security problems. Network covert channel is a kind of intrusion mode of leaking information in the network environment. It uses the network protocol as the carrier and embeds the confidential information into the first special field of the network protocol for transmission, which poses a great security threat to the Internet. Therefore, analyzing the characteristics of network protocols and network covert channels and studying the detection technology of network covert channels have become hot issues in the field of security research and application. At present, formal methods and automated verification techniques are widely used in the field of network protocol security analysis. Based on the formal description of network protocols and network attackers, a formal detection and analysis model based on CSP is proposed in this paper. This paper first analyzes the characteristics of network storage covert channel and defines the attributes and concealment vulnerabilities for the first part of network protocol. According to the definition of attributes, the first part of the network protocol is divided into three types. Then a general model of network storage covert channel detection and analysis based on CSP formal language is proposed. The model describes the network protocol and attacker semantically. Define the events and basic processes in the network protocol interaction system and the network storage covert channel, and the security constraints to be satisfied. On the basis of semantic correctness of network protocol, using the definition of trace model in CSP and the FDR detection tool, the hidden channel of network storage is detected and analyzed by the refining relation between the detection processes. Finally, the model is modeled and verified by using TCP protocol as an example. The result is that the counter case sequence of security constraint is detected, and each counter case sequence corresponds to a network storage covert channel attack. The validation proves the validity and availability of the CSP formal model.
【学位授予单位】：西安电子科技大学
【学位级别】：硕士
【学位授予年份】：2014
【分类号】：TP393.08

【参考文献】