@inproceedings{5774,
  abstract     = {{Information flow analysis investigates the flow of data in applications, checking in particular for flows from private sources to public sinks. Flow- and path-sensitive analyses are, however, often too costly to be performed every time a security-critical application is run. In this paper, we propose a variant of proof carrying code for information flow security. To this end, we develop information flow (IF) certificates which get attached to programs as well as a method for IF certificate validation. We prove soundness of our technique, i.e., show it to be tamper-free. The technique is implemented within the program analysis tool CPAchecker. Our experiments confirm that the use of certificates pays off for costly analysis runs.}},
  author       = {{Töws, Manuel and Wehrheim, Heike}},
  booktitle    = {{Theoretical Aspects of Computing – ICTAC 2018}},
  isbn         = {{9783030025076}},
  issn         = {{0302-9743}},
  pages        = {{435--454}},
  publisher    = {{Springer International Publishing}},
  title        = {{{Information Flow Certificates}}},
  doi          = {{10.1007/978-3-030-02508-3_23}},
  year         = {{2018}},
}

@inproceedings{5769,
  abstract     = {{Information Flow Analysis (IFA) aims at detecting illegal flows of information between program entities. “Legality” is therein specified in terms of various security policies. For the analysis, this opens up two possibilities: building generic, policy independent and building specific, policy dependent IFAs. While the former needs to track all dependencies between program entities, the latter allows for a reduced and thus more efficient analysis.

In this paper, we start out by formally defining a policy independent information flow analysis. Next, we show how to specialize this IFA via policy specific variable tracking, and prove soundness of the specialization. We furthermore investigate refinement relationships between policies, allowing an IFA for one policy to be employed for its refinements. As policy refinement depends on concrete program entities, we additionally propose a precomputation of policy refinement conditions, enabling an efficient refinement check for concrete programs.}},
  author       = {{Töws, Manuel and Wehrheim, Heike}},
  booktitle    = {{Formal Methods and Software Engineering - 19th International Conference  on Formal Engineering Methods (ICFEM 2017)}},
  isbn         = {{9783319686899}},
  issn         = {{0302-9743}},
  pages        = {{362--378}},
  publisher    = {{Springer International Publishing}},
  title        = {{{Policy Dependent and Independent Information Flow Analyses}}},
  doi          = {{10.1007/978-3-319-68690-5_22}},
  year         = {{2017}},
}

@inproceedings{227,
  abstract     = {{Information flow analysis studies the flow of data between program entities (e.g. variables), where the allowed flow is specified via security policies. Typical information flow analyses compute a conservative (over-)approximation of the flows in a program. Such an analysis may thus signal non-existing violations of the security policy.In this paper, we propose a new technique for inspecting the reported violations (counterexamples) for spuriousity. Similar to counterexample-guided-abstraction-refinement (CEGAR) in software verification, we use the result of this inspection to improve the next round of the analysis. We prove soundness of this scheme.}},
  author       = {{Töws, Manuel and Wehrheim, Heike}},
  booktitle    = {{Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)}},
  pages        = {{466----483}},
  title        = {{{A CEGAR Scheme for Information Flow Analysis}}},
  doi          = {{10.1007/978-3-319-47846-3_29}},
  year         = {{2016}},
}

@inproceedings{170,
  abstract     = {{We present PAndA2, an extendable, static analysis tool for Android  apps  which  examines  permission  related security  threats  like overprivilege, existence of permission redelegation and permission flows. PAndA2 comes along with a textual and graphical visualization of the analysis result and even supports the comparison of analysis results for different android app versions.}},
  author       = {{Jakobs, Marie-Christine and Töws, Manuel and Pauck, Felix}},
  booktitle    = {{Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems}},
  editor       = {{Ishikawa F, Romanovsky A, Troubitsyna E}},
  title        = {{{PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper)}}},
  year         = {{2016}},
}

@misc{359,
  author       = {{Töws, Manuel}},
  publisher    = {{Universität Paderborn}},
  title        = {{{Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen in SMT-LIB}}},
  year         = {{2014}},
}