TY - CONF AU - Richter, Cedric AU - Haltermann, Jan Frederik AU - Jakobs, Marie-Christine AU - Pauck, Felix AU - Schott, Stefan AU - Wehrheim, Heike ID - 35426 T2 - 37th IEEE/ACM International Conference on Automated Software Engineering TI - Are Neural Bug Detectors Comparable to Software Developers on Variable Misuse Bugs? ER - TY - CONF AB - We present CLARC (Cryptographic Library for Anonymous Reputation and Credentials), an anonymous credentials system (ACS) combined with an anonymous reputation system. Using CLARC, users can receive attribute-based credentials from issuers. They can efficiently prove that their credentials satisfy complex (access) policies in a privacy-preserving way. This implements anonymous access control with complex policies. Furthermore, CLARC is the first ACS that is combined with an anonymous reputation system where users can anonymously rate services. A user who gets access to a service via a credential, also anonymously receives a review token to rate the service. If a user creates more than a single rating, this can be detected by anyone, preventing users from spamming ratings to sway public opinion. To evaluate feasibility of our construction, we present an open-source prototype implementation. AU - Bemmann, Kai AU - Blömer, Johannes AU - Bobolz, Jan AU - Bröcher, Henrik AU - Diemert, Denis Pascal AU - Eidens, Fabian AU - Eilers, Lukas AU - Haltermann, Jan Frederik AU - Juhnke, Jakob AU - Otour, Burhan AU - Porzenheim, Laurens Alexander AU - Pukrop, Simon AU - Schilling, Erik AU - Schlichtig, Michael AU - Stienemeier, Marcel ID - 3265 SN - 978-1-4503-6448-5 T2 - Proceedings of the 13th International Conference on Availability, Reliability and Security - ARES '18 TI - Fully-Featured Anonymous Credentials with Reputation System 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 - GEN AU - Haltermann, Jan Frederik ID - 12885 TI - Analyzing Data Usage in Array Programs ER - TY - GEN AB - Software verification has recently made enormous progress due to the development of novel verification methods and the speed-up of supporting technologies like SMT solving. To keep software verification tools up to date with these advances, tool developers keep on integrating newly designed methods into their tools, almost exclusively by re-implementing the method within their own framework. While this allows for a conceptual re-use of methods, it requires novel implementations for every new technique. In this paper, we employ cooperative verification in order to avoid reimplementation and enable usage of novel tools as black-box components in verification. Specifically, cooperation is employed for the core ingredient of software verification which is invariant generation. Finding an adequate loop invariant is key to the success of a verification run. Our framework named CoVerCIG allows a master verification tool to delegate the task of invariant generation to one or several specialized helper invariant generators. Their results are then utilized within the verification run of the master verifier, allowing in particular for crosschecking the validity of the invariant. We experimentally evaluate our framework on an instance with two masters and three different invariant generators using a number of benchmarks from SV-COMP 2020. The experiments show that the use of CoVerCIG can increase the number of correctly verified tasks without increasing the used resources AU - Haltermann, Jan Frederik AU - Wehrheim, Heike ID - 17825 T2 - arXiv:2008.04551 TI - Cooperative Verification via Collective Invariant Generation ER -