Checking Secure Information Flow in Programs

This thesis is concerned with static code analysis. More particularly, with code analysis techniques for checking information flows in programs. First this thesis describes why is important to trace the information flows in a program, it introduces some fundamental concepts and presents the state of art. Then, two methods for checking secure information flow are proposed. The first is based on code transformation, and reuses the type analysis of the Java byte code Verifier. This method analyses programs written in a subset of the Java Virtual Machine Language. The second approach, named instruction-level security typing, has been defined in the framework of Abstract Interpretation end ha been shown more precise than standard typing approaches. This method has been applied to check the classical non-interference property in stack-based assembly programs and in high-level language programs.