Author:
Stephan Gocht
Place:
Karlsruhe Institute of Technology, Bachelor thesis, 2014
Date: December 2014
Abstract

Path conditions are a static analysis tool for information flow control (IFC). They can be used to produce witnesses for an illegal flow, which do not necessarily represent a concrete execution of the program. This bachelor thesis will provide a detailed approach to eliminate these false witnesses using counterexample guided abstraction refinement (CEGAR) and thereby increase precision.

As not all values satisfying the PC need to occur simultaneously during a program execution, a property is introduced which is true iff the values occur during the program execution. Some values are always occurring simultaneously if a flow exists. This information can be used to increase precision and is added to the described property, without using temporal logic. Finally, the CEGAR approach is adopted to provide an algorithm for checking this property.

links

BibTex

@bachelorsThesis{stephan-gocht-thesis,

    author = "Stephan Gocht",

    title  = {Refinement of Path Conditions for Information Flow Analysis},

    school = {Karlsruhe Institute of Technology},

    type   = {Bachelor Thesis},

    year   = {2014},

    month  = {December}