# Combining Static and Dynamic Program Analysis Techniques for Checking Relational Properties

#### PhD Thesis

Author(s):Mihai Herda
School:Karlsruhe Institute of Technology (KIT)
Year:2020
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.
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.
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.
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.

## BibTeX

@phdthesis{HerdaDiss,
author       = {Mihai Herda},
year         = {2020},
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.}
}