Automated Software Analysis Group

Refinement of Path Conditions for Information Flow Analysis

  • 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.



    author = "Stephan Gocht",
    title  = {Refinement of Path Conditions for Information Flow Analysis},
    school = {Karlsruhe Institute of Technology},
    type   = {Bachelor Thesis},
    year   = {2014},
    month  = {December}