Are Neural Bug Detectors Comparable to Software Developers on Variable Misuse Bugs? - Richter, Cedric; Haltermann, Jan Frederik; Jakobs, Marie-Christine; Pauck, Felix; Schott, Stefan; Wehrheim, Heike (37th IEEE/ACM International Conference on Automated Software Engineering)

Scaling Arbitrary Android App Analyses - Pauck, Felix (37th IEEE/ACM International Conference on Automated Software Engineering)

MAAS: Hiding Trojans in Approximate Circuits - Ahmed, Qazi Arbab; Awais, Muhammad; Platzner, Marco (The 24th International Symposium on Quality Electronic Design (ISQED'23), San Francisco, Califorina USA)

Verifying Software and Reconfigurable Hardware Services - Wehrheim, Heike; Platzner, Marco; Bodden, Eric; Schubert, Philipp; Pauck, Felix; Jakobs, Marie-Christine (On-The-Fly Computing -- Individualized IT-services in dynamic markets)

On-The-Fly Computing -- Individualized IT-services in dynamic markets - Haake, Claus-Jochen; Meyer auf der Heide, Friedhelm; Platzner, Marco; Wachsmuth, Henning; Wehrheim, Heike
In the proposal for our CRC in 2011, we formulated a vision of markets for IT services that describes an approach to the provision of such services that was novel at that time and, to a large extent, remains so today: „Our vision of on-the-fly computing is that of IT services individually and automatically configured and brought to execution from flexibly combinable services traded on markets. At the same time, we aim at organizing markets whose participants maintain a lively market of services through appropriate entrepreneurial actions.“ Over the last 12 years, we have developed methods and techniques to address problems critical to the convenient, efficient, and secure use of on-the-fly computing. Among other things, we have made the description of services more convenient by allowing natural language input, increased the quality of configured services through (natural language) interaction and more efficient configuration processes and analysis procedures, made the quality of (the products of) providers in the marketplace transparent through reputation systems, and increased the resource efficiency of execution through reconfigurable heterogeneous computing nodes and an integrated treatment of service description and configuration. We have also developed network infrastructures that have a high degree of adaptivity, scalability, efficiency, and reliability, and provide cryptographic guarantees of anonymity and security for market participants and their products and services. To demonstrate the pervasiveness of the OTF computing approach, we have implemented a proof-of-concept for OTF computing that can run typical scenarios of an OTF market. We illustrated the approach using a cutting-edge application scenario – automated machine learning (AutoML). Finally, we have been pushing our work for the perpetuation of On-The-Fly Computing beyond the SFB and sharing the expertise gained in the SFB in events with industry partners as well as transfer projects. This work required a broad spectrum of expertise. Computer scientists and economists with research interests such as computer networks and distributed algorithms, security and cryptography, software engineering and verification, configuration and machine learning, computer engineering and HPC, microeconomics and game theory, business informatics and management have successfully collaborated here.

Search Space Characterization for Approximate Logic Synthesis - Witschen, Linus Matthias; Wiersema, Tobias; Reuter, Lucas David; Platzner, Marco (2022 59th ACM/IEEE Design Automation Conference (DAC))

MUSCAT: MUS-based Circuit Approximation Technique - Witschen, Linus Matthias; Wiersema, Tobias; Artmann, Matthias; Platzner, Marco (Design, Automation and Test in Europe (DATE))

Static data-flow analysis for software product lines in C - Schubert, Philipp; Gazzillo, Paul; Patterson, Zach; Braha, Julian; Schiebel, Fabian; Hermann, Ben; Wei, Shiyi; Bodden, Eric (Automated Software Engineering)
Abstract Many critical codebases are written in C, and most of them use preprocessor directives to encode variability, effectively encoding software product lines. These preprocessor directives, however, challenge any static code analysis. SPLlift, a previously presented approach for analyzing software product lines, is limited to Java programs that use a rather simple feature encoding and to analysis problems with a finite and ideally small domain. Other approaches that allow the analysis of real-world C software product lines use special-purpose analyses, preventing the reuse of existing analysis infrastructures and ignoring the progress made by the static analysis community. This work presents VarAlyzer , a novel static analysis approach for software product lines. VarAlyzer first transforms preprocessor constructs to plain C while preserving their variability and semantics. It then solves any given distributive analysis problem on transformed product lines in a variability-aware manner. VarAlyzer ’s analysis results are annotated with feature constraints that encode in which configurations each result holds. Our experiments with 95 compilation units of OpenSSL show that applying VarAlyzer enables one to conduct inter-procedural, flow-, field- and context-sensitive data-flow analyses on entire product lines for the first time, outperforming the product-based approach for highly-configurable systems.
Keywords: inter-procedural static analysis; software product lines; preprocessor; LLVM; C/C++

Learning Realistic Mutations: Bug Creation for Neural Bug Detectors - Richter, Cedric; Wehrheim, Heike (2022 IEEE Conference on Software Testing, Verification and Validation (ICST))

TSSB-3M: Mining single statement bugs at massive scale - Richter, Cedric; Wehrheim, Heike (2022 IEEE/ACM 19th International Conference on Mining Software Repositories (MSR))

On the Detection and Circumvention of Bitstream-Level Trojans in FPGAs - Ahmed, Qazi Arbab; Platzner, Marco

Weak Progressive Forward Simulation Is Necessary and Sufficient for Strong Observational Refinement - Dongol, Brijesh; Schellhorn, Gerhard; Wehrheim, Heike (33rd International Conference on Concurrency Theory, CONCUR 2022, September 12-16, 2022, Warsaw, Poland)

TaintBench: Automatic real-world malware benchmarking of Android taint analyses - Luo, Linghui; Pauck, Felix; Piskachev, Goran; Benz, Manuel; Pashchenko, Ivan; Mory, Martin; Bodden, Eric; Hermann, Ben; Massacci, Fabio (Empirical Software Engineering)
Due to the lack of established real-world benchmark suites for static taint analyses of Android applications, evaluations of these analyses are often restricted and hard to compare. Even in evaluations that do use real-world apps, details about the ground truth in those apps are rarely documented, which makes it difficult to compare and reproduce the results. To push Android taint analysis research forward, this paper thus recommends criteria for constructing real-world benchmark suites for this specific domain, and presents TaintBench, the first real-world malware benchmark suite with documented taint flows. TaintBench benchmark apps include taint flows with complex structures, and addresses static challenges that are commonly agreed on by the community. Together with the TaintBench suite, we introduce the TaintBench framework, whose goal is to simplify real-world benchmarking of Android taint analyses. First, a usability test shows that the framework improves experts’ performance and perceived usability when documenting and inspecting taint flows. Second, experiments using TaintBench reveal new insights for the taint analysis tools Amandroid and FlowDroid: (i) They are less effective on real-world malware apps than on synthetic benchmark apps. (ii) Predefined lists of sources and sinks heavily impact the tools’ accuracy. (iii) Surprisingly, up-to-date versions of both tools are less accurate than their predecessors.

On Strong Observational Refinement and Forward Simulation - Derrick, John; Doherty, Simon; Dongol, Brijesh; Schellhorn, Gerhard; Wehrheim, Heike (Proceedings of the 35th International Symposium on Distributed Computing (DISC))

Timing Optimization for Virtual FPGA Configurations - Witschen, Linus Matthias; Wiersema, Tobias; Raeisi Nafchi, Masood; Bockhorn, Arne; Platzner, Marco (Proceedings of International Symposium on Applied Reconfigurable Computing (ARC'21))

Lossless, Persisted Summarization of Static Callgraph, Points-To and Data-Flow Analysis - Schubert, Philipp; Hermann, Ben; Bodden, Eric (European Conference on Object-Oriented Programming (ECOOP))
Static analysis is used to automatically detect bugs and security breaches, and aids compileroptimization. Whole-program analysis (WPA) can yield high precision, however causes long analysistimes and thus does not match common software-development workflows, making it often impracticalto use for large, real-world applications.This paper thus presents the design and implementation ofModAlyzer, a novel static-analysisapproach that aims at accelerating whole-program analysis by making the analysis modular andcompositional. It shows how to computelossless, persisted summaries for callgraph, points-to anddata-flow information, and it reports under which circumstances this function-level compositionalanalysis outperforms WPA.We implementedModAlyzeras an extension to LLVM and PhASAR, and applied it to 12 real-world C and C++ applications. At analysis time,ModAlyzermodularly and losslessly summarizesthe analysis effect of the library code those applications share, hence avoiding its repeated re-analysis.The experimental results show that the reuse of these summaries can save, on average, 72% ofanalysis time over WPA. Moreover, because it is lossless, the module-wise analysis fully retainsprecision and recall. Surprisingly, as our results show, it sometimes even yields precision superior toWPA. The initial summary generation, on average, takes about 3.67 times as long as WPA.

Jicer: Simplifying Cooperative Android App Analysis Tasks - Pauck, Felix; Wehrheim, Heike (2021 IEEE 21st International Working Conference on Source Code Analysis and Manipulation (SCAM))

Software/Hardware Co-Verification for Custom Instruction Set Processors - Jakobs, Marie-Christine; Pauck, Felix; Platzner, Marco; Wehrheim, Heike; Wiersema, Tobias (IEEE Access)
Verification of software and processor hardware usually proceeds separately, software analysis relying on the correctness of processors executing machine instructions. This assumption is valid as long as the software runs on standard CPUs that have been extensively validated and are in wide use. However, for processors exploiting custom instruction set extensions to meet performance and energy constraints the validation might be less extensive, challenging the correctness assumption. In this paper we present a novel formal approach for hardware/software co-verification targeting processors with custom instruction set extensions. We detail two different approaches for checking whether the hardware fulfills the requirements expected by the software analysis. The approaches are designed to explore a trade-off between generality of the verification and computational effort. Then, we describe the integration of software and hardware analyses for both techniques and describe a fully automated tool chain implementing the approaches. Finally, we demonstrate and compare the two approaches on example source code with custom instructions, using state-of-the-art software analysis and hardware verification techniques.
Keywords: Software Analysis; Abstract Interpretation; Custom Instruction; Hardware Verification

Cooperative Android App Analysis with CoDiDroid - Pauck, Felix; Wehrheim, Heike (Software Engineering 2021)

Hardware Trojans in Reconfigurable Computing - Ahmed, Qazi Arbab (2021 IFIP/IEEE 29th International Conference on Very Large Scale Integration (VLSI-SoC))

Malicious Routing: Circumventing Bitstream-level Verification for FPGAs - Ahmed, Qazi Arbab; Wiersema, Tobias; Platzner, Marco (2021 Design, Automation & Test in Europe Conference & Exhibition (DATE))
The battle of developing hardware Trojans and corresponding countermeasures has taken adversaries towards ingenious ways of compromising hardware designs by circumventing even advanced testing and verification methods. Besides conventional methods of inserting Trojans into a design by a malicious entity, the design flow for field-programmable gate arrays (FPGAs) can also be surreptitiously compromised to assist the attacker to perform a successful malfunctioning or information leakage attack. The advanced stealthy malicious look-up-table (LUT) attack activates a Trojan only when generating the FPGA bitstream and can thus not be detected by register transfer and gate level testing and verification. However, also this attack was recently revealed by a bitstream-level proof-carrying hardware (PCH) approach. In this paper, we present a novel attack that leverages malicious routing of the inserted Trojan circuit to acquire a dormant state even in the generated and transmitted bitstream. The Trojan's payload is connected to primary inputs/outputs of the FPGA via a programmable interconnect point (PIP). The Trojan is detached from inputs/outputs during place-and-route and re-connected only when the FPGA is being programmed, thus activating the Trojan circuit without any need for a trigger logic. Since the Trojan is injected in a post-synthesis step and remains unconnected in the bitstream, the presented attack can currently neither be prevented by conventional testing and verification methods nor by recent bitstream-level verification techniques.

Into the Woods: Experiences from Building a Dataflow Analysis Framework for C/C++ - Schubert, Philipp; Hermann, Ben; Bodden, Eric; Leer, Richard (SCAM '21: IEEE International Working Conference on Source Code Analysis and Manipulation (Engineering Track))

Modeling the Effects of Global Variables in Data-Flow Analysis for C/C++ - Schubert, Philipp; Sattler, Florian; Schiebel, Fabian; Hermann, Ben; Bodden, Eric (2021 IEEE 21st International Working Conference on Source Code Analysis and Manipulation (SCAM))

Proof-carrying Approximate Circuits - Witschen, Linus Matthias; Wiersema, Tobias; Platzner, Marco (IEEE Transactions On Very Large Scale Integration Systems)
Approximate circuits trade-off computational accuracy against improvements in hardware area, delay, or energy consumption. IP core vendors who wish to create such circuits need to convince consumers of the resulting approximation quality. As a solution we propose proof-carrying approximate circuits: The vendor creates an approximate IP core together with a certificate that proves the approximation quality. The proof certificate is bundled with the approximate IP core and sent off to the consumer. The consumer can formally verify the approximation quality of the IP core at a fraction of the typical computational cost for formal verification. In this paper, we first make the case for proof-carrying approximate circuits and then demonstrate the feasibility of the approach by a set of synthesis experiments using an exemplary approximation framework.
Keywords: Approximate circuit synthesis; approximate computing; error metrics; formal verification; proof-carrying hardware

Accelerating Static Call-Graph, Points-to and Data-Flow Analysis Through Persisted Summaries - Schubert, Philipp; Bodden, Eric; Hermann, Ben

Search Space Characterization for AxC Synthesis - Witschen, Linus Matthias; Wiersema, Tobias; Platzner, Marco (Fifth Workshop on Approximate Computing (AxC 2020))
On the circuit level, the design paradigm Approximate Computing seeks to trade off computational accuracy against a target metric, e.g., energy consumption. This trade-off is possible for many applications due to their inherent resiliency against inaccuracies. In the past, several automated approximation frameworks have been presented, which either utilize designated approximation techniques or libraries to replace approximable circuit parts with inaccurate versions. The frameworks invoke a search algorithm to iteratively explore the search space of performance degraded circuits, and validate their quality individually. In this paper, we propose to reverse this procedure. Rather than exploring the search space, we delineate the approximate parts of the search space which are guaranteed to lead to valid approximate circuits. Our methodology is supported by formal verification and independent of approximation techniques. Eventually, the user is provided with quality bounds of the individual approximable circuit parts. Consequently, our approach guarantees that any approximate circuit which implements these parts within the determined quality constraints satisfies the global quality constraints, superseding a subsequent quality verification. In our experimental results, we present the runtimes of our approach.

Algorithm Selection for Software Validation Based on Graph Kernels - Richter, Cedric; Hüllermeier, Eyke; Jakobs, Marie-Christine; Wehrheim, Heike (Journal of Automated Software Engineering)

A Case for a New IT Ecosystem: On-The-Fly Computing - Karl, Holger; Kundisch, Dennis; Meyer auf der Heide, Friedhelm; Wehrheim, Heike (Business & Information Systems Engineering)

CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation - Witschen, Linus Matthias; Wiersema, Tobias; Ghasemzadeh Mohammadi, Hassan; Awais, Muhammad; Platzner, Marco (Microelectronics Reliability)
Existing approaches and tools for the generation of approximate circuits often lack generality and are restricted to certain circuit types, approximation techniques, and quality assurance methods. Moreover, only few tools are publicly available. This hinders the development and evaluation of new techniques for approximating circuits and their comparison to previous approaches. In this paper, we ﬁrst analyze and classify related approaches and then present CIRCA, our ﬂexible framework for search-based approximate circuit generation. CIRCA is developed with a focus on modularity and extensibility. We present the architecture of CIRCA with its clear separation into stages and functional blocks, report on the current prototype, and show initial experiments.
Keywords: Approximate Computing; Framework; Pareto Front; Accuracy

Android App Merging for Benchmark Speed-Up and Analysis Lift-Up - Pauck, Felix; Zhang, Shikun (2019 34th IEEE/ACM International Conference on Automated Software Engineering Workshop (ASEW))
In the field of software analysis a trade-off between scalability and accuracy always exists. In this respect, Android app analysis is no exception, in particular, analyzing large or many apps can be challenging. Dealing with many small apps is a typical challenge when facing micro-benchmarks such as DROIDBENCH or ICC-BENCH. These particular benchmarks are not only used for the evaluation of novel tools but also in continuous integration pipelines of existing mature tools to maintain and guarantee a certain quality-level. Considering this latter usage it becomes very important to be able to achieve benchmark results as fast as possible. Hence, benchmarks have to be optimized for this purpose. One approach to do so is app merging. We implemented the Android Merge Tool (AMT) following this approach and show that its novel aspects can be used to produce scaled up and accurate benchmarks. For such benchmarks Android app analysis tools do not suffer from the scalability-accuracy trade-off anymore. We show this throughout detailed experiments on DROIDBENCH employing three different analysis tools (AMANDROID, ICCTA, FLOWDROID). Benchmark execution times are largely reduced without losing benchmark accuracy. Moreover, we argue why AMT is an advantageous successor of the state-of-the-art app merging tool (APKCOMBINER) in analysis lift-up scenarios.
Keywords: Program Analysis; Android App Analysis; Taint Analysis; App Merging; Benchmark

ModGuard: Identifying Integrity &Confidentiality Violations in Java Modules - Dann, Andreas; Hermann, Ben; Bodden, Eric (IEEE Transactions on Software Engineering)

Combining Verifiers in Conditional Model Checking via Reducers - Beyer, Dirk; Jakobs, Marie-Christine; Lemberger, Thomas; Wehrheim, Heike (Software Engineering and Software Management (SE/SWM 2019), Stuttgart, Germany, February 18-22, 2019)

PeSCo: Predicting Sequential Combinations of Verifiers - (Competition Contribution) - Richter, Cedric; Wehrheim, Heike (Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6-11, 2019, Proceedings, Part III)

PhASAR: An Inter-Procedural Static Analysis Framework for C/C++ - Schubert, Philipp; Hermann, Ben; Bodden, Eric (Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2019), Held as Part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2019))

Together Strong: Cooperative Android App Analysis - Pauck, Felix; Wehrheim, Heike (Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering)
Recent years have seen the development of numerous tools for the analysis of taint flows in Android apps. Taint analyses aim at detecting data leaks, accidentally or by purpose programmed into apps. Often, such tools specialize in the treatment of specific features impeding precise taint analysis (like reflection or inter-app communication). This multitude of tools, their specific applicability and their various combination options complicate the selection of a tool (or multiple tools) when faced with an analysis instance, even for knowledgeable users, and hence hinders the successful adoption of taint analyses. In this work, we thus present CoDiDroid, a framework for cooperative Android app analysis. CoDiDroid (1) allows users to ask questions about flows in apps in varying degrees of detail, (2) automatically generates subtasks for answering such questions, (3) distributes tasks onto analysis tools (currently DroidRA, FlowDroid, HornDroid, IC3 and two novel tools) and (4) at the end merges tool answers on subtasks into an overall answer. Thereby, users are freed from having to learn about the use and functionality of all these tools while still being able to leverage their capabilities. Moreover, we experimentally show that cooperation among tools pays off with respect to effectiveness, precision and scalability.
Keywords: Android Taint Analysis; Cooperation; Precision; Tools

When Are Software Verification Results Valid for Approximate Hardware? - Isenberg, Tobias; Jakobs, Marie-Christine; Pauck, Felix; Wehrheim, Heike (Tests and Proofs - 13th International Conference, TAP 2019, Held as Part of the Third World Congress on Formal Methods 2019, Porto, Portugal, October 9-11, 2019, Proceedings)

Proof-Carrying Hardware Versus the Stealthy Malicious LUT Hardware Trojan - Ahmed, Qazi Arbab; Wiersema, Tobias; Platzner, Marco (Applied Reconfigurable Computing)
Reconfigurable hardware has received considerable attention as a platform that enables dynamic hardware updates and thus is able to adapt new configurations at runtime. However, due to their dynamic nature, e.g., field-programmable gate arrays (FPGA) are subject to a constant possibility of attacks, since each new configuration might be compromised. Trojans for reconfigurable hardware that evade state-of-the-art detection techniques and even formal verification, are thus a large threat to these devices. One such stealthy hardware Trojan, that is inserted and activated in two stages by compromised electronic design automation (EDA) tools, has recently been presented and shown to evade all forms of classical pre-configuration detection techniques. This paper presents a successful pre-configuration countermeasure against this ``Malicious Look-up-table (LUT)''-hardware Trojan, by employing bitstream-level Proof-Carrying Hardware (PCH). We show that the method is able to alert innocent module creators to infected EDA tools, and to prohibit malicious ones to sell infected modules to unsuspecting customers.

Know your analysis: how instrumentation aids understanding static analysis - Schubert, Philipp; Leer, Richard; Hermann, Ben; Bodden, Eric (Proceedings of the 8th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis - SOAP 2019)

An FPGA/HMC-Based Accelerator for Resolution Proof Checking - Hansmeier, Tim; Platzner, Marco; Andrews, David (ARC 2018: Applied Reconfigurable Computing. Architectures, Tools, and Applications)
Modern Boolean satisfiability solvers can emit proofs of unsatisfiability. There is substantial interest in being able to verify such proofs and also in using them for further computations. In this paper, we present an FPGA accelerator for checking resolution proofs, a popular proof format. Our accelerator exploits parallelism at the low level by implementing the basic resolution step in hardware, and at the high level by instantiating a number of parallel modules for proof checking. Since proof checking involves highly irregular memory accesses, we employ Hybrid Memory Cube technology for accelerator memory. The results show that while the accelerator is scalable and achieves speedups for all benchmark proofs, performance improvements are currently limited by the overhead of transitioning the proof into the accelerator memory.

CIRCA: Towards a Modular and Extensible Framework for Approximate Circuit Generation - Witschen, Linus Matthias; Wiersema, Tobias; Ghasemzadeh Mohammadi, Hassan; Awais, Muhammad; Platzner, Marco (Third Workshop on Approximate Computing (AxC 2018))
Existing approaches and tools for the generation of approximate circuits often lack generality and are restricted to certain circuit types, approximation techniques, and quality assurance methods. Moreover, only few tools are publicly available. This hinders the development and evaluation of new techniques for approximating circuits and their comparison to previous approaches. In this paper, we ﬁrst analyze and classify related approaches and then present CIRCA, our ﬂexible framework for search-based approximate circuit generation. CIRCA is developed with a focus on modularity and extensibility. We present the architecture of CIRCA with its clear separation into stages and functional blocks, report on the current prototype, and show initial experiments.
Keywords: Approximate Computing; Framework; Pareto Front; Accuracy

Do Android Taint Analysis Tools Keep their Promises? - Pauck, Felix; Bodden, Eric; Wehrheim, Heike (arXiv:1804.02903)
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.

Making the Case for Proof-carrying Approximate Circuits - Witschen, Linus Matthias; Wiersema, Tobias; Platzner, Marco (4th Workshop On Approximate Computing (WAPCO 2018))

Information Flow Certificates - Töws, Manuel; Wehrheim, Heike (Theoretical Aspects of Computing – ICTAC 2018)
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.

Do Android taint analysis tools keep their promises? - Pauck, Felix; Bodden, Eric; Wehrheim, Heike (Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - ESEC/FSE 2018)

CrySL: An Extensible Approach to Validating the Correct Usage of Cryptographic APIs - Krüger, Stefan; Späth, Johannes; Ali, Karim; Bodden, Eric; Mezini, Mira (European Conference on Object-Oriented Programming (ECOOP))
Keywords: ITSECWEBSITE; CROSSING

Validity of Software Verification Results on Approximate Hardware - Isenberg, Tobias; Jakobs, Marie-Christine; Pauck, Felix; Wehrheim, Heike (IEEE Embedded Systems Letters)
Approximate computing (AC) is an emerging paradigm for energy-efficient computation. The basic idea of AC is to sacrifice high precision for low energy by allowing hardware to carry out “approximately correct” calculations. This provides a major challenge for software quality assurance: programs successfully verified to be correct might be erroneous on approximate hardware. In this letter, we present a novel approach for determining under what conditions a software verification result is valid for approximate hardware. To this end, we compute the allowed tolerances for AC hardware from successful verification runs. More precisely, we derive a set of constraints which—when met by the AC hardware—guarantees the verification result to carry over to AC. On the practical side, we furthermore: 1) show how to extract tolerances from verification runs employing predicate abstraction as verification technology and 2) show how to check such constraints on hardware designs. We have implemented all techniques, and exemplify them on example C programs and a number of recently proposed approximate adders.

Reducer-Based Construction of Conditional Verifiers - Beyer, Dirk; Jakobs, Marie-Christine; Lemberger, Thomas; Wehrheim, Heike (Proceedings of the 40th International Conference on Software Engineering (ICSE))
to appear

Compact Proof Witnesses - Jakobs, Marie-Christine; Wehrheim, Heike (NASA Formal Methods: 9th International Symposium)
Proof witnesses are proof artifacts showing correctness of programs wrt. safety properties. The recent past has seen a rising interest in witnesses as (a) proofs in a proof-carrying-code context, (b) certificates for the correct functioning of verification tools, or simply (c) exchange formats for (partial) verification results. As witnesses in all theses scenarios need to be stored and processed, witnesses are required to be as small as possible. However, software verification tools – the prime suppliers of witnesses – do not necessarily construct small witnesses. In this paper, we present a formal account of proof witnesses. We introduce the concept of weakenings, reducing the complexity of proof witnesses while preserving the ability of witnessing safety. We develop aweakening technique for a specific class of program analyses, and prove it to be sound. Finally, we experimentally demonstrate our weakening technique to indeed achieve a size reduction of proof witnesses.

Certiﬁcation Matters for Service Markets - Jakobs, Marie-Christine; Krämer, Julia; van Straaten, Dirk; Lettmann, Theodor (The Ninth International Conferences on Advanced Service Computing (SERVICE COMPUTATION))
Whenever customers have to decide between different instances of the same product, they are interested in buying the best product. In contrast, companies are interested in reducing the construction effort (and usually as a consequence thereof, the quality) to gain profit. The described setting is widely known as opposed preferences in quality of the product and also applies to the context of service-oriented computing. In general, service-oriented computing emphasizes the construction of large software systems out of existing services, where services are small and self-contained pieces of software that adhere to a specified interface. Several implementations of the same interface are considered as several instances of the same service. Thereby, customers are interested in buying the best service implementation for their service composition wrt. to metrics, such as costs, energy, memory consumption, or execution time. One way to ensure the service quality is to employ certificates, which can come in different kinds: Technical certificates proving correctness can be automatically constructed by the service provider and again be automatically checked by the user. Digital certificates allow proof of the integrity of a product. Other certificates might be rolled out if service providers follow a good software construction principle, which is checked in annual audits. Whereas all of these certificates are handled differently in service markets, what they have in common is that they influence the buying decisions of customers. In this paper, we review state-of-the-art developments in certification with respect to service-oriented computing. We not only discuss how certificates are constructed and handled in service-oriented computing but also review the effects of certificates on the market from an economic perspective.

Incremental Inductive Verification of Parameterized Timed Systems - Isenberg, Tobias (ACM Transactions on Embedded Computing Systems)
We propose and extend an approach for the verification of safety properties for parameterized timed systems modeled as networks of timed automata. For this task, we introduce an incremental workflow that is based on our algorithm IC3 with Zones. It proceeds in a cycle in which single models of the system are verified, and the verification results are employed for the reasoning about the entire system. Starting with the smallest instances, the verification of the safety property is carried out fast and efficient. On successful verification, the algorithm produces an inductive strengthening of the safety property. We reuse this result and try to reason about the entire parameterized timed system. To this end, we extrapolate the inductive strengthening into a candidate for the next-larger model. In case this candidate is a valid inductive strengthening for the next larger model, our main theorem reasons about all models of the parameterized timed system, stating that the safety property holds true for all models. Otherwise, the main cycle starts over with the verification of the next larger model. This workflow is iterated indefinitely, until able to reason about the entire parameterized timed system, until a counterexample trace is found, or until the single models become too large to be handled in the verification. We reuse the intermediate results in a Feedback-loop in order to accelerate the verification runs for the single models. Furthermore, we consider an extended formalism in comparison to our previous publications.

Policy Dependent and Independent Information Flow Analyses - Töws, Manuel; Wehrheim, Heike (Formal Methods and Software Engineering - 19th International Conference on Formal Engineering Methods (ICFEM 2017))
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.

Predicting Rankings of Software Verification Tools - Czech, Mike; Hüllermeier, Eyke; Jakobs, Marie-Christine; Wehrheim, Heike (Proceedings of the 3rd International Workshop on Software Analytics)
Today, software verification tools have reached the maturity to be used for large scale programs. Different tools perform differently well on varying code. A software developer is hence faced with the problem of choosing a tool appropriate for her program at hand. A ranking of tools on programs could facilitate the choice. Such rankings can, however, so far only be obtained by running all considered tools on the program.In this paper, we present a machine learning approach to predicting rankings of tools on programs. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for programs. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from the software verification competition SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy (rank correlation > 0.6).

Predicting Rankings of Software Verification Competitions - Czech, Mike; Hüllermeier, Eyke; Jakobs, Marie-Christine; Wehrheim, Heike
Software verification competitions, such as the annual SV-COMP, evaluate software verification tools with respect to their effectivity and efficiency. Typically, the outcome of a competition is a (possibly category-specific) ranking of the tools. For many applications, such as building portfolio solvers, it would be desirable to have an idea of the (relative) performance of verification tools on a given verification task beforehand, i.e., prior to actually running all tools on the task.In this paper, we present a machine learning approach to predicting rankings of tools on verification tasks. The method builds upon so-called label ranking algorithms, which we complement with appropriate kernels providing a similarity measure for verification tasks. Our kernels employ a graph representation for software source code that mixes elements of control flow and program dependence graphs with abstract syntax trees. Using data sets from SV-COMP, we demonstrate our rank prediction technique to generalize well and achieve a rather high predictive accuracy. In particular, our method outperforms a recently proposed feature-based approach of Demyanova et al. (when applied to rank predictions).

PART_PW: From Partial Analysis Results to a Proof Witness - Jakobs, Marie-Christine (Software Engineering and Formal Methods)
Today, verification tools do not only output yes or no, but also provide correctness arguments or counterexamples. While counterexamples help to fix bugs, correctness arguments are used to increase the trust in program correctness, e.g., in Proof-Carrying Code (PCC). Correctness arguments are well-studied for single analyses, but not when a set of analyses together verifies a program, each of the analyses checking only a particular part. Such a set of partial, complementary analyses is often used when a single analysis would fail or is inefficient on some program parts.We propose PART_PW, a technique which allows us to automatically construct a proof witness (correctness argument) from the analysis results obtained by a set of partial, complementary analyses. The constructed proof witnesses are proven to be valid correctness arguments and in our experiments we use them seamlessly and efficiently in existing PCC approaches.

IDEal: Efficient and Precise Alias-aware Dataflow Analysis - Späth, Johannes; Ali, Karim; Bodden, Eric (2017 International Conference on Object-Oriented Programming, Languages and Applications (OOPSLA/SPLASH))
Keywords: ATTRACT; ITSECWEBSITE; CROSSING

Computation on Encrypted Data using Data Flow Authentication - Fischer, Andreas; Fuhry, Benny; Kerschbaum, Florian; Bodden, Eric (CoRR)

Proof-Carrying Hardware via Inductive Invariants - Isenberg, Tobias; Platzner, Marco; Wehrheim, Heike; Wiersema, Tobias (ACM Transactions on Design Automation of Electronic Systems)
Proof-carrying hardware (PCH) is a principle for achieving safety for dynamically reconfigurable hardware systems. The producer of a hardware module spends huge effort when creating a proof for a safety policy. The proof is then transferred as a certificate together with the configuration bitstream to the consumer of the hardware module, who can quickly verify the given proof. Previous work utilized SAT solvers and resolution traces to set up a PCH technology and corresponding tool flows. In this article, we present a novel technology for PCH based on inductive invariants. For sequential circuits, our approach is fundamentally stronger than the previous SAT-based one since we avoid the limitations of bounded unrolling. We contrast our technology to existing ones and show that it fits into previously proposed tool flows. We conduct experiments with four categories of benchmark circuits and report consumer and producer runtime and peak memory consumption, as well as the size of the certificates and the distribution of the workload between producer and consumer. Experiments clearly show that our new induction-based technology is superior for sequential circuits, whereas the previous SAT-based technology is the better choice for combinational circuits.

Programs from Proofs: A Framework for the Safe Execution of Untrusted Software - Jakobs, Marie-Christine; Wehrheim, Heike (ACM Transactions on Programming Languages and Systems)
Today, software is traded worldwide on global markets, with apps being downloaded to smartphones within minutes or seconds. This poses, more than ever, the challenge of ensuring safety of software in the face of (1) unknown or untrusted software providers together with (2) resource-limited software consumers. The concept of Proof-Carrying Code (PCC), years ago suggested by Necula, provides one framework for securing the execution of untrusted code. PCC techniques attach safety proofs, constructed by software producers, to code. Based on the assumption that checking proofs is usually much simpler than constructing proofs, software consumers should thus be able to quickly check the safety of software. However, PCC techniques often suffer from the size of certificates (i.e., the attached proofs), making PCC techniques inefficient in practice.In this article, we introduce a new framework for the safe execution of untrusted code called Programs from Proofs (PfP). The basic assumption underlying the PfP technique is the fact that the structure of programs significantly influences the complexity of checking a specific safety property. Instead of attaching proofs to program code, the PfP technique transforms the program into an efficiently checkable form, thus guaranteeing quick safety checks for software consumers. For this transformation, the technique also uses a producer-side automatic proof of safety. More specifically, safety proving for the software producer proceeds via the construction of an abstract reachability graph (ARG) unfolding the control-flow automaton (CFA) up to the degree necessary for simple checking. To this end, we combine different sorts of software analysis: expensive analyses incrementally determining the degree of unfolding, and cheap analyses responsible for safety checking. Out of the abstract reachability graph we generate the new program. In its CFA structure, it is isomorphic to the graph and hence another, this time consumer-side, cheap analysis can quickly determine its safety.Like PCC, Programs from Proofs is a general framework instantiable with different sorts of (expensive and cheap) analysis. Here, we present the general framework and exemplify it by some concrete examples. We have implemented different instantiations on top of the configurable program analysis tool CPAchecker and report on experiments, in particular on comparisons with PCC techniques.

Just test what you cannot verify! - Czech, Mike; Jakobs, Marie-Christine; Wehrheim, Heike (Software Engineering 2016)
Software verification is an established method to ensure software safety. Nevertheless, verification still often fails, either because it consumes too much resources, e.g., time or memory, or the technique is not mature enough to verify the property. Often then discarding the partial verification, the validation process proceeds with techniques like testing.To enable standard testing to profit from previous, partial verification, we use a summary of the verification effort to simplify the program for subsequent testing. Our techniques use this summary to construct a residual program which only contains program paths with unproven assertions. Afterwards, the residual program can be used with standard testing tools.Our first experiments show that testing profits from the partial verification.The test effort is reduced and combined verification and testing is faster than a complete verification.

An Architecture and Design Tool Flow for Embedding a Virtual FPGA into a Reconfigurable System-on-Chip - Wiersema, Tobias; Bockhorn, Arne; Platzner, Marco (Computers & Electrical Engineering)
Virtual field programmable gate arrays (FPGA) are overlay architectures realized on top of physical FPGAs. They are proposed to enhance or abstract away from the physical FPGA for experimenting with novel architectures and design tool flows. In this paper, we present an embedding of a ZUMA-based virtual FPGA fabric into a complete configurable system-on-chip. Such an embedding is required to fully harness the potential of virtual FPGAs, in particular to give the virtual circuits access to main memory and operating system services, and to enable a concurrent operation of virtualized and non-virtualized circuitry. We discuss our extension to ZUMA and its embedding into the ReconOS operating system for hardware/software systems. Furthermore, we present an open source tool flow to synthesize configurations for the virtual FPGA, along with an analysis of the area and delay overheads involved.

A CEGAR Scheme for Information Flow Analysis - Töws, Manuel; Wehrheim, Heike (Proceedings of the 18th International Conference on Formal Engineering Methods (ICFEM 2016))
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.

Boomerang: Demand-Driven Flow- and Context-Sensitive Pointer Analysis for Java - Späth, Johannes; Nguyen Quang Do, Lisa; Ali, Karim; Bodden, Eric (European Conference on Object-Oriented Programming (ECOOP))
Keywords: ATTRACT; ITSECWEBSITE

PAndA 2 : Analyzing Permission Use and Interplay in Android Apps (Tool Paper) - Jakobs, Marie-Christine; Töws, Manuel; Pauck, Felix (Workshop on Formal and Model-Driven Techniques for Developing Trustworthy Systems)
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.

Verifying Worst-Case Completion Times for Reconfigurable Hardware Modules using Proof-Carrying Hardware - Wiersema, Tobias; Platzner, Marco (Proceedings of the 11th International Symposium on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC 2016))
Runtime reconfiguration can be used to replace hardware modules in the field and even to continuously improve them during operation. Runtime reconfiguration poses new challenges for validation, since the required properties of newly arriving modules may be difficult to check fast enough to sustain the intended system dynamics. In this paper we present a method for just-in-time verification of the worst-case completion time of a reconfigurable hardware module. We assume so-called run-to-completion modules that exhibit start and done signals indicating the start and end of execution, respectively. We present a formal verification approach that exploits the concept of proof-carrying hardware. The approach tasks the creator of a hardware module with constructing a proof of the worst-case completion time, which can then easily be checked by the user of the module, just prior to reconfiguration. After explaining the verification approach and a corresponding tool flow, we present results from two case studies, a short term synthesis filter and a multihead weigher. The resultsclearly show that cost of verifying the completion time of the module is paid by the creator instead of the user of the module.

Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning - Jakobs, Marie-Christine (Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM))
Before execution, users should formally validate the correctness of software received from untrusted providers. To accelerate this validation, in the proof carrying code (PCC) paradigm the provider delivers the software together with a certificate, a formal proof of the software’s correctness. Thus, the user only checks if the attached certificate shows correctness of the delivered software.Recently, we introduced configurable program certification, a generic, PCC based framework supporting various software analyses and safety properties. Evaluation of our framework revealed that validation suffers from certificate reading. In this paper, we present two orthogonal approaches which improve certificate validation, both reducing the impact of certificate reading. The first approach reduces the certificate size, storing information only if it cannot easily be recomputed. The second approach partitions the certificate into independently checkable parts. The trick is to read parts of the certificate while already checking read parts. Our experiments show that validation highly benefits from our improvements.

