Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Tight Complexity Bounds for Counting Generalized Dominating Sets in Bounded-Treewidth Graphs
Full text linkWe investigate how efficiently a well-studied family of domination-type problems can be solved on bounded-treewidth graphs.
For sets of non-negative integers, a -set of a graph is a set of vertices such that for every , and for every .
The problem of finding a -set (of a certain size) unifies standard problems such as \textsc{Independent Set}, \textsc{Dominating Set}, \textsc{Independent Dominating Set}, and many others.
For almost all pairs of finite or cofinite sets , we determine (under standard complexity assumptions) the best possible value such that there is an algorithm that counts -sets in time c_{\sigma,\rho}^\tw\cdot n^{\O(1)} (if a tree decomposition of width \tw is given in the input).
Let \sigMax denote the largest element of if is finite, or the largest missing integer if is cofinite; \rhoMax is defined analogously for .
Surprisingly, is often significantly smaller than the natural bound \sigMax+\rhoMax+2 achieved by existing algorithms [van Rooij, 2020].
Toward defining , we say that is \mname-structured if there is a pair such that every integer in equals mod \mname, and every integer in equals mod \mname.
Then, setting
\begin{itemize}
\item c_{\sigma,\rho}=\max\{\sigMax,\rhoMax\}+1 if is
\mname-structured for some \mname \ge 3, or 2-structured with \sigMax\neq \rhoMax, or 2-structured with \sigMax=\rhoMax being odd,
\item c_{\sigma,\rho}=\max\{\sigMax,\rhoMax\}+2 if is 2-structured,
but not \mname-structured for any \mname \ge 3, and \sigMax=\rhoMax is even, and
\item c_{\sigma,\rho}=\sigMax+\rhoMax+2 if is not
\mname-structured for any \mname\ge 2,
\end{itemize}
we provide algorithms counting -sets in time c_{\sigma,\rho}^\tw\cdot n^{\O(1)}.
For example, for the \textsc{Exact Independent Dominating Set} problem (also known as
\textsc{Perfect Code}) corresponding to and , this improves the
3^\tw\cdot n^{\O(1)} algorithm
of van Rooij to 2^\tw\cdot n^{\O(1)}.
Despite the unusually delicate definition of , we show that our algorithms are most likely optimal, i.e.,
for any pair of finite or cofinite sets where the problem is non-trivial (except those having cofinite with ), and any , a (c_{\sigma,\rho}-\varepsilon)^\tw\cdot
n^{\O(1)}-algorithm counting the number of -sets would violate the Counting Strong Exponential-Time Hypothesis (\#SETH).
For finite sets and , our lower bounds also extend to the decision version, showing that our algorithms are optimal in this setting as well.
In contrast, for many cofinite sets, we show that further significant improvements for the decision and optimization versions are possible using the technique of representative sets
Automated Security Analysis of Exposure Notification Systems
Full text linkWe present the first formal analysis and comparison of the security of the two most widely deployed exposure notification systems, ROBERT and the Google and Apple Exposure Notification (GAEN) framework.
ROBERT is the most popular instalment of the centralised approach to exposure notification, in which the risk score is computed by a central server. GAEN, in contrast, follows the decentralised approach, where the user's phone calculates the risk. The relative merits of centralised and decentralised systems have proven to be a controversial question. The majority of the previous analyses have focused on the privacy implications of these systems, ours is the first formal analysis to evaluate the security of the deployed systems---the absence of false risk alerts.
We model the French deployment of ROBERT and the most widely deployed GAEN variant, Germany's Corona-Warn-App. We isolate the precise conditions under which these systems prevent false alerts. We determine exactly how an adversary can subvert the system via network and Bluetooth sniffing, database leakage or the compromise of phones, back-end systems and health authorities. We also investigate the security of the original specification of the DP3T protocol, in order to identify gaps between the proposed scheme and its ultimate deployment.
We find a total of 27 attack patterns, including many that distinguish the centralised from the decentralised approach, as well as attacks on the authorisation procedure that differentiate all three protocols. Our results suggest that ROBERT's centralised design is more vulnerable against both opportunistic and highly resourced attackers trying to perform mass-notification attacks
Automated Analysis of Protocols that use Authenticated Encryption: How Subtle AEAD Differences can impact Protocol Security
Full text linkMany modern security protocols such as TLS, WPA2, WireGuard, and Signal use a cryptographic primitive called Authenticated Encryption (optionally with Authenticated Data), also known as an AEAD scheme. AEAD is a variant of symmetric encryption that additionally provides authentication. While authentication may seem to be a straightforward additional requirement, it has in fact turned out to be complex: many different security notions for AEADs are still being proposed, and several recent protocol-level attacks exploit subtle behaviors that differ among real-world AEAD schemes.
We provide the first automated analysis method for protocols that use AEADs that can systematically find attacks that exploit the subtleties of the specific type of AEAD used. This can then be used to analyze specific protocols with a fixed AEAD choice, or to provide guidance on which AEADs might be (in)sufficient to make a protocol design secure. We develop generic symbolic AEAD models, which we instantiate for the Tamarin prover. Our approach can automatically and efficiently discover protocol attacks that could previously only be found using manual inspection, such as the Salamander attack on Facebook’s message franking, and attacks on SFrame and YubiHSM. Furthermore, our analysis reveals undesirable behaviors of several other protocols
ResolFuzz: Differential Fuzzing of DNS Resolvers
Full text linkThis paper identifies and analyzes vulnerabilities in the DNS infrastructure, with particular focus on recursive DNS resolvers. We aim to identify semantic bugs that could lead to incorrect resolver responses, introducing risks to the internet’s critical infrastructure. To achieve this, we introduce ResolFuzz, a mutation-based fuzzer to search for semantic differences across DNS resolver implementations. ResolFuzz combines differential analysis with a rule-based mechanism to distinguish between benign differences and potential threats. We evaluate our prototype on seven resolvers and uncover multiple security vulnerabilities, including inaccuracies in resolver responses and possible amplification issues in PowerDNS Recursor’s handling of DNAMEResource Records (RRs). Moreover, we demonstrate the potential for self-sustaining DoS attacks in resolved and trust-dns, further underlining the necessity of comprehensive DNS security. Through these contributions, our research underscores the potential of differential fuzzing in uncovering DNS vulnerabilities
Certifiers Make Neural Networks Vulnerable to Availability Attacks
Full text linkTo achieve reliable, robust, and safe AI systems, it is vital to implement fallback strategies when AI predictions cannot be trusted. Certifiers for neural networks are a reliable way to check the robustness of these predictions. They guarantee for some predictions that a certain class of manipulations or attacks could not have changed the outcome. For the remaining predictions without guarantees, the method abstains from making a prediction, and a fallback strategy needs to be invoked, which typically incurs additional costs, can require a human operator, or even fail to provide any prediction. While this is a key concept towards safe and secure AI, we show for the first time that this approach comes with its own security risks, as such fallback strategies can be deliberately triggered by an adversary. In addition to naturally occurring abstains for some inputs and perturbations, the adversary can use training-time attacks to deliberately trigger the fallback with high probability. This transfers the main system load onto the fallback, reducing the overall system's integrity and/or availability. We design two novel availability attacks, which show the practical relevance of these threats. For example, adding 1% poisoned data during training is sufficient to trigger the fallback and hence make the model unavailable for up to 100% of all inputs by inserting the trigger. Our extensive experiments across multiple datasets, model architectures, and certifiers demonstrate the broad applicability of these attacks. An initial investigation into potential defenses shows that current approaches are insufficient to mitigate the issue, highlighting the need for new, specific solutions
White-box Concealment Attacks Against Anomaly Detectors for Cyber-Physical Systems
No full textAnomaly detection for cyber-physical systems is an effective method to detect ongoing process anomalies caused by an attacker. Recently, a number of anomaly detection techniques were proposed (e.g., ML based, invariant rule based, control theoretical). Little is known about the resilience of those anomaly detectors against attackers that conceal their attacks to evade detection. In particular, their resilience against white-box concealment attacks has so far only been investigated for the subset of neural network-based detectors. In this work, we demonstrate for the first time that white-box concealment attacks can also be applied to detectors that are not based on neural network solutions. In order to achieve this, we propose a generic white-box attack that evades anomaly detectors and can be adapted even if the target detection technique does not optimize a loss function. We design and implement a framework to perform our attacks, and test it on several detectors from related work. Our results show that it is possible to completely evade a wide range of detectors (based on diverse detection techniques) while reducing the number of samples that need to be manipulated (compared to prior black-box concealment attacks)
FetchBench: Systematic Identification and Characterization of Proprietary Prefetchers
Full text linkPrefetchers speculatively fetch memory using predictions on future memory use by applications. Different CPUs may use different prefetcher types, and two implementations of the same prefetcher can differ in details of their characteristics, leading to distinct runtime behavior. For a few implementations, security researchers showed through manual analysis how to exploit specific prefetchers to leak data. Identifying such vulnerabilities required tedious reverse-engineering, as prefetcher implementations are proprietary and undocumented. So far, no systematic study of prefetchers in common CPUs is available, preventing further security assessment.
In this work, we address the following question: How can we systematically identify and characterize under-specified prefetchers in proprietary processors? To answer this question, we systematically analyze approaches to prefetching, design cross-platform tests to identify and characterize prefetchers on a given CPU, and demonstrate that our implementation FetchBench can characterize prefetchers on 19 different ARM and x86-64 CPUs. For example, FetchBench uncovers and characterizes a previously unknown replay-based prefetcher on the ARM Cortex-A72 CPU. Based on these findings, we demonstrate two novel attacks that exploit this undocumented prefetcher as a side channel to leak secret information, even from the secure TrustZone into the normal world
Chopsticks: Fork-Free Two-Round Multi-Signatures from Non-Interactive Assumptions
Full text linkMulti-signatures have been drawing lots of attention in recent years, due to their applications in cryptocurrencies.
Most early constructions require three-round signing, and recent constructions have managed to reduce the round complexity to two. However, their security proofs are mostly based on non-standard, interactive assumptions (e.g. one-more assumptions) and come with a huge security loss, due to multiple uses of rewinding (aka the Forking Lemma).
This renders the quantitative guarantees given by the security proof useless.
In this work, we improve the state of the art by proposing two efficient two-round multi-signature schemes from the (standard, non-interactive) Decisional Diffie-Hellman (DDH) assumption.
Both schemes are proven secure in the random oracle model without rewinding.
We do not require any pairing either.
Our first scheme supports key aggregation but has a security loss linear in the number of signing queries, and our second scheme is the first tightly secure construction.
A key ingredient in our constructions is a new homomorphic dual-mode commitment scheme for group elements, that allows to equivocate for messages of a certain structure.
The definition and efficient construction of this commitment scheme is of independent interest
nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models
Full text linkA rigorous formalization of desired system requirements is indispensable when performing any verification task. This often limits the application of verification techniques, as writing formal specifications is an error-prone and time-consuming manual task. To facilitate this, we present nl2spec, a framework for applying Large Language Models (LLMs) to derive formal specifications (in temporal logics) from unstructured natural language. In particular, we introduce a new methodology to detect and resolve the inherent ambiguity of system requirements in natural language: we utilize LLMs to map subformulas of the formalization back to the corresponding natural language fragments of the input. Users iteratively add, delete, and edit these sub-translations to amend erroneous formalizations, which is easier than manually redrafting the entire formalization. The framework is agnostic to specific application domains and can be extended to similar specification languages and new neural models. We perform a user study to obtain a challenging dataset, which we use to run experiments on the quality of translations. We provide an open-source implementation, including a web-based frontend
Empirical Research Methods in Usable Privacy and Security
Full text linkResearchers in the usable privacy and security (UPS) field study privacy- and security-relevant perceptions and behaviors and aim to design systems that simul- taneously address requirements for usability/user experience, security, and privacy. Human-computer interaction (HCI) and social science research methods are well-suited to study many of the types of questions that are relevant in UPS, which often involve concepts such as subjective experience, attitudes, understanding, behavior and behavior change. However, there are many challenges specific to UPS that are not usually described in more generic methods textbooks. We highlight techniques for risk representation, options for participant recruitment, ethics-related topics in study design, and biases that may play a role in UPS studies with human participants