TY - GEN AU - Rautenberg, Kai ID - 3320 TI - Korrektheitsbeweise für Muster von Servicekompositionen ER - TY - CONF AB - Over the years, Design by Contract (DbC) has evolved as a powerful concept for program documentation, testing, and verification. Contracts formally specify assertions on (mostly) object-oriented programs: pre- and postconditions of methods, class invariants, allowed call orders, etc. Missing in the long list of properties specifiable by contracts are, however, method correlations: DbC languages fall short on stating assertions relating methods. In this paper, we propose the novel concept of inter-method contract, allowing precisely for expressing method correlations.We present JMC as a language for specifying and JMCTest as a tool for dynamically checking inter-method contracts on Java programs. JMCTest fully automatically generates objects on which the contracted methods are called and the validity of the contract is checked. Using JMCTest, we detected that large Java code bases (e.g. JBoss, Java RT) frequently violate standard inter-method contracts. In comparison to other verification tools inspecting (some) inter-method contracts, JMCTest can find bugs that remain undetected by those tools. AU - Börding, Paul AU - Haltermann, Jan Frederik AU - Jakobs, Marie-Christine AU - Wehrheim, Heike ID - 3414 T2 - Proceedings of the IFIP International Conference on Testing Software and Systems (ICTSS 2018) TI - JMCTest: Automatically Testing Inter-Method Contracts in Java VL - 11146 ER - TY - CHAP AU - Schellhorn, Gerhard AU - Wedel, Monika AU - Travkin, Oleg AU - König, Jürgen AU - Wehrheim, Heike ID - 3536 SN - 0302-9743 T2 - Software Engineering and Formal Methods TI - FastLane Is Opaque – a Case Study in Mechanized Proofs of Opacity ER - TY - JOUR AU - Doherty, Simon AU - Derrick, John AU - Dongol, Brijesh AU - Wehrheim, Heike ID - 3153 JF - CoRR TI - Causal Linearizability: Compositionality for Partially Ordered Executions ER - TY - GEN AB - In recent years, researchers have developed a number of tools to conduct taint analysis of Android applications. While all the respective papers aim at providing a thorough empirical evaluation, comparability is hindered by varying or unclear evaluation targets. Sometimes, the apps used for evaluation are not precisely described. In other cases, authors use an established benchmark but cover it only partially. In yet other cases, the evaluations differ in terms of the data leaks searched for, or lack a ground truth to compare against. All those limitations make it impossible to truly compare the tools based on those published evaluations. We thus present ReproDroid, a framework allowing the accurate comparison of Android taint analysis tools. ReproDroid supports researchers in inferring the ground truth for data leaks in apps, in automatically applying tools to benchmarks, and in evaluating the obtained results. We use ReproDroid to comparatively evaluate on equal grounds the six prominent taint analysis tools Amandroid, DIALDroid, DidFail, DroidSafe, FlowDroid and IccTA. The results are largely positive although four tools violate some promises concerning features and accuracy. Finally, we contribute to the area of unbiased benchmarking with a new and improved version of the open test suite DroidBench. AU - Pauck, Felix AU - Bodden, Eric AU - Wehrheim, Heike ID - 2711 T2 - arXiv:1804.02903 TI - Do Android Taint Analysis Tools Keep their Promises? ER - TY - CONF AB - 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. AU - Töws, Manuel AU - Wehrheim, Heike ID - 5774 SN - 0302-9743 T2 - Theoretical Aspects of Computing – ICTAC 2018 TI - Information Flow Certificates ER - TY - CONF AU - Pauck, Felix AU - Bodden, Eric AU - Wehrheim, Heike ID - 4999 SN - 9781450355735 T2 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2018 TI - Do Android taint analysis tools keep their promises? ER - TY - JOUR AU - Derrick, John AU - Doherty, Simon AU - Dongol, Brijesh AU - Schellhorn, Gerhard AU - Travkin, Oleg AU - Wehrheim, Heike ID - 6828 IS - 5 JF - Formal Asp. Comput. TI - Mechanized proofs of opacity: a comparison of two techniques VL - 30 ER - TY - CONF AU - Doherty, Simon AU - Dongol, Brijesh AU - Wehrheim, Heike AU - Derrick, John ID - 6836 T2 - Integrated Formal Methods - 14th International Conference, {IFM} 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings TI - Making Linearizability Compositional for Partially Ordered Executions ER - TY - CONF AU - Doherty, Simon AU - Dongol, Brijesh AU - Wehrheim, Heike AU - Derrick, John ID - 6838 T2 - Integrated Formal Methods - 14th International Conference, {IFM} 2018, Maynooth, Ireland, September 5-7, 2018, Proceedings TI - Making Linearizability Compositional for Partially Ordered Executions ER -