Just test what you cannot verify! - Czech, Mike; Jakobs, Marie-Christine; Wehrheim, Heike (Fundamental Approaches to Software Engineering)
Today, software verification is an established analysis method which can provide high guarantees for software safety. However, the resources (time and/or memory) for an exhaustive verification are not always available, and analysis then has to resort to other techniques, like testing. Most often, the already achieved partial verification results arediscarded in this case, and testing has to start from scratch.In this paper, we propose a method for combining verification and testing in which testing only needs to check the residual fraction of an uncompleted verification. To this end, the partial results of a verification run are used to construct a residual program (and residual assertions to be checked on it). The residual program can afterwards be fed into standardtesting tools. The proposed technique is sound modulo the soundness of the testing procedure. Experimental results show that this combinedusage of verification and testing can significantly reduce the effort for the subsequent testing.

Incremental Inductive Verification of Parameterized Timed Systems - Isenberg, Tobias (Proceedings of the 15th International Conference on Application of Concurrency to System Design (ACSD))
We propose an incremental workflow for the verification of parameterized systems modeled as symmetric networks of timed automata. Starting with a small number of timed automata in the network, a safety property is verified using IC3, a state-of-the-art algorithm based on induction.The result of the verification, an inductive strengthening, is reused proposing a candidate inductive strengthening for a larger network.If the candidate is valid, our main theorem states that the safety property holds for all sizes of the network of timed automata. Otherwise the number of automata is increased and the next iteration is started with a new run of IC3.We propose and thoroughly examine optimizations to our workflow, e.g. Feedback mechanisms to speed up the run of IC3.

