Fully Automatic Logic-Based Information Flow Analysis

• Applicant: Dr. Richard Bubel
• Subject Area: Software Engineering and Programming Languages
• Term: from 2012 to 2016
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 228021792

In this project we will develop a fully automatic logic-based approach for information-flow analysis of object-oriented programs (specifically, Java).Language-based information-flow security analysis allows to ensure that no secrets can be learned by observing different runs of a program.Current information-flow analyses are either• fully automatic, but highly approximate and imprecise. Hence, they classify many actually secure programs as insecure. Most of these approaches are also limited to small, academic toy languages.• or they are precise analyses, but require significant, time-consuming, and expensive userinteraction.In this project we envision a deductive information-flow analysis for programs written in a real-word programming language (Java), which is fully automatic and accepts a significantly larger class of secure programs than previous automatic approaches.This increase of the analysis performance will be achieved as follows:1. We will base our approach on a general program logic and symbolic execution. The advantage of taking a logic-based approach is to achieve a faithful and precise modeling of the program language semantics without a priori simplifications or abstractions. Other approaches start with a coarse abstraction and have to iterate through several refinement steps until they reach the necessary precision.2. To be fully automatic and to avoid any kind of user interaction, we will develop a technique for symbolic state abstraction. This technique allows us to handle program constructs such as loops—which would otherwise require user-interaction—fully automatic. The proposed technique will abstract the symbolic state but not the program itself. The abstraction is performed only if necessary (on-demand) and restricted to those parts of the state, which are possibly modified by, e.g., a loop. For the remaining part of the symbolic state we stay precise.This is complemented by formalisations of a number of secure information-flow properties such as non-interference and delimited information release, specifically tailored towards our approach.In addition we will automatically generate exploits for insecure programs to support the developer in understanding the present information-flow policy violation. Our approach is based on symbolic execution, which can serve as a basis for automatic test generation. We will use this fact to generalize test case generation to exploit generation.

• DFG Programme: Priority Programmes
• Subproject of: SPP 1496: Reliably Secure Software Systems
• Participating Person: Professor Dr. Reiner Hähnle