Implementation And Semi-automatic Formal Verification Of Key Functions Of Mimic Routers

The mimic router is designed based on the dynamic heterogeneous redundant architecture of mimic defense,which has good defense capability for unknown vulnerabilities and backdoors.The key functional codes such as protocol proxies are in the pivotal position of internal and external communication in the mimic router and are not protected by the dynamic heterogeneous redundant architecture,in which the hidden program flaws and security vulnerabilities will affect the overall defense capability of the mimic router,so the security of key functional codes such as protocol proxies is of great importance to the mimic router.The basic motivation of this thesis is to design and implement highly secure key functional components of the mimic router,such as protocol proxies,so as to improve the attack resistance of the mimic router.Traditional software testing techniques,such as code review and unit testing,can only check and find some conventional types of defects and vulnerabilities,but cannot fully guarantee their security,so there is an urgent need for other techniques to conduct a more comprehensive and in-depth inspection of the key functional components implemented.Formal verification techniques prove that a program or system satisfies certain properties described by a formal statute through mathematical methods such as logical deduction,and thus provide higher assurance of the security of the verified program than traditional software testing techniques such as code review and unit testing.If formal verification techniques are applied to the development of key functional components of the mimic router,the overall attack resistance of the mimic router can be further improved.However,formal verification techniques themselves have the problems of high verification cost and constraint of the code to be verified,and the key functional code of the mimic router also faces the problem of not being able to use conventional formal verification techniques such as logical deduction due to its complex state and implementation across multiple layers of messages in computer networks.As a result,the field of mimic defense currently has only some work on model building and checking of the dynamic heterogeneous redundant architecture itself,and lacks formal verification work for a specific mimic defense device.Based on these problems and the current situation,this thesis designs and implements key functional components such as protocol proxies in mimic defense routers,and studies and discusses the application of formal verification techniques in them.The optimization method when writing the implementation and the formal specification is proposed,which effectively reduces the verification cost.The main work of this thesis is as follows.(1)To address the problem that the complex state of the key functional code of the proposed router makes it impossible to use conventional formal verification techniques such as logical deduction,a combination-based semi-automatic formal verification technique is used to reduce the number of program states to be checked,and the formal verification technique is successfully applied to the checking of the key functional code of the proposed router.By splitting the critical function code into multiple sub-modules,using exhaustive symbolic execution and writing loop invariants for infinite state program loops,the path explosion problem is avoided and all program control flow of the critical function code is obtained.Using Hall logic and separation logic,formal statutes and manual guidelines are written for the key functional codes that need to be checked,machine checks are performed for each program control path obtained from symbolic execution,and finally the overall check of the key functional codes is completed using a combined approach.(2)To address the problem of excessive amount of additional proof work due to the use of formal verification techniques,an optimization method when writing implementation and formal statutes is proposed.Based on the understanding of the semi-automatic formal verification technique,some optimizations are made in advance when writing the implementation code and the formal statute to avoid unnecessary extra proof work when machine checking the proof.In this thesis,we propose some basic principles to be followed when writing the implementation code and formal statute,which can effectively reduce the extra proof cost caused by introducing semi-automatic formal verification techniques into the code checking of key functions of the proposed router.(3)Based on the above scheme and techniques,we designed and implemented the traffic speed limit module,RIP protocol proxy,and TCP protocol proxy in the mimetic defensive router,wrote formal statutes and manual guidelines for these three modules,and checked them with semi-automatic formal verification techniques.The traffic rate-limiting module is located at the front end of the input proxy of the proposed constructive router and limits the rate of messages entering the input proxy of the proposed constructive router.the RIP protocol proxy sniffs RIP messages between neighbors and the master entity of the RIP router and distributes RIP messages to each heterogeneous RIP router slave entity of the proposed constructive router by simulating the neighbors to copy the RIP messages.the TCP protocol proxy sniffs TCP messages between neighbors and the TCP messages between the master entities,simulates the establishment of TCP connections between the neighbors and the slave entities,and provides a programmatic interface to the upper layer application layer protocol proxy.The formal verification work in this thesis found 9.5 hidden program defects and security vulnerabilities per thousand lines of implementation,as a comparison,83.3% of the defects and vulnerabilities were not detected by traditional software testing techniques such as unit testing during the design and implementation phase.