Verification And Synthesis Strategy Of Information Flow Security Properties Based On Petri Net

Nowadays, due to our country and society widespread dependence on computer and network technology, information security is more and more valued. Standard security mechanisms such as access control are essential components for protecting the confidentiality and integrity of data. But even in a secure system which has been implemented Mandatory Access Control mechanism, a high-level process can signal information to a low-level process by using covert channel. Because information disclosure is essentially illegal flow of information, the technique of information flow analysis has been used to find potential disclosure of information. It gives the definition of information flow security properties to describe the legal information flow. So we can judge whether a system has the disclosure of information by verifying the security properties of this system and prevent the unauthorized users getting the information.Traditional information flow analysis uses "Unwinding Method" to verify the information flow security properties, which could be just used in deterministic system and is not sufficient for un-deterministic system. In this paper, we use Petri net to model security system and give a sufficient algorithmic verification method. This algorithmic is implemented by calculating the reachable graph of the Petri net. To reduce the work of calculating, we give some rules to simplify the Petri net and this procedure will not change the security property. Because a system is usually composed by some subsystems, we further give the synthesis model which can keep the security property and give a method to conclude the security property of a system from its subsystems. The main contribution of this paper rests with the following:1. Present a sufficient algorithmic verification method for information flow security properties on Petri net. Use Petri net to model security system and give the definition of information flow security properties, then give a sufficient algorithmic verification method by calculating the reachable graph of Petri net which illustrates the statement set produced by firing transitions. The algorithmic verifies the security properties by the influence on result statement sets of the firing of transition sequences. With this sufficient algorithm we can not only determine the establishment of properties, but also give the reason of not.2. Design rules of simplifying Petri net and prove the security properties will not be changed. Because the node of a reachable graph is huge, we give three simplification rules:place simplification rule, transition simplification rule and comprehensive simplification rule. These rules delete transitions and places which will not influence the security properties of a Petri net to simplify the reachable graph. To verify these rules are valuable, we prove that the simplified system keeps the security of the original one.3. Give the synthesis models which can keep security properties on Petri net and prove them. After analyzing the existing synthesis of Petri net for information flow security properties, present the synthesis models to insure the composed net can keep the security properties of the subnets which satisfy same security properties.In the last, we develop the software "the verification system for Petri net based information flow security properties". It is used to verify whether a system is satisfied with the information security properties and find the path of information leakage when it is not.