In the process of programmable networks simplifying network management and increasing network flexibility through custom packet behavior, security incidents caused by human logic errors are seriously threatening their safe operation, robust verification methods are required to ensure their correctness. As one of the formal methods, symbolic execution offers a viable approach for verifying programmable networks by systematically exploring all possible paths within a program. However, its application in this field encounters scalability issues due to path explosion and complex constraint-solving. Therefore, in this paper, we propose NetVerifier, a scalable verification system for programmable networks. To mitigate the path explosion issue, we develop multiple pruning strategies that strategically eliminate irrelevant execution paths while preserving verification integrity by precisely identifying the execution paths related to the verification purpose. To address the complex constraint-solving problem, we introduce an execution results reuse solution to avoid redundant computation of the same constraints. To apply these solutions intelligently, a matching algorithm is implemented to automatically select appropriate solutions based on the characteristics of the verification requirement. Moreover, Language Aided Verification (LAV), an assertion language, is designed to express verification intentions in a concise form. Experimental results on diverse open-source programs of varying scales demonstrate NetVerifier’s improvement in scalability and effectiveness in identifying potential network errors. In the best scenario, compared with ASSERT-P4, NetVerifier reduced the execution path, verification time, and memory occupation of the verification process by 99.92%, 94.76%, and 65.19%, respectively.

In the cloud-edge collaborative network, advanced persistent threats (APTs) pose a serious security risk to critical network assets. Although network deception defense can mislead attackers’ cognition, its effectiveness depends on dynamically selecting appropriate rotation timings of the deception defense. However, the deployment of deception resources and state updates is not completed instantaneously, and existing methods ignore the state transition delay and the dynamic interaction between the attackers and defenders during the real attack and defense process. To address this, we propose a deception defense timing selection method based on the time-delayed FlipIt game. Firstly, a network state evolution model integrating state transition delay is constructed, and the dynamic transfer process between node states is characterized by a set of delay differential equations. Secondly, a cloud-edge collaborative defense architecture is designed. On this basis, a time-delayed FlipIt game model (TD-FlipIt) is established, and the gate control mechanism is introduced to formalize the defense cooling period as a constraint for the rotation action of deception resources. Subsequently, we use the multi-agent deep deterministic policy gradient (MADDPG) algorithm to solve the rotation strategy for deception defense timing. Experimental results show that the proposed method can effectively optimize the selection of defense timing, ensuring defense effectiveness while reducing resource consumption, and providing effective support for defense in the cloud-edge collaborative environment.