---
_id: '5774'
abstract:
- lang: eng
  text: 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:
- first_name: Manuel
  full_name: Töws, Manuel
  id: '11315'
  last_name: Töws
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Töws M, Wehrheim H. Information Flow Certificates. In: <i>Theoretical Aspects
    of Computing – ICTAC 2018</i>. Cham: Springer International Publishing; 2018:435-454.
    doi:<a href="https://doi.org/10.1007/978-3-030-02508-3_23">10.1007/978-3-030-02508-3_23</a>'
  apa: 'Töws, M., &#38; Wehrheim, H. (2018). Information Flow Certificates. In <i>Theoretical
    Aspects of Computing – ICTAC 2018</i> (pp. 435–454). Cham: Springer International
    Publishing. <a href="https://doi.org/10.1007/978-3-030-02508-3_23">https://doi.org/10.1007/978-3-030-02508-3_23</a>'
  bibtex: '@inproceedings{Töws_Wehrheim_2018, place={Cham}, title={Information Flow
    Certificates}, DOI={<a href="https://doi.org/10.1007/978-3-030-02508-3_23">10.1007/978-3-030-02508-3_23</a>},
    booktitle={Theoretical Aspects of Computing – ICTAC 2018}, publisher={Springer
    International Publishing}, author={Töws, Manuel and Wehrheim, Heike}, year={2018},
    pages={435–454} }'
  chicago: 'Töws, Manuel, and Heike Wehrheim. “Information Flow Certificates.” In
    <i>Theoretical Aspects of Computing – ICTAC 2018</i>, 435–54. Cham: Springer International
    Publishing, 2018. <a href="https://doi.org/10.1007/978-3-030-02508-3_23">https://doi.org/10.1007/978-3-030-02508-3_23</a>.'
  ieee: M. Töws and H. Wehrheim, “Information Flow Certificates,” in <i>Theoretical
    Aspects of Computing – ICTAC 2018</i>, 2018, pp. 435–454.
  mla: Töws, Manuel, and Heike Wehrheim. “Information Flow Certificates.” <i>Theoretical
    Aspects of Computing – ICTAC 2018</i>, Springer International Publishing, 2018,
    pp. 435–54, doi:<a href="https://doi.org/10.1007/978-3-030-02508-3_23">10.1007/978-3-030-02508-3_23</a>.
  short: 'M. Töws, H. Wehrheim, in: Theoretical Aspects of Computing – ICTAC 2018,
    Springer International Publishing, Cham, 2018, pp. 435–454.'
date_created: 2018-11-21T09:51:37Z
date_updated: 2022-01-06T07:02:40Z
ddc:
- '000'
department:
- _id: '77'
doi: 10.1007/978-3-030-02508-3_23
file:
- access_level: closed
  content_type: application/pdf
  creator: mtoews
  date_created: 2018-11-26T15:11:32Z
  date_updated: 2018-11-26T15:11:32Z
  file_id: '5837'
  file_name: Töws-Wehrheim2018_Chapter_InformationFlowCertificates.pdf
  file_size: 518016
  relation: main_file
  success: 1
file_date_updated: 2018-11-26T15:11:32Z
has_accepted_license: '1'
language:
- iso: eng
page: 435-454
place: Cham
project:
- _id: '1'
  name: SFB 901
- _id: '3'
  name: SFB 901 - Project Area B
- _id: '12'
  name: SFB 901 - Subproject B4
publication: Theoretical Aspects of Computing – ICTAC 2018
publication_identifier:
  isbn:
  - '9783030025076'
  - '9783030025083'
  issn:
  - 0302-9743
  - 1611-3349
publication_status: published
publisher: Springer International Publishing
status: public
title: Information Flow Certificates
type: conference
user_id: '477'
year: '2018'
...
---
_id: '5769'
abstract:
- lang: eng
  text: "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.\r\n\r\nIn 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:
