The consistency verification of Computer Network Defense Policy and measures

Computer Network Defense Policy is the rules of computer network and security devices. In order to achieve specific security objectives, the network need to choose the defensive measures under certain conditions. In order to generate the measures implemented by the device, it usually requires manual or automated translation from high-level network defense policy. In the translation process, due to the presence of semantic loss, man-made understanding mistakes, device machinery, etc., the high-level policy requirements cannot be completely satisfied. This will result in hiding network security risks or vulnerabilities. Through analysis of the consistency between high-level policy and low-level measures, and pointing out the lack and redundancy between the policy and measures, it can guide the further translation of policy on the device. This paper presents a novel formal and automated method to verify the consistency. When errors are detected, we will point out the location of the misconfiguration. The same time, based on SMT solving tools, it has been implemented in a prototype of consistency verifier. Experiments demonstrate that this tool is able to check the consistency and have good scalability and efficiency.