Sie haben Javascript deaktiviert!
Sie haben versucht eine Funktion zu nutzen, die nur mit Javascript möglich ist. Um sämtliche Funktionalitäten unserer Internetseite zu nutzen, aktivieren Sie bitte Javascript in Ihrem Browser.

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right) Show image information

Jan Haltermann, Manuel Töws, Felix Pauck, Cedric Richter, Heike Wehrheim, Jürgen König, Arnab Sharma, Steffen Beringer, Oleksandra Koslova, Elisabeth Schlatt (left to right)

Manuel Töws, M. Sc.

Address:Manuel Töws
Paderborn University
Faculty of Electrical Engineering, Computer Science and Mathematics
Warburger Str. 100
D-33098 Paderborn, Germany
Phone:+49 (0) 5251-60-4272
Fax: +49 (0) 5251-60-3993 
Secretary:Elisabeth Schlatt
Phone: +49 (0) 5251-60-3764
Email: schlatt(at)
Office: O4.125


SS 2018L.079.07502Proseminar: Android App AnalyseSupervisor
Former Teaching
WS 2017/18L.079.05101ModellierungOrganization+Tutor
WS 2017/18L.079.08000Seminar: Software Transactional MemorySupervisor
SS 2017L.079.05200Grundlagen der Programmierung 2Organization+Tutor
SS 2017L.079.07500Proseminar: Software Analyse Verfahren und WerkzeugeSupervisor
WS 2016/17L.079.05301Grundlagen der RechnerarchitekturTutor
WS 2016/17L.079.08000Seminar: Formal Models for Safe and Secure SystemsSupervisor
SS 2016L.079.05200Grundlagen der Programmierung 2Organization+Tutor
SS 2016L.079.07500Proseminar: Moderne ProgrammiersprachenSupervisor
WS 2015/16L.079.07014Project Group: A³: Android App AnalysisOrganization+Supervisor
SS 2015L.079.07014Project Group: A³: Android App AnalysisOrganization+Supervisor


Open list in Research Information System


Information Flow Certificates

M. Töws, H. Wehrheim, in: Theoretical Aspects of Computing – ICTAC 2018, Springer International Publishing, 2018, pp. 435-454

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.


Policy Dependent and Independent Information Flow Analyses

M. Töws, H. Wehrheim, in: Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods (ICFEM 2017), Springer International Publishing, 2017, pp. 362-378

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.


PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper)

M. Jakobs, M. Töws, F. Pauck, in: Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems, 2016

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.

A CEGAR Scheme for Information Flow Analysis

M. Töws, H. Wehrheim, in: Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016), 2016, pp. 466--483

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.


Open list in Research Information System

The University for the Information Society