- first_name: Manuel
  full_name: Töws, Manuel
  id: '11315'
  last_name: Töws
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Töws M, Wehrheim H. Policy Dependent and Independent Information Flow Analyses.
    In: <i>Formal Methods and Software Engineering - 19th International Conference 
    on Formal Engineering Methods (ICFEM 2017)</i>. Springer International Publishing;
    2017:362-378. doi:<a href="https://doi.org/10.1007/978-3-319-68690-5_22">10.1007/978-3-319-68690-5_22</a>'
  apa: Töws, M., &#38; Wehrheim, H. (2017). Policy Dependent and Independent Information
    Flow Analyses. In <i>Formal Methods and Software Engineering - 19th International
    Conference  on Formal Engineering Methods (ICFEM 2017)</i> (pp. 362–378). Springer
    International Publishing. <a href="https://doi.org/10.1007/978-3-319-68690-5_22">https://doi.org/10.1007/978-3-319-68690-5_22</a>
  bibtex: '@inproceedings{Töws_Wehrheim_2017, title={Policy Dependent and Independent
    Information Flow Analyses}, DOI={<a href="https://doi.org/10.1007/978-3-319-68690-5_22">10.1007/978-3-319-68690-5_22</a>},
    booktitle={Formal Methods and Software Engineering - 19th International Conference 
    on Formal Engineering Methods (ICFEM 2017)}, publisher={Springer International
    Publishing}, author={Töws, Manuel and Wehrheim, Heike}, year={2017}, pages={362–378}
    }'
  chicago: Töws, Manuel, and Heike Wehrheim. “Policy Dependent and Independent Information
    Flow Analyses.” In <i>Formal Methods and Software Engineering - 19th International
    Conference  on Formal Engineering Methods (ICFEM 2017)</i>, 362–78. Springer International
    Publishing, 2017. <a href="https://doi.org/10.1007/978-3-319-68690-5_22">https://doi.org/10.1007/978-3-319-68690-5_22</a>.
  ieee: M. Töws and H. Wehrheim, “Policy Dependent and Independent Information Flow
    Analyses,” in <i>Formal Methods and Software Engineering - 19th International
    Conference  on Formal Engineering Methods (ICFEM 2017)</i>, 2017, pp. 362–378.
  mla: Töws, Manuel, and Heike Wehrheim. “Policy Dependent and Independent Information
    Flow Analyses.” <i>Formal Methods and Software Engineering - 19th International
    Conference  on Formal Engineering Methods (ICFEM 2017)</i>, Springer International
    Publishing, 2017, pp. 362–78, doi:<a href="https://doi.org/10.1007/978-3-319-68690-5_22">10.1007/978-3-319-68690-5_22</a>.
  short: '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.'
date_created: 2018-11-21T09:38:43Z
date_updated: 2022-01-06T07:02:39Z
ddc:
- '000'
department:
- _id: '77'
doi: 10.1007/978-3-319-68690-5_22
file:
- access_level: closed
  content_type: application/pdf
  creator: mtoews
  date_created: 2018-11-26T15:07:42Z
  date_updated: 2018-11-26T15:07:42Z
  file_id: '5836'
  file_name: Töws-Wehrheim2017_Chapter_PolicyDependentAndIndependentI.pdf
  file_size: 424031
  relation: main_file
  success: 1
file_date_updated: 2018-11-26T15:07:42Z
has_accepted_license: '1'
language:
- iso: eng
page: 362-378
project:
- _id: '12'
  name: SFB 901 - Subproject B4
- _id: '3'
  name: SFB 901 - Project Area B
- _id: '1'
  name: SFB 901
publication: Formal Methods and Software Engineering - 19th International Conference  on
  Formal Engineering Methods (ICFEM 2017)
publication_identifier:
  isbn:
  - '9783319686899'
  - '9783319686905'
  issn:
  - 0302-9743
  - 1611-3349
publication_status: published
publisher: Springer International Publishing
status: public
title: Policy Dependent and Independent Information Flow Analyses
type: conference
user_id: '477'
year: '2017'
...
---
_id: '227'
abstract:
- lang: eng
  text: 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:
- first_name: Manuel
  full_name: Töws, Manuel
  id: '11315'
  last_name: Töws
- first_name: Heike
  full_name: Wehrheim, Heike
  id: '573'
  last_name: Wehrheim
