Search

We consider while-language programs with variables of two security types: low and high. Security static analysis of information flows of such programs identifies insecure information flows which can cause leaks. Semantic rules of such an analysis which was proposed in [6] assign security types for expressions, operators and compositions of operators. We use these rules to propose an algorithm of security static analysis to discover a security type of the program under consideration. If such a type can be assigned, information flows of the program are secure; otherwise, it contains insecure information flows. We have used flex and bison [5] tools to implement a translator for a while-language into the MMIX computer [2] instruction sequence.