Dissertation: Slicing of Concurrent Programs and its Application to Information Flow Control

Information flow control is concerned with the security of sensitive information being processed by a software. It aims to ensure that software does not leak rightfully accessed sensitive information to unauthorized sinks or taints it with data from unauthorized sources during its computations. It can be used supplementary to established security techniques like access control or encryption to enhance the protection of sensitive information.

This thesis presents a practical technique for information flow control for concurrent programs with threads and shared-memory communication. The technique guarantees confidentiality of information with respect to a reasonable attacker model and utilizes program dependence graphs (PDGs), a language-independent representation of information flow in a program, which allows to apply it to all programs that can be translated into a PDG.

The thesis is embedded in the ValSoft/Joana project of the Programming Paradigms Group at the Karlsruhe Institute of Technology. The project aims to develop IFC techniques that analyze security relevant software written in established languages, like C or Java, with maximal precision, so that no information leaks are missed and very few false alarms are generated. Its core is the Joana framework, a general-purpose program analysis framework based on PDGs, highly precise representations of the possible information flows in a program. Joana focuses on Java and is currently able to build PDGs for Java programs with up to 30.000 lines of code. It is capable of full Java bytecode, including features like objects, dynamic dispatch, side effects of procedure calls, exceptions and threads.

At the time this thesis started, ValSoft/Joana focused on analyzing Java programs for smart cards, written in JavaCard. Such programs are comparatively small, and JavaCard did not support threads at that time. The Joana framework was already able to create PDGs for Java programs with threads, but made very conservative approximations in order to do so, leading to very imprecise results. Furthermore, the already existing information flow control technique was limited to sequential Java programs. Threads are an integral component of the Java language, so full support of Java threads had to be integrated into Joana in order to analyze general Java programs. This was the task of this thesis. It accomplishes that task by making the following major contributions:

• It extends Joana with a may-happen-in-parallel analysis, which identifies those parts of a Java program that may execute concurrently. Using this analysis, a large number of dependences computed by the previous versions of Joana can be identified as redundant.
• PDGs are usually examined via graph traversal. A PDG of a concurrent program comprises all possible ways of interleaving of its threads, wherefore it may contain dependences based on incompatible ways of interleaving and thus, paths that cannot be realized by any program execution. It is left to the graph traversal algorithm to avoid these unrealizable paths. To this end, the thesis investigates, develops, improves and compares highly precise algorithms for the traversal of PDGs that address that problem.
• The above enhancements of Joana are used to develop an information flow control technique for concurrent programs based on PDGs and their traversal. The technique guarantees the confidentiality of successfully verified programs independent from the concrete scheduler and is permissive compared with other approaches.

A crucial objective of the author was to develop algorithms capable of full Java bytecode, to avoid restrictions on the syntax of the programs to be analyzed. Furthermore, for many investigated subproblems, alternative algorithms are presented, which solve the subproblem with different degrees of precision, runtime costs and implementation effort. This enables a user to choose the algorithm that suits best. All presented algorithms have been integrated into Joana, resulting in a PDG-based, general-purpose program analysis framework for full Java bytecode, containing, to the best of our knowledge, the first reported implementation of an information flow control technique for a contemporary language with threads and shared memory.