0-abstract-toc.tex

% !TEX root = main.tex
\begin{abstract}
    This project describes how a modern static analyzer detects unsafe dataflow, i.e.\ data that 
    comes from an untrusted source that flows unmodified to a sink.
    It gives an introduction to CodeQL, a static analyzer developed by Github,
    and their logic-programming language QL.
    We formalize a specification of an algorithm that detects unsafe dataflow,
    analysing a reduced imperative language without support for procedure calls or objects.
    We then prove, using a tracing operational semantics, that any algorithm
    conforming to this specification is sound.
    Following that, we provide an implementation of such an algorithm in QL.
    This implementation is supported by a database schema and library for our toy language.
    The implementation is based on the same principles as the algorithm used to
    detect unsafe dataflow by CodeQL when analysing Java code.
    Namely, it works on an auxiliary datastructure, the dataflow graph.
    We explain how the implementation can be used to get a certificate that 
    a program does not exhibit unsafe dataflow.
    To highlight how close QL code is to first-order predicate logic, we translate
    the main parts of our implementation back to the usual logic syntax.
    We end with describing an improvement in the Java dataflow library
    that was contributed as part of this project, and by outlining why the original 
    project goal of developing a path-sensitive extension to the dataflow algorithm
    used by CodeQL did not work out.
\end{abstract}
\tableofcontents