Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Universal Composability is Secure Compilation
Get PDFUniversal composability is a framework for the specification and analysis of cryptographic protocols with a strong compositionality guarantee: UC protocols are secure even when composed with other protocols. Secure compilation tells whether compiled programs are as secure as their source-level counterparts, no matter what target-level code they interact with. These two disciplines are studied in isolation, but we believe there is a deeper connection between them with benefits from both worlds to reap. This paper outlines the connection between universal composability and robust compilation, the latest of secure compilation theories. We show how to read the universal composability theorem in terms of a robust compilation theorem and vice-versa. This, in turn, shows which elements of one theory corresponds to which element in the other theory. We believe this is the first step towards understanding how can secure compilation theories be used in universal composability settings and vice-versa
Revisiting the Relationship Between Fault Detection,Test Adequacy Criteria, and Test Set Size
Get PDFThe research community has long recognized a complex interrelationship between test set size, test adequacy criteria, and test effectiveness in terms of fault detection. However, there is substantial confusion about the role and importance of controlling for test set size when assessing and comparing test adequacy criteria. This paper makes the following contributions: (1) A review of contradictory analyses of the relationship between fault detection, test suite size, and test adequacy criteria. Specifically, this paper addresses the supposed contradiction of prior work and explains why test suite size is neither a confounding variable, as previously suggested,nor an independent variable that should be experimentally manipulated. (2) An explication and discussion of the experimental design and sampling strategies of prior work, together with a discussion of conceptual and statistical problems, and specific guidelines for future work. (3) A methodology for comparing test-adequacy criteria on an equal basis, which accounts for test suite size by treating it as a covariate. (4) An empirical evaluation that compares the effectiveness of coverage-based and mutation-based testing to one another and random testing. Additionally, this paper proposes probabilistic coupling, a methodology for approximating the representativeness of a set of test goals for a given set of real fault
The Hierarchy of Hyperlogics: A Knowledge Reasoning Perspective
No full textWe discuss the hierarchy of hyperlogics from a knowledge reasoning perspective. Hyperproperties generalize trace properties by relating multiple traces. Recently, logics for hyperproperties have been obtained from standard logics by adding variables for traces or paths to temporal logics like LTL and CTL*, and by adding the equal-level predicate to first-order and second-order logics, like monadic first-order logic of order and MSO. The resulting hierarchy of hyperlogics provides interesting opportunities for knowledge reasoning research: many epistemic properties and system properties in multi-agent systems, like distributivity, are hyperproperties. At the same time, first-order and second-order reasoning methods become applicable to hyperproperties
How to Win First-Order Safety Games
Get PDFFirst-order (FO) transition systems have recently attracted attention for the verification of parametric systems such as network protocols, software-defined networks or multi-agent workflows like conference management systems. Functional correctness or noninterference of these systems have conveniently been formulated as safety or hypersafety properties, respectively. In this article, we take the step from verification to synthesis---tackling the question whether it is possible to automatically synthesize predicates to enforce safety or hypersafety properties like noninterference. For that, we generalize FO transition systems to FO safety games. For FO games with monadic predicates only, we provide a complete classification into decidable and undecidable cases. For games with non-monadic predicates, we concentrate on universal first-order invariants, since these are sufficient to express a large class of properties---for example noninterference. We identify a non-trivial sub-class where invariants can be proven inductive and FO winning strategies be effectively constructed. We also show how the extraction of weakest FO winning strategies can be reduced to SO quantifier elimination itself. We demonstrate the usefulness of our approach by automatically synthesizing nontrivial FO specifications of messages in a leader election protocol as well as for paper assignment in a conference management system to exclude unappreciated disclosure of reports
BIAS: Bluetooth Impersonation AttackS
Get PDFBluetooth (BR/EDR) is a pervasive technology for wireless communication used by billions of devices. The Bluetooth standard includes a legacy authentication procedure and a secure authentication procedure, allowing devices to authenticate to each other using a long term key. Those procedures are used during pairing and secure connection establishment to prevent impersonation attacks. In this paper, we show that the Bluetooth specification contains vulnerabilities enabling to perform impersonation attacks during secure connection establishment. Such vulnerabilities include the lack of mandatory mutual authentication, overly permissive role switching, and an authentication procedure downgrade. We describe each vulnerability in detail, and we exploit them to design, implement, and evaluate master and slave impersonation attacks on both the legacy authentication procedure and the secure authentication procedure. We refer to our attacks as Bluetooth Impersonation AttackS (BIAS). Our attacks are standard compliant, and are therefore effective against any standard compliant Bluetooth device regardless the Bluetooth version, the security mode (e.g., Secure Connections), the device manufacturer, and the implementation details. Our attacks are stealthy because the Bluetooth standard does not require to notify end users about the outcome of an authentication procedure, or the lack of mutual authentication. To confirm that the BIAS attacks are practical, we successfully conduct them against 31 Bluetooth devices (28 unique Bluetooth chips) from major hardware and software vendors, implementing all the major Bluetooth versions, including Apple, Qualcomm, Intel, Cypress, Broadcom, Samsung, and CSR
CTRL-PACE: Controlled Randomness for e-Passport Password Authentication
No full textSecurity of many cryptographic protocols is conditioned by the quality of the random elements generated in the course of the protocol execution. On the other hand, cryptographic devices implementing these protocols are designed given technical limitations, usability requirements and cost constraints. This frequently results in a black box solution. Unfortunately, black box random number generators may enable creating backdoors for stealing signing keys, breaking authentication protocols and encrypted communication. In this paper we deal with this problem and extend our approach proposed during MYCRYPT’2016. The solution discussed is generating random parameters so that: (a) the protocols are backwards compatible (a user gets additional data that can be simply ignored), (b) verification of randomness might be executed any time without notice, so a device is forced to behave honestly, (c) the solution makes almost no intrusion in the existing protocols and is easy to implement, (d) the owner of a cryptographic device becomes secured against its designer and manufacturer that may even predict the output of the generator. In this paper we focus on a case when Diffie-Hellman protocol is executed for a generator that itself is a secret – this case has not been solved in our paper from MYCRYPT’2016. On the other hand, exactly this case occurs for the PACE protocol from the ICAO standard specifying electronic travel documents. For the sake of the proof we develop a framework of nested security games that aims to enable security proofs of modified protocols without redoing the proofs designed for their original versions
Comments on the “Draft Ethics Guidelines for Trustworthy AI” by the High-Level Expert Group on Artificial Intelligence.
Get PDFThe European Commission appointed the High-Level Expert Group on Artificial Intelligence (AI HLEG). The AI HLEG has the objective to support the implementation of the European strategy on Artificial Intelligence. This will include the elaboration of recommendations on future-related policy development and on ethical, legal and societal issues related to AI. In January 2019, the Commission asked stakeholders for comments on the AI HLEG’s “Draft Ethics Guidelines for Trustworthy AI”. CISPA submitted the following comments and remarks in the Stakeholders’ Consultation
The KNOB is Broken: Exploiting Low Entropy in the Encryption Key Negotiation Of Bluetooth BR/EDR
No full textWe present an attack on the encryption key negotiation protocol of Bluetooth BR/EDR. The attack allows a third party, without knowledge of any secret material (such as link and encryption keys), to make two (or more) victims agree on an encryption key with only 1 byte (8 bits) of entropy. Such low entropy enables the attacker to easily brute force the negotiated encryption keys, decrypt the eavesdropped ciphertext, and inject valid encrypted messages (in real-time). The attack is stealthy because the encryption key negotiation is transparent to the Bluetooth users. The attack is standard-compliant because all Bluetooth BR/EDR versions require to support encryption keys with entropy between 1 and 16 bytes and do not secure the key negotiation protocol. As a result, the attacker completely breaks Bluetooth BR/EDR security without being detected. We call our attack Key Negotiation Of Bluetooth (KNOB) attack.
The attack targets the firmware of the Bluetooth chip because the firmware (Bluetooth controller) implements all the security features of Bluetooth BR/EDR. As a standard-compliant attack, it is expected to be effective on any firmware that follows the specification and on any device using a vulnerable firmware. We describe how to perform the KNOB attack, and we implement it. We evaluate our implementation on more than 14 Bluetooth chips from popular manufacturers such as Intel, Broadcom, Apple, and Qualcomm. Our results demonstrate that all tested devices are vulnerable to the KNOB attack. We discuss countermeasures to fix the Bluetooth specification and its implementation
Efficient UC Commitment Extension with Homomorphism for Free (and Applications)
No full textHomomorphic universally composable (UC) commitments allow for the sender to reveal the result of additions and multiplications of values contained in commitments without revealing the values themselves while assuring the receiver of the correctness of such computation on committed values.
In this work, we construct essentially optimal additively homomorphic UC commitments from any (not necessarily UC or homomorphic) extractable commitment. We obtain amortized linear computational complexity in the length of the input messages and rate 1.
Next, we show how to extend our scheme to also obtain multiplicative homomorphism at the cost of asymptotic optimality but retaining low concrete complexity for practical parameters.
While the previously best constructions use UC oblivious transfer as the main building block, our constructions only require extractable commitments and PRGs, achieving better concrete efficiency and offering new insights into the sufficient conditions for obtaining homomorphic UC commitments.
Moreover, our techniques yield public coin protocols, which are compatible with the Fiat-Shamir heuristic.
These results come at the cost of realizing a restricted version of the homomorphic commitment functionality where the sender is allowed to perform any number of commitments and operations on committed messages but is only allowed to perform a single batch opening of a number of commitments.
Although this functionality seems restrictive, we show that it can be used as a building block for more efficient instantiations of recent protocols for secure multiparty computation and zero knowledge non-interactive arguments of knowledge
Summarizing Dynamic Graphs using MDL
Get PDFHow can we succinctly describe a large, dynamic graph over time? Given a large dynamic graph, can we �find "important" patterns that evolve over time, so that we can easily summarize and visualize the graph? In real life, these patterns signify interaction between nodes over time -- for example, how the network traffic of a bank changes during the day, how calling patterns change season over season, or how people watch different genre of movies over different times of the year. Our work focuses on the problem of how to find and rank these patterns. To this end, we formalize this problem as minimizing the encoding cost in a data compression paradigm and propose Mango, an effective heuristic for discovering evolving patterns in dynamic graphs. We then apply our method to both synthetic and real datasets to show that Mango is able to summarize dynamic graphs by meaningful static and temporal patterns