Programs from Proofs of Predicated Dataflow Analyses - Jakobs, Marie-Christine; Wehrheim, Heike (Proceedings of the 30th Annual ACM Symposium on Applied Computing)
Programs from Proofs" is a generic method which generates new programs out of correctness proofs of given programs. The technique ensures that the new and given program are behaviorally equivalent and that the new program is easily verifiable, thus serving as an alternative to proof-carrying code concepts. So far, this generic method has one instantiation that verifies type-state properties of programs. In this paper, we present a whole range of new instantiations, all based on data ow analyses. More precisely, we show how an imprecise but fast data ow analysis can be enhanced with a predicate analysis as to yield a precise but expensive analysis. Out of the safety proofs of this analysis, we generate new programs, again behaviorally equivalent to the given ones, which are easily verifiable" in the sense that now the data ow analysis alone can yield precise results. An experimental evaluation practically supports our claim of easy verification.

On-The-Fly Verification of Reconfigurable Image Processing Modules based on a Proof-Carrying Hardware Approach - Wiersema, Tobias; Wu, Sen; Platzner, Marco (Proceedings of the International Symposium in Reconfigurable Computing (ARC))
Proof-carrying hardware is an approach that has recently been proposed for the efficient verification of reconfigurable modules. We present an application of proof-carrying hardware to guarantee the correct functionality of dynamically reconfigured image processing modules. Our prototype comprises a reconfigurable-system-on-chip with an embedded virtual FPGA fabric. This setup allows us to leverage open source FPGA synthesis and backend tools to produce FPGA configuration bitstreams with an open format and, thus, to demonstrate and experimentally evaluate proof-carrying hardware at the bitstream level.

