Research On Key Technologies Of Network Security Control Based On Formal Semantics

The integrated air-ground information network has the properties of air-based network,intergenerational ground network and interconnection between air and ground.In order to deal with the complex dynamic changes of multi-domain and multi-business,potential unknown attacks,high performance interconnection security control and reasonable and efficient deployment of policy distribution,a key technology solution of security control based on formal semantic method is provided.Formal semantic method is used to formalize the modeling of specific problems.The corresponding semantic execution model is given for interpretation.Semantic security analysis is done under certain circumstances.Thus,the semantic security of the integrated multi-domain network is improved.It is applied to the secure interconnection control system of integrated air-ground multi-domain network.The main innovations and works achieved include the following four aspects:1)Rule conflict detection of interconnection security control based on semantic consistency analysisThere are differences in security requirements of the services carried by the multidomain network.Thus,rule conflict detection of multi-domain interconnection security control based on semantic consistency analysis is proposed from the perspective of differential security control in the integrated air-ground network based on user type,service type,security domain,security level and characteristics of ground-based network.The method can express rules recognized by the gateway and policies supporting multi-domain configuration respectively.Through the translation of policy to rules,the configuration policy can be transformed into gateway rules,and the rules can be loaded into the gateway to implement the interconnection of multi-domain network.The policies and rules are given semantic interpretation,and the mapping security and semantic security of the method are proved through semantic analysis,so as to ensure the semantic consistency of security control.The large throughput test shows that the method simplifies the rules and improves the filtering efficiency.2)Detection response policies of interconnection security control supporting dynamic expansionDue to the changeable nature of the integrated network,the security requirements change with the change of the multi domain network context.For the diversified and potentially unknown attack scenarios,the traditional static deployment security policy and manual security architecture for existing attacks can no longer meet the dynamic security needs of all kinds of users in integration of air-ground network.Aiming at this problem,a dynamic expansion method of interconnected security control policies for intelligent network attack detection is proposed.The policies of attacker,network and alarm event is formally described by first-order logic in the method.The attack chain is searched in the semantic model according to the atomic formula generated by the alarm event policy.Firewall blocks the attack behavior in the network according to the response rules obtained by searching the semantic tree and mapping,as well as the characteristics of network speed,protocol handshake and quintuple.The semantic security of the method is proved through a series of formal analysis.The combined experiments of traffic and host behavior detection,publish and subscribe,attack chain construction and firewall verify the feasibility of this method.It can support the generalization of intrusion detection and response.3)Optimization of interconnected security control based on semantic security analysis of process communicationFacing the demand of multi-domain security control in the integrated network of air and ground,to solve the problem that "single-process regular matching restricts the performance of interconnected security gateway",the method of high-performance optimization of interconnected security control based on semantic security analysis of process communication is proposed.The interaction model of master-slave processes is described in a parallel programming language in the method.The the state transition system semantics are given to accurately express the combined semantics of the master-slave processes.The security of master-slave processes in combinatorial semantics is analyzed,which ensures that the parallel running of processes has no deadlock and starvation,and is equivalent to the original regular matching.Experimental results show that the proposed method can give full play to the advantages of multi-core hardware and reduce the context switching overhead of the scheduler.In the case of complex regular expressions,the method is an order of magnitude better than single-core running.4)Lightweight for policies distribution protocol based on embedded security protocol logicAiming at the authentication problem of the security control policy distribution in the interconnection of network security control equipment with limited computing resources of satellite,the lightweight certification supporting high-speed distribution of interconnected security control was proposed to ensure the security and reliability of policy distribution.The authentication protocol construction is formally described in the method.The implementation model interpretation of the protocol is also given.Through formal semantic analysis,the method has the properties of the secrecy,non-injective synchronicity and injective synchronicity.The experimental results show that This method can support highspeed distribution of interconnected security control.Through the integrated air-ground experimental platform test,lightweight authentication protocol realizes heterogeneous communication between space-based network and ground network.Parallel optimization of high performance fine-grained multidomain interconnection security control and dynamic extension of attack detection and response policies are deployed in a specific safety gateway and run in coordination with other systems,forming the ability of secure and controlled exchange of information between different networks,real-time blocking of cross-network attacks and cooperative protection of the integration of air and ground.