本文選題：網(wǎng)絡(luò)存儲隱蔽信道 + 通信順序進(jìn)程��； 參考：《西安電子科技大學(xué)》2014年碩士論文

【摘要】：計(jì)算機(jī)網(wǎng)絡(luò)技術(shù)是一把雙刃劍，在給人們生活帶來極大便利的同時(shí)，也帶來了更多的網(wǎng)絡(luò)安全問題。網(wǎng)絡(luò)隱蔽信道是網(wǎng)絡(luò)環(huán)境中一種泄露信息的入侵方式，它利用網(wǎng)絡(luò)協(xié)議作為載體，通過把機(jī)密信息嵌入到網(wǎng)絡(luò)協(xié)議首部特殊字段進(jìn)行傳輸，對互聯(lián)網(wǎng)造成極大的安全威脅。因此，分析網(wǎng)絡(luò)協(xié)議和網(wǎng)絡(luò)隱蔽信道的特點(diǎn)，，研究網(wǎng)絡(luò)隱蔽信道的檢測技術(shù)成為當(dāng)前安全研究與應(yīng)用領(lǐng)域的熱點(diǎn)問題。 目前，形式化方法和自動化驗(yàn)證技術(shù)在網(wǎng)絡(luò)協(xié)議安全分析領(lǐng)域得到廣泛應(yīng)用。本文通過對網(wǎng)絡(luò)協(xié)議和網(wǎng)絡(luò)攻擊者形式化描述，針對網(wǎng)絡(luò)存儲隱蔽信道的構(gòu)建特性，提出一種基于CSP的形式化檢測和分析模型。 本文首先分析網(wǎng)絡(luò)存儲隱蔽信道的特點(diǎn)，為網(wǎng)絡(luò)協(xié)議首部定義屬性和隱蔽漏洞的概念。并根據(jù)屬性定義，把網(wǎng)絡(luò)協(xié)議首部劃分為三種類型。然后提出一種基于CSP形式語言的網(wǎng)絡(luò)存儲隱蔽信道檢測和分析通用模型，該模型對網(wǎng)絡(luò)協(xié)議和攻擊者進(jìn)行語義描述，定義網(wǎng)絡(luò)協(xié)議交互系統(tǒng)和網(wǎng)絡(luò)存儲隱蔽信道中的事件與基本進(jìn)程，以及所要滿足的安全約束。在網(wǎng)絡(luò)協(xié)議的語義正確性的基礎(chǔ)上，利用CSP中跡模型的提煉定義以及FDR檢測工具，通過檢測進(jìn)程之間的提煉關(guān)系來對網(wǎng)絡(luò)存儲隱蔽信道進(jìn)行檢測和分析。 最后，以TCP協(xié)議為例對模型進(jìn)行建模驗(yàn)證，驗(yàn)證結(jié)果為檢測到違反安全約束的反例序列，每條反例序列對應(yīng)一個網(wǎng)絡(luò)存儲隱蔽信道攻擊。該驗(yàn)證證明了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.
【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2014
【分類號】：TP393.08

【參考文獻(xiàn)】

相關(guān)期刊論文 前2條

1 周巢塵;通信的順序進(jìn)程及其研究[J];計(jì)算機(jī)學(xué)報(bào);1983年01期

2 卿斯?jié)h,朱繼鋒;安勝安全操作系統(tǒng)的隱蔽通道分析[J];軟件學(xué)報(bào);2004年09期

本文編號：1844411