IccTA: Detecting Inter-Component Privacy Leaks in Android Apps - Li, Li; Bartel, Alexandre; Bissyande, Tegawende F.; Klein, Jacques; Le Traon, Yves; Arzt, Steven; Rasthofer, Siegfried; Bodden, Eric; Octeau, Damien; McDaniel, Patrick (2015 International Conference on Software Engineering (ICSE))
Keywords: CROSSING; ATTRACT; ITSECWEBSITE

Programs from Proofs -- Approach and Applications - Wonisch, Daniel; Schremmer, Alexander; Wehrheim, Heike (Proceedings of the Software Engineering Conference (SE))
Proof-carrying code approaches aim at safe execution of untrusted code by having the code producer attach a safety proof to the code which the code consumer only has to validate. Depending on the type of safety property, proofs can however become quite large and their validation - though faster than their construction - still time consuming. In this paper we introduce a new concept for safe execution of untrusted code. It keeps the idea of putting the time consuming part of proving on the side of the code producer, however, attaches no proofs to code anymore but instead uses the proof to transform the program into an equivalent but more eﬃciently veriﬁable program. Code consumers thus still do proving themselves, however, on a computationally inexpensive level only. Experimental results show that the proof eﬀort can be reduced by several orders of magnitude, both with respect to time and space.

