计算机科学 ›› 2019, Vol. 46 ›› Issue (2): 139-144.doi: 10.11896/j.issn.1002-137X.2019.02.022

• 信息安全 • 上一篇    下一篇

信息流格模型的非法流分析

王雪健, 赵国磊, 常朝稳, 王瑞云   

  1. 中国人民解放军信息工程大学 郑州450001
  • 收稿日期:2018-07-04 出版日期:2019-02-25 发布日期:2019-02-25
  • 通讯作者: 王雪健(1993-),男,硕士生,主要研究方向为信息安全、形式化验证,E-mail:wxj1857@163.com
  • 作者简介:赵国磊(1979-),男,博士,讲师,主要研究方向为信息安全、形式化验证,E-mail:glz0371@163.com;常朝稳(1966-),男,博士,教授,博士生导师,CCF会员,主要研究方向为信息安全;王瑞云(1992-),女,硕士生,主要研究方向为信息安全。
  • 基金资助:
    本文受面向用户的可信云计算环境安全研究基金(61572517)资助。

Illegal Flow Analysis for Lattice Model of Information Flow

WANG Xue-jian, ZHAO Guo-lei, CHANG Chao-wen, WANG Rui-yun   

  1. PLA Information Engineering University,Zhengzhou 450001,China
  • Received:2018-07-04 Online:2019-02-25 Published:2019-02-25

摘要: 随着互联网的发展以及网络空间地位的上升,信息的重要性与日俱增。为确保信息安全,对非法信息流的控制显得尤为重要。文中分析了信息流格模型中信息流动的安全性,为更好地对模型内部的信息流进行分类,首先,对信息流格模型进行线性化分析,使得模型被线性化表述,并将其称为线性信息流格模型。接着,引入马尔科夫链,并利用马尔科夫链的常返态属性和瞬时态属性的概率变化,来量化表示模型中主体和客体之间的转换状态,从而检测出模型内部的各个信息流。进一步地,根据模型内部的主体和客体分别对应的常返态与瞬时态的概率对比,分析每个信息流的安全状态,即:当模型检测中同时出现两个常返态时,违反了安全模型,从而导致非法信息流的出现。由于概率变化存在同一性,该方法会产生误差并影响其检测结果。为弥补这一不足,介绍了SPA语言,然后对线性信息流格模型进行了SPA语言的描述,并采用形式化中的无干扰方法对马尔科夫链模型内概率同一性的不足进行补充说明。最后,检测出其中隐藏的非法信息流,判断出含误差下各个信息流的安全状态,并得出结论:符合安全模型但违反安全策略的信息流不满足无干扰属性。这对信息流安全检测软件的设计及硬件应用具有重要意义。

关键词: SPA, 马尔科夫链, 无干扰性, 信息流, 隐通道

Abstract: With the development of the Internet,the status of cyberspace has risen,and the importance of information is increasing.To ensure the security of information,it is particularly important for the control of illegal information flow.This paper analyzed the security of information flow in a lattice model of information flow,and classified the information flow inside the model better.Firstly,the linear analysis is done for the lattice model of the information flow,which is called a linear lattice model of information flow.Then,the Markov chain is introduced,the state attribute of the Markov chain is used,and the probability variation of the two states in the Markov chain is used to quantify the representation between the subject and the object in the model.Further,the security state of each information flow is analyzed by comparing the probability of the normal return state and the transient state corresponding to the internal body and the object respectively.That is to say,when two constant return states occur simultaneously in the model detection,the security model is violated,and an illegal information flow occurs.Due to the identity of the change in probability,the method produces errors and affects its detection results.In order to overcome this shortcoming,this paper introduced the SPA language,then described the SPA language of the linear information flow model,and used the non-interference method in formalization to make the lack of probability identity in the Markov chain model.Finally,the illegal information flow hidden in it is detected,the security state of each information flow with error is judged,and it is concluded that the information flow that conforms to the security model but violates the security policy does not satisfy the non-interference attribute.This is a major significance on software design and hardware application.

