@phdthesis{29769, abstract = {{Wettstreit zwischen der Entwicklung neuer Hardwaretrojaner und entsprechender Gegenmaßnahmen beschreiten Widersacher immer raffiniertere Wege um Schaltungsentwürfe zu infizieren und dabei selbst fortgeschrittene Test- und Verifikationsmethoden zu überlisten. Abgesehen von den konventionellen Methoden um einen Trojaner in eine Schaltung für ein Field-programmable Gate Array (FPGA) einzuschleusen, können auch die Entwurfswerkzeuge heimlich kompromittiert werden um einen Angreifer dabei zu unterstützen einen erfolgreichen Angriff durchzuführen, der zum Beispiel Fehlfunktionen oder ungewollte Informationsabflüsse bewirken kann. Diese Dissertation beschäftigt sich hauptsächlich mit den beiden Blickwinkeln auf Hardwaretrojaner in rekonfigurierbaren Systemen, einerseits der Perspektive des Verteidigers mit einer Methode zur Erkennung von Trojanern auf der Bitstromebene, und andererseits derjenigen des Angreifers mit einer neuartigen Angriffsmethode für FPGA Trojaner. Für die Verteidigung gegen den Trojaner ``Heimtückische LUT'' stellen wir die allererste erfolgreiche Gegenmaßnahme vor, die durch Verifikation mittels Proof-carrying Hardware (PCH) auf der Bitstromebene direkt vor der Konfiguration der Hardware angewendet werden kann, und präsentieren ein vollständiges Schema für den Entwurf und die Verifikation von Schaltungen für iCE40 FPGAs. Für die Gegenseite führen wir einen neuen Angriff ein, welcher bösartiges Routing im eingefügten Trojaner ausnutzt um selbst im fertigen Bitstrom in einem inaktiven Zustand zu verbleiben: Hierdurch kann dieser neuartige Angriff zur Zeit weder von herkömmlichen Test- und Verifikationsmethoden, noch von unserer vorher vorgestellten Verifikation auf der Bitstromebene entdeckt werden.}}, author = {{Ahmed, Qazi Arbab}}, keywords = {{FPGA Security, Hardware Trojans, Bitstream-level Trojans, Bitstream Verification}}, publisher = {{ Paderborn University, Paderborn, Germany}}, title = {{{Hardware Trojans in Reconfigurable Computing}}}, doi = {{10.17619/UNIPB/1-1271}}, year = {{2022}}, } @phdthesis{26746, abstract = {{Previous research in proof-carrying hardware has established the feasibility and utility of the approach, and provided a concrete solution for employing it for the certification of functional equivalence checking against a specification, but fell short in connecting it to state-of-the-art formal verification insights, methods and tools. Due to the immense complexity of modern circuits, and verification challenges such as the state explosion problem for sequential circuits, this restriction of readily-available verification solutions severely limited the applicability of the approach in wider contexts. This thesis closes the gap between the PCH approach and current advances in formal hardware verification, provides methods and tools to express and certify a wide range of circuit properties, both functional and non-functional, and presents for the first time prototypes in which circuits that are implemented on actual reconfigurable hardware are verified with PCH methods. Using these results, designers can now apply PCH to establish trust in more complex circuits, by using more diverse properties which they can express using modern, efficient property specification techniques.}}, author = {{Wiersema, Tobias}}, keywords = {{Proof-Carrying Hardware, Formal Verification, Sequential Circuits, Non-Functional Properties, Functional Properties}}, pages = {{293}}, publisher = {{Paderborn University}}, title = {{{Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware}}}, year = {{2021}}, } @article{27841, abstract = {{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.}}, author = {{Jakobs, Marie-Christine and Pauck, Felix and Platzner, Marco and Wehrheim, Heike and Wiersema, Tobias}}, journal = {{IEEE Access}}, keywords = {{Software Analysis, Abstract Interpretation, Custom Instruction, Hardware Verification}}, publisher = {{IEEE}}, title = {{{Software/Hardware Co-Verification for Custom Instruction Set Processors}}}, doi = {{10.1109/ACCESS.2021.3131213}}, year = {{2021}}, } @article{17358, abstract = {{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.}}, author = {{Witschen, Linus Matthias and Wiersema, Tobias and Platzner, Marco}}, issn = {{1557-9999}}, journal = {{IEEE Transactions On Very Large Scale Integration Systems}}, keywords = {{Approximate circuit synthesis, approximate computing, error metrics, formal verification, proof-carrying hardware}}, number = {{9}}, pages = {{2084 -- 2088}}, publisher = {{IEEE}}, title = {{{Proof-carrying Approximate Circuits}}}, doi = {{10.1109/TVLSI.2020.3008061}}, volume = {{28}}, year = {{2020}}, } @unpublished{16853, abstract = {{State-of-the-art frameworks for generating approximate circuits usually rely on information gained through circuit synthesis and/or verification to explore the search space and to find an optimal solution. Throughout the process, a large number of circuits may be subject to processing, leading to considerable runtimes. In this work, we propose a search which takes error bounds and pre-computed impact factors into account to reduce the number of invoked synthesis and verification processes. In our experimental results, we achieved speed-ups of up to 76x while area savings remain comparable to the reference search method, simulated annealing.}}, author = {{Witschen, Linus Matthias and Ghasemzadeh Mohammadi, Hassan and Artmann, Matthias and Platzner, Marco}}, booktitle = {{Fourth Workshop on Approximate Computing (AxC 2019)}}, keywords = {{Approximate computing, parameter selection, search space exploration, verification, circuit synthesis}}, pages = {{2}}, title = {{{Jump Search: A Fast Technique for the Synthesis of Approximate Circuits}}}, year = {{2019}}, } @misc{1097, author = {{Jentzsch, Felix Paul}}, keywords = {{Approximate Computing, Proof-Carrying Hardware, Formal Verification}}, publisher = {{Universität Paderborn}}, title = {{{Enforcing IP Core Connection Properties with Verifiable Security Monitors}}}, year = {{2018}}, } @inproceedings{36917, abstract = {{The ever-increasing complexity of heterogeneous electronic systems demand for intensified abstraction and automation efforts to improve design, verification and validation productivity, especially in earlier phases of system engineering. Within the verification activity various metrics can be applied to determine functional correctness or the overall progress. Here, a supporting verification methodology defining high-level verification planning down to the actual metric code development is essential. Moreover, an advanced assistance for the designer, such as a tooling infrastructure to automatize and accelerate the metric code implementation, is needed to minimize the influence of errorprone manual coding. In this article we present a single-source verification metric code-generation methodology for improved coverage automation. We determine (i) a suitable metric model for model-based capture of verification metrics as well as (ii) an assisted model-based processing and generation flow of the verification environment and metric skeletons. We apply our method to a SystemC case-study, in doing so, targeting metric code implementation productivity and consistency enhancement.}}, author = {{Kuznik, Christoph and Müller, Wolfgang and Defo, Gilles Bertrand}}, keywords = {{System Design, Verification}}, title = {{{An Assisted Single Source Verification Metric Model Code Generation Methodology}}}, year = {{2014}}, } @inproceedings{34585, abstract = {{In this paper, we present an efficient approach to virtual platform modeling for TriCore-based SoCs by combining fast and open software emulation with IEEE-1666 Standard SystemC simulation. For evaluation we consider Infineon's recently introduced AURIX processor family as a target platform, which utilizes multiple CPU cores operating in lockstep mode, memories, hierarchical buses, and a rich set of peripherals. For SoC prototyping, we integrate the fast and open instruction accurate QEMU software emulator with the TLMu library for SystemC co-verification. This article reports our most recent efforts of the implementation of the TriCore instruction set for QEMU. The experimental results demonstrate the functional correctness and performance of our TriCore implementation.}}, author = {{Koppelmann, Bastian and Messidat, Bernd and Becker, Markus and Müller, Wolfgang and Scheytt, J. Christoph}}, booktitle = {{Proceedings of the Design and Verification Conference Europe (DVCON Europe)}}, keywords = {{System Design, Verification}}, title = {{{Fast and Open Virtual Platforms for TriCore-based SoCs Using QEMU}}}, year = {{2014}}, } @inproceedings{2370, author = {{Woehrle, Matthias and Plessl, Christian and Lim, Roman and Beutel, Jan and Thiele, Lothar}}, booktitle = {{IEEE Int. Conf. on Sensor Networks, Ubiquitous, and Trustworthy Computing (SUTC)}}, isbn = {{978-0-7695-3158-8}}, keywords = {{WSN, testing, verification}}, pages = {{201--208}}, publisher = {{IEEE Computer Society}}, title = {{{EvAnT: Analysis and Checking of event traces for Wireless Sensor Networks}}}, doi = {{10.1109/SUTC.2008.24}}, year = {{2008}}, } @inproceedings{2393, author = {{Beutel, Jan and Dyer, Matthias and Lim, Roman and Plessl, Christian and Woehrle, Matthias and Yuecel, Mustafa and Thiele, Lothar}}, booktitle = {{Proc. Int. Conf. Networked Sensing Systems (INSS)}}, isbn = {{1-4244-1231-5}}, keywords = {{WSN, testing, verification}}, pages = {{303--303}}, publisher = {{IEEE}}, title = {{{Automated Wireless Sensor Network Testing}}}, doi = {{10.1109/INSS.2007.4297445}}, year = {{2007}}, } @inproceedings{39069, abstract = {{We present the syntax and semantics of a past- and future-oriented temporal extension of the Object Constraint Language (OCL). Our extension supports designers to express time-bounded properties over a state-oriented UML model of a system under development. The semantics is formally defined over the system states of a mathematical object model. Additionally, we present a mapping to Clocked Linear Temporal Logic (Clocked LTL) formulae, which is the basis for further application in verification with model checking. We demonstrate the applicability of the approach by the example of a buffer specification in the context of a production system.}}, author = {{Flake, Stephan and Müller, Wolfgang}}, booktitle = {{Proceedings of SEFM´04}}, isbn = {{0-7695-2222-X}}, keywords = {{Unified modeling language, Logic, Clocks, Boolean functions, Application software, Time factors, Real time systems, Formal verification, Buffer storage, Software packages}}, publisher = {{IEEE}}, title = {{{Past- and Future-Oriented Time-Bound Temporal Properties with OCL}}}, doi = {{10.1109/SEFM.2004.1347516}}, year = {{2004}}, } @inproceedings{39382, abstract = {{We present a rigorous but transparent semantics definition of the SpecC language that covers the execution of SpecC behaviors and their interaction with the kernel process. The semantics include wait, wait for, par, and try statements as they are introduced in SpecC. We present our definition in form of distributed abstract state machine (ASM) rules strictly following the lines of the SpecC Language Reference Manual. We mainly see our formal semantics in three application areas. First, it is a concise, unambiguous description for documentation and standardization. Second, it applies as a high-level, pseudo code-oriented specification for the implementation of a SpecC simulator. Finally, it is a first step for SpecC synthesis in order to identify similar concepts with other languages like VHDL and SystemC for the definition of common patterns and language subsets.}}, author = {{Müller, Wolfgang and Dömer, Rainer and Gerstlauer, Andreas}}, booktitle = {{Proceedings of the ISSS02}}, isbn = {{1-58113-576-9}}, keywords = {{Standardization, Kernel, Permission, Formal verification, Logic functions, Documentation, Reasoning about programs, Specification languages, Formal specifications, Software systems}}, title = {{{The Formal Execution Semantics of SpecC}}}, doi = {{10.1145/581199.581234 }}, year = {{2002}}, } @inproceedings{39403, abstract = {{The Unified Modeling Language (UML) has received wide acceptance as a standard language in the field of software specification by means of different diagram types. In a recent version of UML, the textual Object Constraint Language (OCL) was introduced to support specification of constraints for UML models. But OCL currently does not provide sufficient means to specify constraints over the dynamic behavior of a model. This article presents an OCL extension that is consistent with current OCL and enables modelers to specify state-related time-bounded constraints. We consider the case study of a flexible manufacturing system and identify typical real-time constraints. The constraints are presented in our temporal OCL extension as well as in temporal logic formulae. For general application, we define a semantics of our OCL extension by means of a time-bounded temporal logic based on Computational Tree Logic (CTL).}}, author = {{Flake, Stephan and Müller, Wolfgang}}, booktitle = {{Proceedings of HICSS-35}}, isbn = {{0-7695-1435-9}}, keywords = {{Unified modeling language, Logic, Formal verification, Real time systems, Programming profession, Vehicle dynamics, Software standards, Flexible manufacturing systems, Electronics industry, Protocols}}, location = {{Big Island, HI, USA }}, title = {{{Specification of Real-Time Properties for UML Models}}}, doi = {{10.1109/HICSS.2002.994469}}, year = {{2002}}, } @inproceedings{39421, abstract = {{We present a rigorous but transparent semantics definition of SystemC that covers method, thread, and clocked thread behavior as well as their interaction with the simulation kernel process. The semantics includes watching statements, signal assignment, and wait statements as they are introduced in SystemC V1.O. We present our definition in form of distributed Abstract State Machines (ASMs) rules reflecting the view given in the SystemC User's Manual and the reference implementation. We mainly see our formal semantics as a concise, unambiguous, high-level specification for SystemC-based implementations and for standardization. Additionally, it can be used as a sound basis to investigate SystemC interoperability with Verilog and VHDL.}}, author = {{Müller, Wolfgang and Ruf, Jürgen and Hoffmann, D. W. and Gerlach, Joachim and Kropf, Thomas and Rosenstiehl, W.}}, booktitle = {{Proceedings of the Design, Automation, and Test in Europe (DATE’01)}}, isbn = {{0-7695-0993-2}}, keywords = {{Yarn, Formal verification, Kernel, Hardware design languages, Electronic design automation and methodology, Algebra, Computational modeling, Logic functions, Computer languages, Clocks}}, publisher = {{IEEE}}, title = {{{The Simulation Semantics of SystemC}}}, doi = {{10.1109/DATE.2001.915002}}, year = {{2001}}, } @inbook{34448, abstract = {{We present a rigorous but transparent semantic definition for VHDL corresponding to the IEEE VHDL’ 93 standard [68, 9, 84]. Our definition covers the full behavior of signal and variable assignments as well as the behavior of the various wait statements including delta, time, and postponed cycles. We consider explicitly declared signals, ports, local variables, and shared variables. Our specification defines an abstract VHDL ’ 93 interpreter in the form of transition rules for an evolving algebra machine (EA-Machine) [60]. It faithfully reflects and supports the view of simulation given in the IEEE VHDL ’ 93 standard language reference manual. The definition can be understood without any prior formal training. We illustrate our definition by running the example VHDL program set out in the Introduction to this volume.}}, author = {{Börger, Egon and Glässer, Uwe and Müller, Wolfgang}}, booktitle = {{Semantics of VHDL}}, editor = {{Delgado Kloos, C. and Breuer, Peter T.}}, isbn = {{978-1-4615-2237-9}}, keywords = {{Transition Rule Formal Verification Variable Assignment Kernel Process Simulation Cycle}}, pages = {{107 -- 139}}, publisher = {{Kluwer Academic Publishers}}, title = {{{A Formal Definition of an Abstract VHDL'93 Simulator by EA-Machines}}}, doi = {{10.1007/978-1-4615-2237-9_5}}, year = {{1995}}, }