Certification for Configurable Program Analysis - Jakobs, Marie-Christine; Wehrheim, Heike (Proceedings of the 21st International Symposium on Model Checking of Software (SPIN))
Configurable program analysis (CPA) is a generic concept for the formalization of different software analysis techniques in a single framework. With the tool CPAchecker, this framework allows for an easy configuration and subsequent automatic execution of analysis procedures ranging from data-flow analysis to model checking. The focus of the tool CPAchecker is thus on analysis. In this paper, we study configurability from the point of view of software certification. Certification aims at providing (via a prior analysis) a certificate of correctness for a program which is (a) tamper-proof and (b) more efficient to check for validity than a full analysis. Here, we will show how, given an analysis instance of a CPA, to construct a corresponding sound certification instance, thereby arriving at configurable program certification. We report on experiments with certification based on different analysis techniques, and in particular explain which characteristics of an underlying analysis allow us to design an efficient (in the above (b) sense) certification procedure.

Memory Security in Reconfigurable Computers: Combining Formal Verification with Monitoring - Wiersema, Tobias; Drzevitzky, Stephanie; Platzner, Marco (Proceedings of the International Conference on Field-Programmable Technology (FPT))
Ensuring memory access security is a challenge for reconfigurable systems with multiple cores. Previous work introduced access monitors attached to the memory subsystem to ensure that the cores adhere to pre-defined protocols when accessing memory. In this paper, we combine access monitors with a formal runtime verification technique known as proof-carrying hardware to guarantee memory security. We extend previous work on proof-carrying hardware by covering sequential circuits and demonstrate our approach with a prototype leveraging ReconOS/Zynq with an embedded ZUMA virtual FPGA overlay. Experiments show the feasibility of the approach and the capabilities of the prototype, which constitutes the first realization of proof-carrying hardware on real FPGAs. The area overheads for the virtual FPGA are measured as 2x-10x, depending on the resource type. The delay overhead is substantial with almost 100x, but this is an extremely pessimistic estimate that will be lowered once accurate timing analysis for FPGA overlays become available. Finally, reconfiguration time for the virtual FPGA is about one order of magnitude lower than for the native Zynq fabric.