Key words: Covert channel, Information flow, Markov chain, Non-interference, SPA

中图分类号: 

  • TP309
[1]JANCZEWSKI,LECH J,ANDREW M.Information Security Policy[J].IEEE Software,2005,17(5):26-32.
[2]ADETOYE A O,BADII A.A Policy Model for Secure Information Flow[C]∥ Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security.Springer Berlin Heidelberg,2009:1-17.
[3]DENNING D E.Certification of programs for secure information flow[J].Communications of the Acm,1977,20(20):504-513.
[4]YANG P,WANG Q,MI X,et al.An Improved BLP Model with More Flexibility[C]∥ International Conference on Embedded Software and Systems.IEEE,2017:192-197.
[5]LIU G,ZHANG J,LIU J,et al.Improved Biba model based on trusted computing[J].Security & Communication Networks,2015,8(16):2793-2797.
[6]GOGUEN J A,MESEGUER J.Unwinding and Inference Control[C]∥ 1984 IEEE Symposium on Security and Privacy.IEEE,2016:75.
[7]OLMEDO M T C,MAS J F.Markov Chain[M]∥Geomatic Approaches for Modeling Land Change Scenarios.2018.
[8]HASUO I.Generic Forward and Backward Simulations II:Pro- babilistic Simulation[C]∥International Conference on Concurrency Theory.Springer-Verlag,2010:447-461.
[9]REZAEI F,HEMPEL M,RAKSHIT S M,et al.Automated Covert Channel Modeling over a real network platform[C]∥Wireless Communications and Mobile Computing Conference.IEEE,2014:559-564.
[10]BARR T W,RIXNER S.Medusa:managing concurrency and communication in embedded systems[C]∥Usenix Conference on Usenix Technical Conference.USENIX Association,2014:439-450.
[11]LAMPSON B W.Computer security in the real world[J].Computer,2004,37(6):37-46.
[12]KAUR J,WENDZEL S,EISSA O,et al.Covert channel-internal control protocols:attacks and defense[J].Security & Communication Networks,2016,9(15):2986-2997.
[13]YANG C H,WANG H Y.Modeling and Weaving of Stateful Aspects of Architecture Layer——Based on LTS Method[J].Chinese Journal of Computers,2011,34(2):342-352.(in Chinese)
杨春花,王海洋.体系结构层状态型方面的建模和编织——基于LTS的方法[J].计算机学报,2011,34(2):342-352.
[14]RYAN P Y A.Mathematical Models of Computer Security[M]∥ Computer Security Handbook,Sixth Edition.John Wiley & Sons Inc.,2000:1-62.
[15]ALDINI A,BRAVETTI M,GORRIERI R.A process-algebraic approach for the analysis of probabilistic noninterference[J].Journal of Computer Security,2004,12(2):191-245.
[16]GUNAWAN L A,HERRMANN P.Compositional Verification of Application-Level Security Properties[M]∥Engineering Secure Software and Systems.Springer Berlin Heidelberg,2013:75-90.
[17]NANEVSKI A,BANERJEE A,GARG D.Verification of Information Flow and Access Control Policies with Dependent Types[C]∥IEEE Symposium on Security and Privacy.IEEE Compu-ter Society,2011:165-179.
[18]DENNING,DOROTHY E.Framework and principles for active cyber defense[J].Computers & Security,2014,40:108-113.
[1] 张程瑞, 陈俊杰, 郭浩.
静息态人脑功能超网络模型鲁棒性对比分析
Comparative Analysis of Robustness of Resting Human Brain Functional Hypernetwork Model
计算机科学, 2022, 49(2): 241-247. https://doi.org/10.11896/jsjkx.201200067
[2] 戴宏亮, 钟国金, 游志铭, 戴宏明.
基于Spark的舆情情感大数据分析集成方法
Public Opinion Sentiment Big Data Analysis Ensemble Method Based on Spark
计算机科学, 2021, 48(9): 118-124. https://doi.org/10.11896/jsjkx.210400280
[3] 俞建业, 戚湧, 王宝茁.
基于Spark的车联网分布式组合深度学习入侵检测方法
Distributed Combination Deep Learning Intrusion Detection Method for Internet of Vehicles Based on Spark
计算机科学, 2021, 48(6A): 518-523. https://doi.org/10.11896/jsjkx.200700129
[4] 李嘉明, 赵阔, 屈挺, 刘晓翔.
基于知识图谱的区块链物联网领域研究分析
Research and Analysis of Blockchain Internet of Things Based on Knowledge Graph
计算机科学, 2021, 48(6A): 563-567. https://doi.org/10.11896/jsjkx.200600071
[5] 邓丽, 武金达, 李科学, 卢亚康.
基于TPE的SpaRC算法超参数优化方法
SpaRC Algorithm Hyperparameter Optimization Methodology Based on TPE
计算机科学, 2021, 48(2): 70-75. https://doi.org/10.11896/jsjkx.200500156
[6] 李建兰, 潘岳, 李小聪, 刘子维, 王天宇.
基于CiteSpace的中文评论文本研究现状与趋势分析
Chinese Commentary Text Research Status and Trend Analysis Based on CiteSpace
计算机科学, 2021, 48(11A): 17-21. https://doi.org/10.11896/jsjkx.210300172
[7] 白雪, 努尔布力, 王亚东.
网络安全态势感知研究现状与发展趋势的图谱分析
Map Analysis for Research Status and Development Trend on Network Security Situational Awareness
计算机科学, 2020, 47(6A): 340-343. https://doi.org/10.11896/JsJkx.190500169
[8] 杨宗霖, 李天瑞, 刘胜久, 殷成凤, 贾真, 珠杰.
基于Spark Streaming的流式并行文本校对
Streaming Parallel Text Proofreading Based on Spark Streaming
计算机科学, 2020, 47(4): 36-41. https://doi.org/10.11896/jsjkx.190300070
[9] 朱岸青, 李帅, 唐晓东.
Spark平台中的并行化FP_growth关联规则挖掘方法
Parallel FP_growth Association Rules Mining Method on Spark Platform
计算机科学, 2020, 47(12): 139-143. https://doi.org/10.11896/jsjkx.191000110
[10] 禹鑫燚, 施甜峰, 唐权瑞, 殷慧武, 欧林林.
面向预测性维护的工业设备管理系统
Industrial Equipment Management System for Predictive Maintenance
计算机科学, 2020, 47(11A): 667-672. https://doi.org/10.11896/jsjkx.200100091
[11] 邓定胜.
一种改进的DBSCAN算法在Spark平台上的应用
Application of Improved DBSCAN Algorithm on Spark Platform
计算机科学, 2020, 47(11A): 425-429. https://doi.org/10.11896/jsjkx.190700071
[12] 冯雪.
基于外部语义知识补全的自然语言查询
Natural Language Querying with External Semantic Enrichment
计算机科学, 2019, 46(8): 272-276. https://doi.org/10.11896/j.issn.1002-137X.2019.08.045
[13] 郭佳.
基于改进的人工神经网络对存储系统性能进行预测的方法
Method of Predicting Performance of Storage System Based on Improved Artificial Neural Network
计算机科学, 2019, 46(6A): 52-55.
[14] 贾宁, 李瑛达.
基于智能可穿戴设备的个性化健康监管平台的构建
Construction of Personalized Health Monitoring Platform Based on Intelligent Wearable Device
计算机科学, 2019, 46(6A): 566-570.
[15] 赵新伟, 刘伟.
一种基于节点状态的MANET路由发现和建立策略
MANET Routing Discovery and Establishment Strategy Based on Node State
计算机科学, 2019, 46(6): 112-117. https://doi.org/10.11896/j.issn.1002-137X.2019.06.016
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!