citation:
  ama: 'Töws M, Wehrheim H. A CEGAR Scheme for Information Flow Analysis. In: <i>Proceedings
    of the 18th International Conference on Formal Engineering Methods (ICFEM 2016)</i>.
    LNCS. ; 2016:466--483. doi:<a href="https://doi.org/10.1007/978-3-319-47846-3_29">10.1007/978-3-319-47846-3_29</a>'
  apa: Töws, M., &#38; Wehrheim, H. (2016). A CEGAR Scheme for Information Flow Analysis.
    In <i>Proceedings of the 18th International Conference on Formal Engineering Methods
    (ICFEM 2016)</i> (pp. 466--483). <a href="https://doi.org/10.1007/978-3-319-47846-3_29">https://doi.org/10.1007/978-3-319-47846-3_29</a>
  bibtex: '@inproceedings{Töws_Wehrheim_2016, series={LNCS}, title={A CEGAR Scheme
    for Information Flow Analysis}, DOI={<a href="https://doi.org/10.1007/978-3-319-47846-3_29">10.1007/978-3-319-47846-3_29</a>},
    booktitle={Proceedings of the 18th International Conference on Formal Engineering
    Methods (ICFEM 2016)}, author={Töws, Manuel and Wehrheim, Heike}, year={2016},
    pages={466--483}, collection={LNCS} }'
  chicago: Töws, Manuel, and Heike Wehrheim. “A CEGAR Scheme for Information Flow
    Analysis.” In <i>Proceedings of the 18th International Conference on Formal Engineering
    Methods (ICFEM 2016)</i>, 466--483. LNCS, 2016. <a href="https://doi.org/10.1007/978-3-319-47846-3_29">https://doi.org/10.1007/978-3-319-47846-3_29</a>.
  ieee: M. Töws and H. Wehrheim, “A CEGAR Scheme for Information Flow Analysis,” in
    <i>Proceedings of the 18th International Conference on Formal Engineering Methods
    (ICFEM 2016)</i>, 2016, pp. 466--483.
  mla: Töws, Manuel, and Heike Wehrheim. “A CEGAR Scheme for Information Flow Analysis.”
    <i>Proceedings of the 18th International Conference on Formal Engineering Methods
    (ICFEM 2016)</i>, 2016, pp. 466--483, doi:<a href="https://doi.org/10.1007/978-3-319-47846-3_29">10.1007/978-3-319-47846-3_29</a>.
  short: 'M. Töws, H. Wehrheim, in: Proceedings of the 18th International Conference
    on Formal Engineering Methods (ICFEM 2016), 2016, pp. 466--483.'
date_created: 2017-10-17T12:41:36Z
date_updated: 2022-01-06T06:55:39Z
ddc:
- '040'
department:
- _id: '77'
doi: 10.1007/978-3-319-47846-3_29
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-21T10:33:38Z
  date_updated: 2018-03-21T10:33:38Z
  file_id: '1506'
  file_name: 227-chp_3A10.1007_2F978-3-319-47846-3_29.pdf
  file_size: 682849
  relation: main_file
  success: 1
file_date_updated: 2018-03-21T10:33:38Z
has_accepted_license: '1'
language:
- iso: eng
page: 466--483
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Proceedings of the 18th International Conference on Formal Engineering
  Methods (ICFEM 2016)
series_title: LNCS
status: public
title: A CEGAR Scheme for Information Flow Analysis
type: conference
user_id: '477'
year: '2016'
...
---
_id: '170'
abstract:
- lang: eng
  text: 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:
- first_name: Marie-Christine
  full_name: Jakobs, Marie-Christine
  last_name: Jakobs
- first_name: Manuel
  full_name: Töws, Manuel
  id: '11315'
  last_name: Töws
- first_name: Felix
  full_name: Pauck, Felix
  id: '22398'
  last_name: Pauck
