采用完整性威胁树的信息流完整性度量方法
|
摘要
针对传统信息流完整性分析方法缺乏对具体系统结构及关联性攻击事件考虑的缺陷,提出完整性威胁树对系统信息流完整性做量化分析,提出条件触发门对存在关联的攻击事件进行建模。使用攻击代价来量化攻击各信道的难易度,依据架构相关的完整性威胁树,利用可满足性模理论及其工具求解最小攻击代价,以量化分析系统完整性威胁。通过对实际飞控系统模型的建模分析求解说明方法的实用性,并得出条件触发门参数对系统完整性的影响。
In order to avert the drawback of traditional information flow integrity analysis on ignoring the specific system architecture and associated attack events,an integrity threat tree to quantify the integrity of the system information flow,and the conditional trigger gate to model the associated attack events were proposed.The attack cost was used to quantify the degree of difficulty on attacking each channel.According to the architecture-related integrity threat tree,the minimum attack cost and corresponding target channel set required to achieve the attack target were solved by using the satisfiability modulo theories.The practicality of our approach was demonstrated by the modeling and analysis of the actual flight control system models,and the influence of the conditional trigger gate parameters on the system integrity was discussed.
In order to avert the drawback of traditional information flow integrity analysis on ignoring the specific system architecture and associated attack events,an integrity threat tree to quantify the integrity of the system information flow,and the conditional trigger gate to model the associated attack events were proposed.The attack cost was used to quantify the degree of difficulty on attacking each channel.According to the architecture-related integrity threat tree,the minimum attack cost and corresponding target channel set required to achieve the attack target were solved by using the satisfiability modulo theories.The practicality of our approach was demonstrated by the modeling and analysis of the actual flight control system models,and the influence of the conditional trigger gate parameters on the system integrity was discussed.
引文
[1]DENNING D E.A lattice model of secure information flow[J].Communications of the ACM,1976,19(5):236-243.
[2]BIBA K J.Integrity considerations for secure computer systems:technical report:ESD-TR-76-372[R].1977.
[3]吴泽智,陈性元,杨智,等.信息流控制研究进展[J].软件学报,2017,28(1):135-159.WU Z Z,CHEN X Y,YANG Z,et al.Survey on information flow control[J].Journal of Software,2017,28(1):135-159.
[4]MILLEN J K.Covert channel capacity[C]//IEEE Symposium on Security and Privacy.1987:60.
[5]CLARKSON M R,SCHNEIDER F B.Quantification of integrity[J].Mathematical Structures in Computer Science,2015,25(2):28-43.
[6]KORDY B,PIETRE-CAMBACEDES L,SCHWEITZER P.DAG-based attack and defense modeling:don’t miss the forest for the attack trees[J].Computer Science Review,2014,(13-14):1-38.
[7]JHAWAR R,KORDY B,MAUW S,et al.Attack trees with sequential conjunction[C]//The 30th IFIP TC 11 International Conference,2015:339-353.
[8]AUDINOT M,PINCHINAT S,KORDY B.Is my attack tree correct[C]//The 22nd European Symposium on Research in Computer Security.2017:83-102.
[9]HOME R,MAUW S,TIU A.Semantics for specialising attack trees based on linear logic[J].Fundamenta Informaticae,2017,153(1-2):57-86.
[10]SAMET R.Recovery device for real-time dual-redundant computer systems[J].IEEE Transactions on Dependable and Secure Computing,2010,8(3):391-403.
[11]MAHONY R.KUMAR V.CORKE P.Multirotor aerial vehicles:modeling,estimation,and control of a quadrotor[J].IEEE Robotics and Automation Magazine,2012,19(3):20-32.
[12]张杨,吴文海,汪杰.舰载无人机横侧向着舰控制律设计[J].航空学报,2017,38(S1):128-134.ZHANG Y,WU W H,WANG J.Design of carrier UAV lateral/di rectional landing control law[J].Acta Aeronautica ET Astronautica Sinica,2017,38(S1):128-134.
[13]HARTLEY E N,MACIEJOWSKI J M.A longitudinal flight control law based on robust MPC and H2 methods to accommodate sensor loss in the reconfigure Benchmark[J].IFAC Papers Online,2015,48(21):1000-1005.
[2]BIBA K J.Integrity considerations for secure computer systems:technical report:ESD-TR-76-372[R].1977.
[3]吴泽智,陈性元,杨智,等.信息流控制研究进展[J].软件学报,2017,28(1):135-159.WU Z Z,CHEN X Y,YANG Z,et al.Survey on information flow control[J].Journal of Software,2017,28(1):135-159.
[4]MILLEN J K.Covert channel capacity[C]//IEEE Symposium on Security and Privacy.1987:60.
[5]CLARKSON M R,SCHNEIDER F B.Quantification of integrity[J].Mathematical Structures in Computer Science,2015,25(2):28-43.
[6]KORDY B,PIETRE-CAMBACEDES L,SCHWEITZER P.DAG-based attack and defense modeling:don’t miss the forest for the attack trees[J].Computer Science Review,2014,(13-14):1-38.
[7]JHAWAR R,KORDY B,MAUW S,et al.Attack trees with sequential conjunction[C]//The 30th IFIP TC 11 International Conference,2015:339-353.
[8]AUDINOT M,PINCHINAT S,KORDY B.Is my attack tree correct[C]//The 22nd European Symposium on Research in Computer Security.2017:83-102.
[9]HOME R,MAUW S,TIU A.Semantics for specialising attack trees based on linear logic[J].Fundamenta Informaticae,2017,153(1-2):57-86.
[10]SAMET R.Recovery device for real-time dual-redundant computer systems[J].IEEE Transactions on Dependable and Secure Computing,2010,8(3):391-403.
[11]MAHONY R.KUMAR V.CORKE P.Multirotor aerial vehicles:modeling,estimation,and control of a quadrotor[J].IEEE Robotics and Automation Magazine,2012,19(3):20-32.
[12]张杨,吴文海,汪杰.舰载无人机横侧向着舰控制律设计[J].航空学报,2017,38(S1):128-134.ZHANG Y,WU W H,WANG J.Design of carrier UAV lateral/di rectional landing control law[J].Acta Aeronautica ET Astronautica Sinica,2017,38(S1):128-134.
[13]HARTLEY E N,MACIEJOWSKI J M.A longitudinal flight control law based on robust MPC and H2 methods to accommodate sensor loss in the reconfigure Benchmark[J].IFAC Papers Online,2015,48(21):1000-1005.