Combining Static and Dynamic Program Analysis Techniques for Checking Relational Properties

@phdthesis{HerdaDiss,
    author       = {Mihai Herda},
    year         = {2020},
    month        = jan,
    title        = {Combining Static and Dynamic Program Analysis Techniques for Checking Relational
                    Properties},
    school       = {Karlsruhe Institute of Technology (KIT)},
    language     = {english},
    doi          = {10.5445/IR/1000104496},
    abstract     = {The topic of this thesis belongs to the research area of formal software verification.
                    It deals with checking relational properties of computer programs (i.e., properties that
                    consider two or more program executions). The thesis focuses on two specific relational
                    properties: (1) noninterference and (2) whether a program is a correct slice of another.
                    The noninterference property states that running a program with the same public input
                    values will always produce the same public outputs, regardless of the secret inputs
                    (e.g., a password). This means that the secret inputs do not influence public outputs.
                    Program slicing is a technique to reduce a program by removing statements from it while
                    preserving a specified part of its behavior, such as the value of a variable at a
                    program location.
                    \newline

                    The thesis provides frameworks that allow the user to analyze the two properties for a
                    given program. The thesis advances the state of the art in the area of formal verification
                    of relational properties by providing novel approaches for the analysis on the one hand
                    and by combining existing approaches on the other hand. The thesis contains two parts,
                    each handling one of the two relational properties.
                    \newline

                    \emph{Noninterference}.
                    The framework for checking noninterference provides new approaches both for automatic
                    test generation and program debugging, and it combines these new approaches with
                    approaches based on deductive verification and dependency graphs. The first new approach
                    provided by this framework allows for the automatic generation of noninterference tests.
                    It allows the user to search for violations of the noninterference property, and it also
                    provides a coverage criterion for the generated test suites that is appropriate for
                    relational properties. The second new approach provided by the framework is a relational
                    debugger for analyzing noninterference counterexamples. It employs well-known concepts
                    from program debugging, and it extends them for relational program analysis. To support
                    the user in proving a noninterference property, the framework combines an approach based
                    on dependency graphs with a logic-based approach that uses a theorem prover.
                    Dependency-graph-based approaches compute the dependencies between various program parts
                    and check whether the public output depends on the secure input. Compared with logic-based
                    approaches, dependency-graph-based approaches scale better. However, because they
                    over-approximate the dependencies in a program, they may report false alarms. Two further
                    contributions of the framework are thus represented by two combinations of the logic-based
                    and dependency-graph-based approaches: (1) the dependency-graph-based approach simplifies
                    the program that is checked by logic-based approach, and (2) the logic-based approach
                    proves that certain dependencies computed by the dependency-graph-based approach are
                    over-approximations and can be discarded from the analysis.
                    \newline

                    \emph{Program slicing}.
                    The second part of the thesis discusses a framework for automatic program slicing.
                    Whereas most state-of-the-art slicing approaches only perform a syntactical analysis of
                    the program, this framework also considers the semantics of the program and can remove
                    more statements from a program. The first contribution of the slicing framework consists
                    of a relational verification approach that was adapted to check whether a slice is valid,
                    (i.e., whether it preserves the specified behavior of the original program). The
                    advantage of using relational verification is that it works automatically for two similar
                    programs---which is the case when considering a slice candidate and an original program.
                    Thus, unlike the few state-of-the-art slicing approaches that consider the semantics of
                    the program, our approach is automatic. The second contribution of this framework is a
                    new strategy for generating slice candidates by refining dynamic slices (i.e., slices
                    which are valid for a single input) by using the counterexamples provided by the
                    relational verifier.}
}