Description
When auditing a program, Code Property Graphs (CPGs) are a useful tool
to systematically search the program for possible errors. While they can
be efficiently used with common graph databases, they are limited by the
small amount of semantic information contained in them. An auditor looking
for a specified behaviour thus has to devise a query broad enough to not miss
any bugs, yet narrow enough to produce a small enough number of results to be
individually examined by a human. Model checking techniques on the other hand
provide a way to check for behaviours in a program.
However, the models usually lack potentially useful information such as
which values can be controlled by a user.
This thesis aims to combine CTL model checking utilizing the CEGAR
technique with CPGs by proposing a modelchecking filter on query results.
It defines an algorithm for automated construction of a Kripke Structure from
CPG subgraphs given by CFG paths and AST subtrees. It also proposes several ways
to incorporate information available in the CPG as a set of heuristics for the CEGAR
cycle, thereby improving its performance.
The proposed algorithms and optimizations are tested with regards to their computational
benefits and complexity, and two example applications are evaluated for the new
algorithms, including the verification and optimization of algorithms in a program, as
well as the search for potential security vulnerabilities.
|
Thesis topic in co-operation with the Fraunhofer Institute for Applied and Integrated Security AISEC, Garching