Secure Information Flow Based On Syntax Analysis

It is very easy to capture information by computer network. Information is insecurity more and more for invader's activity day by day. It is pressure to develop secure information technique for the information society.Aiming at the study keystones of secure information flow those days, the present dissertation makes some works about secure information flow. The main study works and innovation are as follows:I. Type System Method.1. Volpano et al. developed a type system to ensure secure information flow in a sequential, imperative programming language. We extend the analysis to deal with a non-determinism programming language. We show that the Volpano et al's type system is insufficient to ensure a desirable security property called noninterference. We also show that well-typed non-determinism programs are probabilistically noninterference.2. Many type systems of secure information flow have been developed after the initiation work of Volpano et al.'s about sucure information flow. But so far little type system attention to multidimensional arrays operations of secure information flow, we allow array as first-class value and regards multidimensional arrays as array of array by alias array. To distinguish array from its alias, we propose a novel binary memory model. The soundness of our type system is proved by noninterference property.3. Language-based information flow security policy is often formalized as noninterference, only allow information flow from low security level to high security level. Noninterference is too rigid to use practical program. Downgrading specifies information flow from a high security place to a low security place, also called confidentiality labels declassification. When a practical program declassifies information properly, there is some reason to accept some information release, we present downgrading policies which can specify data is declassified though someoperation if some condition are satisfied. Data labeled with a policy (?) p must be treated at security level ï¿¡, the operator op may be applied to the data providedcondition c is true, and the result of the operation is labeled with security policy p .For all security downgrading policies are intension, we therefore propose a security policy framework that supports downgrading in practical programs, each downgrading step is annotated with some operations when some conditions are satisfied. The soundness of our type system is proved by relaxed noninterference property.II. Data Flow Analysis Method.Suppose information only have two security levels, one is the hihh security(H),...