| As the core equipment of the network,the security of the router is of great significance to the security of the entire cyberspace.However,in recent years,the security status of routers is still not optimistic.Major router manufacturers have frequently been exposed to serious security vulnerabilities in their equipment,and the harm has spread to all regions of the world.The mimic router based on the dynamic heterogeneous redundancy(DHR)architecture design based on mimic defense has higher security than traditional routers.On the premise of not affecting the performance of the system,it realizes the discovery and blocking of attacks based on unknown backdoor vulnerabilities.In the DHR architecture of the mimic router,in addition to the functionally equivalent heterogeneous execution entities,the core is the design of protocol proxies(including input proxy and output proxy),multi-mode voting,dynamic scheduling,and other components.These components,which are also known as the " mimic bracket",are outside the protection capabilities of the DHR architecture.As a bridge between heterogeneous entities and the outside world in a mimic router,as well as the center of entity scheduling control,the security of mimic bracket components is particularly important for mimic routers.Although the attack surface of the "mimic bracket" components is small compared to the execution entities,strict methods are still required to ensure its security and functional correctness,considering its high degree of criticality.For the first time,this paper applies the formal method to the design and implementation of the "mimic bracket" components of the mimic router,which include three modules: packet classifier,ARP protocol proxy,and BGP protocol proxy.This paper mainly completes the following work:1.The shortcomings of existing formal verification methods directly applied to mimic routers are analyzed;through further research on the existing work,we have found it is a practical method to manually write formal specifications based on the separation logic method,use the theorem prover to complete the transformation of codes and specifications into proof conditions and complete the proof.2.Based on the DHR2 master-slave model of the mimic router,the packet classification module,ARP protocol proxy module,and BGP protocol proxy module of the mimic router are designed and implemented.The frame structure and the implementation flow chart of each network function module are introduced in detail.A suitable test environment is built for each network function module,and the functions and performance of the implemented modules are fully tested through various experimental scenarios.The test results show that the implemented modules have complete functions,high robustness and excellent performance.3.Using the Veri Fast theorem prover,a formal specification based on the separation logic is written,which formally proves the memory security of the implemented network function module and ensures that the program will not have memory security problems including null pointer references,memory use after free vulnerabilities,memory double-free vulnerabilities,and memory leaks.On this basis,for each network function module,an accurate and appropriate formal specification is written,the formalization proves the correctness of the module function,and through the formal verification,it is guaranteed that the functional modules implemented meet expectations。 The ratio between program implementation code and verification code is5:3,and the ratio of working time spent between program implementation and program verification is 1:3.Since formal verification eliminates memory security issues in the program code and proves the correctness of module functionality,the cost of formal verification is worth it.The design and verification methods used in this paper can be generalized as experiences to the formal verification of mimic routers,other mimic devices,and system key functional modules,and further improve the overall security of mimic devices and systems. |
PDF Full Text Request