TY - THES AU - Pauck, Felix ID - 43108 TI - Cooperative Android App Analysis ER - TY - THES AU - Witschen, Linus Matthias ID - 34041 TI - Frameworks and Methodologies for Search-based Approximate Logic Synthesis ER - TY - THES AB - 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. AU - Wiersema, Tobias ID - 26746 KW - Proof-Carrying Hardware KW - Formal Verification KW - Sequential Circuits KW - Non-Functional Properties KW - Functional Properties TI - Guaranteeing Properties of Reconfigurable Hardware Circuits with Proof-Carrying Hardware ER - TY - GEN AU - Schott, Stefan ID - 22304 TI - Android App Analysis Benchmark Case Generation ER - TY - GEN AU - Zhang, Shikun ID - 7623 TI - Combining Android Apps for Analysis Purposes ER - TY - GEN AU - Selbach, Nils ID - 7628 TI - Modeling Crypto API usages in OpenSSL's EVP library ER - TY - GEN AB - Secure hardware design is the most important aspect to be considered in addition to functional correctness. Achieving hardware security in today’s globalized Integrated Cir- cuit(IC) supply chain is a challenging task. One solution that is widely considered to help achieve secure hardware designs is Information Flow Tracking(IFT). It provides an ap- proach to verify that the systems adhere to security properties either by static verification during design phase or dynamic checking during runtime. Proof-Carrying Hardware(PCH) is an approach to verify a functional design prior to using it in hardware. It is a two-party verification approach, where the target party, the consumer requests new functionalities with pre-defined properties to the producer. In response, the producer designs the IP (Intellectual Property) cores with the requested functionalities that adhere to the consumer-defined properties. The producer provides the IP cores and a proof certificate combined into a proof-carrying bitstream to the consumer to verify it. If the verification is successful, the consumer can use the IP cores in his hardware. In essence, the consumer can only run verified IP cores. Correctly applied, PCH techniques can help consumers to defend against many unintentional modifications and malicious alterations of the modules they receive. There are numerous published examples of how to use PCH to detect any change in the functionality of a circuit, i.e., pairing a PCH approach with functional equivalence checking for combinational or sequential circuits. For non-functional properties, since opening new covert channels to leak secret information from secure circuits is a viable attack vector for hardware trojans, i.e., intentionally added malicious circuitry, IFT technique is employed to make sure that secret/untrusted information never reaches any unclassified/trusted outputs. This master thesis aims to explore the possibility of adapting Information Flow Tracking into a Proof-Carrying Hardware scenario. It aims to create a method that combines Infor- mation Flow Tracking(IFT) with a PCH approach at bitstream level enabling consumers to validate the trustworthiness of a module’s information flow without the computational costs of a complete flow analysis. AU - Keerthipati, Monica ID - 15920 TI - A Bitstream-Level Proof-Carrying Hardware Technique for Information Flow Tracking ER - TY - THES AB - Traditional cache design uses a consolidated block of memory address bits to index a cache set, equivalent to the use of modulo functions. While this module-based mapping scheme is widely used in contemporary cache structures due to the simplicity of its hardware design and its good performance for sequences of consecutive addresses, its use may not be satisfactory for a variety of application domains having different characteristics.This thesis presents a new type of cache mapping scheme, motivated by programmable capabilities combined with Nature-inspired optimization of reconfigurable hardware. This research has focussed on an FPGA-based evolvable cache structure of the first level cache in a multi-core processor architecture, able to dynamically change cache indexing. To solve the challenge of reconfigurable cache mappings, a programmable Boolean circuit based on a combination of Look-up Table (LUT) memory elements is proposed. Focusing on optimization aspects at the system level, a Performance Measurement Infrastructure is introduced that is able to monitor the underlying microarchitectural metrics, and an adaptive evaluation strategy is presented that leverages on Evolutionary Algorithms, that is not only capable of evolving application-specific address-to-cache-index mappings for level one split caches but also of reducing optimization times. Putting this all together and prototyping in an FPGA for a LEON3/Linux-based multi-core processor, the creation of a system architecture reduces cache misses and improves performance over the use of conventional caches. AU - Ho, Nam ID - 3720 TI - FPGA-based Reconfigurable Cache Mapping Schemes: Design and Optimization ER - TY - GEN AU - Leer, Richard ID - 1044 TI - Measuring Performance of a Static Analysis Framework with an application to Immutability Analysis ER - TY - GEN AU - Strüwer, Jan Niclas ID - 1045 TI - Interactive Data Visualization for Exploded Supergraphs ER - TY - GEN AU - Jentzsch, Felix Paul ID - 1097 KW - Approximate Computing KW - Proof-Carrying Hardware KW - Formal Verification TI - Enforcing IP Core Connection Properties with Verifiable Security Monitors ER - TY - GEN AU - Hansmeier, Tim ID - 3580 TI - An FPGA Accelerator for Checking Resolution Proofs ER - TY - GEN AU - Witschen, Linus Matthias ID - 1157 TI - A Framework for the Synthesis of Approximate Circuits ER - TY - THES AU - Jakobs, Marie-Christine ID - 685 TI - On-The-Fly Safety Checking - Customizing Program Certification and Program Restructuring ER - TY - GEN AU - Pauck, Felix ID - 109 TI - Cooperative static analysis of Android applications ER - TY - GEN AU - Bröcher, Henrik ID - 201 TI - Evaluation von Graphpartitionierungsalgorithmen im Kontext von Konfigurierbarer Softwarezertifizierung ER - TY - THES AU - Isenberg, Tobias ID - 1190 TI - Induction-based Verification of Timed Systems ER - TY - GEN AU - Zhang, Guangli ID - 162 TI - Program Slicing: A Way of Separating WHILE Programs into Precise and Approximate Portions ER - TY - GEN AU - Meißner, Roland ID - 10714 TI - Konzept und Implementation einer Benutzeroberfläche zur Generierung virtueller FPGAs ER - TY - GEN AU - Wu, Sen ID - 331 TI - Webcam application using virtual FPGA ER -