Research on Industrial Internet Data Security Technology based on Formal Verification of SM4

Industrial Internet promotes the transformation of industrial platform from business system driven to data driven through the flow of industrial data between massive multi-source equipment and heterogeneous systems. The data flow of industrial Internet involves the interactive transmission of a large number of key sensitive information between enterprises. Coupled with its inherent openness and heterogeneity, it is facing serious security challenges such as sensitive data leakage and integrity destruction. Cryptography technology is one of the important methods to ensure data security. Among them, the national cryptographic algorithm can meet the requirements of security, autonomy and controllability of Chinese industrial Internet data, and avoid the risk of "backdoor" when the current mainstream international cryptography algorithm protects the key sensitive data. However, there are still security threats such as memory leakage and time-side channel attack which cause the invalidity of encryption mechanism when the national cryptographic algorithm is deployed in industrial Internet system. Formal verification method is an important method to verify the security and reliability of cryptographic algorithms. Existing researches have designed a variety of formal verification mechanisms for the underlying cryptographic algorithms of some structures and protocols, but the research on formal verification for national cryptographic algorithm is still in a blank stage. This paper proposes a formal verification method of SM4 cryptographic algorithm based on programming framework F*, which can ensure the memory security and resist the time-side channel attacks during the implementation of the algorithm. And the method can reduce the security risks, when the national cryptographic algorithm is deployed in the industrial internet.