citation:
  ama: 'Jakobs M-C, Töws M, Pauck F. PAndA 2 : Analyzing Permission Use and Interplay
    in Android Apps (Tool Paper). In: Ishikawa F, Romanovsky A TE, ed. <i>Workshop
    on Formal and Model-Driven Techniques for Developing Trustworthy Systems</i>.
    School of Computing Science Technical Report Series. ; 2016.'
  apa: 'Jakobs, M.-C., Töws, M., &#38; Pauck, F. (2016). PAndA 2 : Analyzing Permission
    Use and Interplay in Android Apps (Tool Paper). In T. E. Ishikawa F, Romanovsky
    A (Ed.), <i>Workshop on Formal and Model-Driven Techniques for Developing Trustworthy
    Systems</i>.'
  bibtex: '@inproceedings{Jakobs_Töws_Pauck_2016, series={School of Computing Science
    Technical Report Series}, title={PAndA 2 : Analyzing Permission Use and Interplay
    in Android Apps (Tool Paper)}, booktitle={Workshop on Formal and Model-Driven
    Techniques for Developing Trustworthy Systems}, author={Jakobs, Marie-Christine
    and Töws, Manuel and Pauck, Felix}, editor={Ishikawa F, Romanovsky A, Troubitsyna
    EEditor}, year={2016}, collection={School of Computing Science Technical Report
    Series} }'
  chicago: 'Jakobs, Marie-Christine, Manuel Töws, and Felix Pauck. “PAndA 2 : Analyzing
    Permission Use and Interplay in Android Apps (Tool Paper).” In <i>Workshop on
    Formal and Model-Driven Techniques for Developing Trustworthy Systems</i>, edited
    by Troubitsyna E Ishikawa F, Romanovsky A. School of Computing Science Technical
    Report Series, 2016.'
  ieee: 'M.-C. Jakobs, M. Töws, and F. Pauck, “PAndA 2 : Analyzing Permission Use
    and Interplay in Android Apps (Tool Paper),” in <i>Workshop on Formal and Model-Driven
    Techniques for Developing Trustworthy Systems</i>, 2016.'
  mla: 'Jakobs, Marie-Christine, et al. “PAndA 2 : Analyzing Permission Use and Interplay
    in Android Apps (Tool Paper).” <i>Workshop on Formal and Model-Driven Techniques
    for Developing Trustworthy Systems</i>, edited by Troubitsyna E Ishikawa F, Romanovsky
    A, 2016.'
  short: 'M.-C. Jakobs, M. Töws, F. Pauck, in: T.E. Ishikawa F, Romanovsky A (Ed.),
    Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems,
    2016.'
date_created: 2017-10-17T12:41:25Z
date_updated: 2022-01-06T06:53:01Z
ddc:
- '040'
department:
- _id: '77'
editor:
- first_name: Troubitsyna E
  full_name: Ishikawa F, Romanovsky A, Troubitsyna E
  last_name: Ishikawa F, Romanovsky A
file:
- access_level: closed
  content_type: application/pdf
  creator: florida
  date_created: 2018-03-21T12:40:27Z
  date_updated: 2018-03-21T12:40:27Z
  file_id: '1539'
  file_name: 170-main_04.pdf
  file_size: 285299
  relation: main_file
  success: 1
file_date_updated: 2018-03-21T12:40:27Z
has_accepted_license: '1'
project:
- _id: '1'
  name: SFB 901
- _id: '12'
  name: SFB 901 - Subprojekt B4
- _id: '3'
  name: SFB 901 - Project Area B
publication: Workshop on Formal and Model-Driven Techniques for Developing Trustworthy
  Systems
related_material:
  link:
  - relation: contains
    url: https://pdfs.semanticscholar.org/58cd/94c8b2335d16aa2558f711cf81b3f7746696.pdf
series_title: School of Computing Science Technical Report Series
status: public
title: 'PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper)'
type: conference
user_id: '15504'
year: '2016'
...
---
_id: '359'
author:
- first_name: Manuel
  full_name: Töws, Manuel
  id: '11315'
  last_name: Töws
citation:
  ama: Töws M. <i>Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen
    in SMT-LIB</i>. Universität Paderborn; 2014.
  apa: Töws, M. (2014). <i>Statistisches Testen von unbeweisbaren Anforderungen an
    Programmspezifikationen in SMT-LIB</i>. Universität Paderborn.
  bibtex: '@book{Töws_2014, title={Statistisches Testen von unbeweisbaren Anforderungen
    an Programmspezifikationen in SMT-LIB}, publisher={Universität Paderborn}, author={Töws,
    Manuel}, year={2014} }'
  chicago: Töws, Manuel. <i>Statistisches Testen von unbeweisbaren Anforderungen an
    Programmspezifikationen in SMT-LIB</i>. Universität Paderborn, 2014.
  ieee: M. Töws, <i>Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen
    in SMT-LIB</i>. Universität Paderborn, 2014.
  mla: Töws, Manuel. <i>Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen
    in SMT-LIB</i>. Universität Paderborn, 2014.
  short: M. Töws, Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen
    in SMT-LIB, Universität Paderborn, 2014.
date_created: 2017-10-17T12:42:02Z
date_updated: 2022-01-06T06:59:26Z
language:
- iso: ger
project:
- _id: '1'
  name: SFB 901
- _id: '11'
  name: SFB 901 - Subprojekt B3
- _id: '3'
  name: SFB 901 - Project Area B
publisher: Universität Paderborn
status: public
title: Statistisches Testen von unbeweisbaren Anforderungen an Programmspezifikationen
  in SMT-LIB
type: mastersthesis
user_id: '15504'
year: '2014'
...