Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Formal Verification of Spectres Combination
Get PDFSpeculative execution allows CPUs to improve performance
by using prediction mechanisms that predict the outcome
of branching and other instructions without waiting for the
correct result. When the prediction is wrong, the CPU rolls
back the effects of the speculatively-executed instructions on
the architectural state (i.e., memory, registers). However, the
side effects on the microarchitectural state, which includes
the cache and buffers, are not rolled back and thus can
leak possible confidential data that was speculatively accessed
(Listing 1). Spectre attacks [1–4] demonstrate that most modern CPUs are affected by this speculation-based vulnerability
Specification Decomposition for Reactive Synthesis
Get PDFReactive synthesis is the task of automatically deriving an implementation from a specification. It is a promising technique for the development of verified programs and hardware. Despite recent advances, reactive synthesis is still not practical when the specified systems reach a certain bound in size and complexity. In this paper, we present a modular synthesis algorithm that decomposes the specification into smaller subspecifications. For them, independent synthesis tasks are performed, and the composition of the resulting implementations is guaranteed to satisfy the full specification. Our algorithm is a preprocessing technique that can be applied to a wide range of synthesis tools. We evaluate our approach with state-of-the-art synthesis tools on established benchmarks and obtain encouraging results: The overall runtime decreases significantly when synthesizing implementations modularly
Graph Similarity Description: How Are These Graphs Similar?
Get PDFHow do social networks differ across platforms? How do information networks change over time? Answering questions like these requires us to compare two or more graphs. This task is commonly treated as a measurement problem, but numerical answers give limited insight. Here, we argue that if the goal is to gain understanding, we should treat graph similarity assessment as a description problem instead. We formalize this problem as a model selection task using the Minimum Description Length principle, capturing the similarity of the input graphs in a common model and the differences between them in transformations to individual models. To discover good models, we propose Momo, which breaks the problem into two parts and introduces efficient algorithms for each. Through an extensive set of experiments on a wide range of synthetic and real-world graphs, we confirm that Momo works well in practic
On Compositional Information Flow Aware Refinement
Get PDFThe concepts of information flow security and refinement are known to have had a troubled relationship ever since the seminal work of McLean. In this work we study refinements that
support changes in data representation and semantics, including the addition of state variables that may induce new observational power or side channels. We propose a new epistemic approach to ignorance-preserving refinement where an abstract model is used as a specification of a system’s permitted information flows, that may include the declassification of secret information. The core idea is to require that refinement steps must not induce observer knowledge that is not already available in the abstract model.
Our study is set in the context of a class of shared variable multi-agent models similar to interpreted systems in epistemic logic. We demonstrate the expressiveness of our framework through a series of small examples and compare our approach to existing, stricter notions of information-flow secure refinement based on bisimulations and noninterference preservation. Interestingly, noninterference preservation is not supported “out of the box” in our setting, because refinement steps may introduce new secrets that are independent of secrets already present at abstract level. To support verification, we first introduce a “cube-shaped” unwinding condition related to conditions recently studied in the context of value-dependent noninterference, kernel verification, and secure compilation. A fundamental problem with ignorance-preserving refinement, caused by the support for general data and observation refinement, is that sequential composability is lost. We propose a solution based on relational pre- and post-conditions and illustrate its use together with unwinding on the oblivious RAM construction of Chung and Pass
Revisiting the Security of COMET Authenticated Encryption Scheme
Get PDFCOMETv1, by Gueron, Jha and Nandi, is a mode of operation for nonce-based authenticated encryption with associated data functionality. It was one of the second round candidates in the ongoing NIST Lightweight Cryptography Standardization Process. In this paper, we study a generalized version of COMETv1, that we call gCOMET, from provable security perspective. First, we present a comprehensive and complete security proof for gCOMET in the ideal cipher model. Second, we view COMET, the underlying mode of operation in COMETv1, as an instantiation of gCOMET, and derive its concrete security bounds. Finally, we propose another instantiation of gCOMET, dubbed COMETv2, and show that this version achieves better security guarantees as well as memory-efficient implementations as compared to COMETv1
Parameterized Intractability of Even Set and Shortest Vector Problem
Get PDFThe -Even Set problem is a parameterized variant of the Minimum Distance Problem of linear codes over , which can be stated as follows: given a generator matrix and an integer , determine whether the code generated by has distance at most , or, in other words, whether there is a nonzero vector such that has at most nonzero coordinates. The question of whether -Even Set is fixed parameter tractable (FPT) parameterized by the distance has been repeatedly raised in the literature; in fact, it is one of the few remaining open questions from the seminal book of Downey and Fellows [1999]. In this work, we show that
-Even Set is W[1]-hard under randomized reductions.
We also consider the parameterized
-Shortest Vector Problem (SVP), in which we are given a lattice whose basis vectors are integral and an integer , and the goal is to determine whether the norm of the shortest vector (in the norm for some fixed ) is at most . Similar to -Even Set, understanding the complexity of this problem is also a long-standing open question in the field of Parameterized Complexity. We show that, for any , -SVP is W[1]-hard to approximate (under randomized reductions) to some constant factor
On the Soundness of Infrastructure Adversaries
Get PDFCompanies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation.
In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the
symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols.
We show, in general, how the soundness and completeness of a rule-based model can be ensured by verifying trace properties, linking soundness to safety properties and completeness to liveness properties. We then demonstrate the approach for a recently proposed threat model that quantifies the confidentiality of email communication on the Internet, including DNS, DNSSEC, and SMTP. Using off-the-shelf protocol verification tools, we discover two flaws in their threat model. After fixing them, we show that it provides symbolic soundness
Hijack-GAN: Unintended-Use of Pretrained, Black-Box GANs
No full textWhile Generative Adversarial Networks (GANs) show increasing performance and the level of realism is becoming indistinguishable from natural images, this also comes with high demands on data and computation. We show that state-of-the-art GAN models -- such as they are being publicly released by researchers and industry -- can be used for a range of applications beyond unconditional image generation. We achieve this by an iterative scheme that also allows gaining control over the image generation process despite the highly non-linear latent spaces of the latest GAN models. We demonstrate that this opens up the possibility to re-use state-of-the-art, difficult to train, pre-trained GANs with a high level of control even if only black-box access is granted. Our work also raises concerns and awareness that the use cases of a published GAN model may well reach beyond the creators' intention, which needs to be taken into account before a full public release
SUSAN: The Structural Similarity Random Walk Kernel
Get PDFRandom walk kernels are a very flexible family of graph kernels, in which we can incorporate edge and vertex similarities through positive definite kernels. In this work we study the particular case within this family in which the vertex kernel has bounded support. We motivate this property as the configurable flexibility in terms of vertex alignment between the two graphs on which the walk is performed. We study several fast and intuitive ways to derive structurally aware labels and combine them with such a vertex kernel, which in turn is incorporated in the random walk kernel. We provide a fast algorithm to compute the resulting random walk kernel and we give precise bounds on its computational complexity. We show that this complexity always remains upper bounded by that of alternative methods in the literature and study conditions under which this advantage can be significantly higher. We evaluate the resulting configurations on their predictive performance on several families of graphs and show significant improvements against the vanilla random walk kernel and other competing algorithms.
Read More: https://epubs.siam.org/doi/abs/10.1137/1.9781611976700.3
SoK: Computer-Aided Cryptography
Get PDFComputer-aided cryptography is an active area of research that develops and applies formal, machine-checkable approaches to the design, analysis, and implementation of cryptography. We present a cross-cutting systematization of the computer-aided cryptography literature, focusing on three main areas: (i) design-level security (both symbolic security and computational security), (ii) functional correctness and efficiency,and (iii) implementation-level security (with a focus on digital side-channel resistance). In each area, we first clarify the role of computer-aided cryptography—how it can help and what the caveats are—in addressing current challenges. We next present a taxonomy of state-of-the-art tools, comparing their accuracy,scope, trustworthiness, and usability. Then, we highlight their main achievements, trade-offs, and research challenges. After covering the three main areas, we present two case studies. First, we study efforts in combining tools focused on different areas to consolidate the guarantees they can provide. Second, we distill the lessons learned from the computer-aided cryptography community’s involvement in the TLS 1.3 standardization effort.Finally, we conclude with recommendations to paper authors,tool developers, and standardization bodies moving forward