Quoc-Sang Phan

Long H. Pham, Quang Loc Le, Quoc-Sang Phan et al.

Symbolic execution is a well established method for test input generation. Despite of having achieved tremendous success over numerical domains, existing symbolic execution techniques for heap-based programs are limited due to the lack of a succinct and precise description for symbolic values over unbounded heaps. In this work, we present a new symbolic execution method for heap-based programs based on separation logic. The essence of our proposal is context-sensitive lazy initialization, a novel approach for efficient test input generation. Our approach differs from existing approaches in two ways. Firstly, our approach is based on separation logic, which allows us to precisely capture preconditions of heap-based programs so that we avoid generating invalid test inputs. Secondly, we generate only fully initialized test inputs, which are more useful in practice compared to those partially initialized test inputs generated by the state-of-the-art tools. We have implemented our approach as a tool, called Java StarFinder, and evaluated it on a set of programs with complex heap inputs. The results show that our approach significantly reduces the number of invalid test inputs and improves the test coverage.

Quoc-Sang Phan

This thesis is concerned with the quantitative assessment of security in software. More specifically, it tackles the problem of efficient computation of channel capacity, the maximum amount of confidential information leaked by software, measured in Shannon entropy or Rényi's min-entropy. Most approaches to computing channel capacity are either efficient and return only (possibly very loose) upper bounds, or alternatively are inefficient but precise; few target realistic programs. In this thesis, we present a novel approach to the problem by reducing it to a model counting problem on first-order logic, which we name Model Counting Modulo Theories or #SMT for brevity. For quantitative security, our contribution is twofold. First, on the theoretical side we establish the connections between measuring confidentiality leaks and fundamental verification algorithms like Symbolic Execution, SMT solvers and DPLL. Second, exploiting these connections, we develop novel #SMT-based techniques to compute channel capacity, which achieve both accuracy and efficiency. These techniques are scalable to real-world programs, and illustrative case studies include C programs from Linux kernel, a Java program from a European project and anonymity protocols. For formal verification, our contribution is also twofold. First, we introduce and study a new research problem, namely #SMT, which has other potential applications beyond computing channel capacity, such as returning multiple-counterexamples for Bounded Model Checking or automated test generation. Second, we propose an alternative approach for Bounded Model Checking using classical Symbolic Execution, which can be parallelised to leverage modern multi-core and distributed architecture.