Integrating Software and Hardware Verification - Jakobs, Marie-Christine; Platzner, Marco; Wiersema, Tobias; Wehrheim, Heike (Proceedings of the 11th International Conference on Integrated Formal Methods (iFM))
Verification of hardware and software usually proceeds separately, software analysis relying on the correctness of processors executing instructions. This assumption is valid as long as the software runs on standard CPUs that have been extensively validated and are in wide use. However, for processors exploiting custom instruction set extensions to meet performance and energy constraints the validation might be less extensive, challenging the correctness assumption.In this paper we present an approach for integrating software analyses with hardware verification, specifically targeting custom instruction set extensions. We propose three different techniques for deriving the properties to be proven for the hardware implementation of a custom instruction in order to support software analyses. The techniques are designed to explore the trade-off between generality and efficiency and span from proving functional equivalence over checking the rules of a particular analysis domain to verifying actual pre and post conditions resulting from program analysis. We demonstrate and compare the three techniques on example programs with custom instructions, using stateof-the-art software and hardware verification techniques.

Embedding FPGA Overlays into Configurable Systems-on-Chip: ReconOS meets ZUMA - Wiersema, Tobias; Bockhorn, Arne; Platzner, Marco (Proceedings of the International Conference on ReConFigurable Computing and FPGAs (ReConFig))
Virtual FPGAs are overlay architectures realized on top of physical FPGAs. They are proposed to enhance or abstract away from the physical FPGA for experimenting with novel architectures and design tool flows. In this paper, we present an embedding of a ZUMA-based virtual FPGA fabric into a complete configurable system-on-chip. Such an embedding is required to fully harness the potential of virtual FPGAs, in particular to give the virtual circuits access to main memory and operating system services, and to enable a concurrent operation of virtualized and non-virtualized circuitry. We discuss our extension to ZUMA and its embedding into the ReconOS operating system for hardware/software systems. Furthermore, we present an open source tool flow to synthesize configurations for the virtual FPGA.

FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps - Arzt, Steven; Rasthofer, Siegfried; Fritz, Christian; Bodden, Eric; Bartel, Alexandre; Klein, Jacques; Le Traon, Yves; Octeau, Damien; McDaniel, Patrick (Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation - PLDI '14)

DroidForce: Enforcing Complex, Data-Centric, System-Wide Policies in Android - Arzt, Steven; Rasthofer, Siegfried; Lovat, Enrico; Bodden, Eric (International Conference on Availability, Reliability and Security (ARES 2014))

Zero Overhead Runtime Monitoring - Wonisch, Daniel; Schremmer, Alexander; Wehrheim, Heike (Proceedings of the 11th International Conference on Software Engineering and Formal Methods (SEFM))
Runtime monitoring aims at ensuring program safety by monitoring the program's behaviour during execution and taking appropriate action before a program violates some property.Runtime monitoring is in particular important when an exhaustive formal verification fails. While the approach allows for a safe execution of programs, it may impose a significant runtime overhead.In this paper, we propose a novel technique combining verification and monitoring which incurs no overhead during runtime at all. The technique proceeds by using the inconclusive result of a verification run as the basis for transforming the program into one where all potential points of failure are replaced by HALT statements. The new program is safe by construction, behaviourally equivalent to the original program (except for unsafe behaviour),and has the same performance characteristics.

Programs from Proofs – A PCC Alternative - Wonisch, Daniel; Schremmer, Alexander; Wehrheim, Heike (Proceedings of the 25th International Conference on Computer Aided Verification (CAV))
Proof-carrying code approaches aim at safe execution of untrusted code by having the code producer attach a safety proof to the code which the code consumer only has to validate. Depending on the type of safety property, proofs can however become quite large and their validation - though faster than their construction - still time consuming. In this paper we introduce a new concept for safe execution of untrusted code. It keeps the idea of putting the time consuming part of proving on the side of the code producer, however, attaches no proofs to code anymore but instead uses the proof to transform the program into an equivalent but more eﬃciently veriﬁable program. Code consumers thus still do proving themselves, however, on a computationally inexpensive level only. Experimental results show that the proof eﬀort can be reduced by several orders of magnitude, both with respect to time and space.

Predicate Analysis with Block-Abstraction Memoization - Wonisch, Daniel; Wehrheim, Heike (Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM))
Predicate abstraction is an established technique for reducing the size of the state space during verification. In this paper, we extend predication abstraction with block-abstraction memoization (BAM), which exploits the fact that blocks are often executed several times in a program. The verification can thus benefit from caching the values of previous block analyses and reusing them upon next entry into a block. In addition to function bodies, BAM also performs well for nested loops. To further increase effectiveness, block memoization has been integrated with lazy abstraction adopting a lazy strategy for cache refinement. Together, this achieves significant performance increases: our tool (an implementation within the configurable program analysis framework CPAchecker) has won the Competition on Software Verification 2012 in the category “Overall”.

