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