Heuristic-Guided Abstraction Refinement for Concurrent Systems - Timm, Nils; Wehrheim, Heike; Czech, Mike (Proceedings of the 14th International Conference on Formal Engineering Methods (ICFEM))
Predicate abstraction is an established technique in software verification. It inherently includes an abstraction refinement loop successively adding predicates until the right level of abstraction is found. For concurrent systems, predicate abstraction can be combined with spotlight abstraction, further reducing the state space by abstracting away certain processes. Refinement then has to decide whether to add a new predicate or a new process. Selecting the right predicates and processes is a crucial task: The positive effect of abstraction may be compromised by unfavourable refinement decisions. Here we present a heuristic approach to abstraction refinement. The basis for a decision is a set of refinement candidates, derived by multiple counterexample-generation. Candidates are evaluated with respect to their influence on other components in the system. Experimental results show that our technique can significantly speed up verification as compared to a naive abstraction refinement.

Block Abstraction Memoization for CPAchecker - Wonisch, Daniel (Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS))
Block Abstraction Memoization (ABM) is a technique in software model checking that exploits the modularity of programs during verification by caching. To this end, ABM records the results of block analyses and reuses them if possible when revisiting the same block again. In this paper we present an implementation of ABM into the predicate-analysis component of the software-verification framework CPAchecker. With our participation at the Competition on Software Verification we aim at providing evidence that ABM can not only substantially increase the efficiency of predicate analysis but also enables verification of a wider range of programs.

Partially Evaluating Finite-State Runtime Monitors Ahead of Time - Bodden, Eric; Lam, Patrick; Hendren, Laurie (ACM Transactions on Programming Languages and Systems)

Selected papers on Integrated Formal Methods (iFM09) - Leuschel, Michael; Wehrheim, Heike (Science of Computer Programming)

Achieving Hardware Security for Reconﬁgurable Systems on Chip by a Proof-Carrying Code Approach - Drzevitzky, Stephanie; Platzner, Marco (Proceedings of the 6th International Workshop on Reconfigurable Communication-centric Systems-on-Chip (ReCoSoC))
Reconﬁgurable systems on chip are increasingly deployed in security and safety critical contexts. When downloading and conﬁguring new hardware functions, we want to make sure that modules adhere to certain security speciﬁcations and do not, for example, contain hardware Trojans. As a possible approach to achieving hardware security we propose and demonstrate the concept of proof-carrying hardware, a concept inspired by previous work on proof-carrying code techniques in the software domain. In this paper, we discuss the hardware trust and threat models behind proof-carrying hardware and then present our experimental setup. We detail the employed open-source tool chain for the runtime veriﬁcation of combinational equivalence and our bitstream format for an abstract FPGA architecture that allows us to experimentally validate the feasibility of our approach.