Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Realizable and Context-Free Hyperlanguages
Get PDFHyperproperties lift conventional trace-based languages from a set of execution traces to a set of sets of executions. From a formal-language perspective, these are sets of sets of words, namely hyperlanguages. Hyperautomata are based on classical automata models that are lifted to handle hyperlanguages. Finite hyperautomata (NFH) have been suggested to express regular hyperproperties. We study the realizability problem for regular hyperlanguages: given a set of languages, can it be precisely described by an NFH? We show that the problem is complex already for singleton hyperlanguages.
We then go beyond regular hyperlanguages, and study context-free hyperlanguages. We show that the natural extension to context-free hypergrammars is highly undecidable. We then suggest a refined model, namely synchronous hypergrammars, which enables describing interesting non-regular hyperproperties, while retaining many decidable properties of context-free grammars
Blurtooth: Exploiting cross-transport key derivation in Bluetooth classic and Bluetooth low energy
Get PDFBluetooth is a pervasive wireless technology specified in an open
standard. The standard defines Bluetooth Classic (BT) for high-
throughput wireless services and Bluetooth Low Energy (BLE) very
low-power ones. The standard also specifies security mechanisms,
such as pairing, session establishment, and cross-transport key
derivation (CTKD). CTKD enables devices to establish BT and BLE
security keys by pairing just once. CTKD was introduced in 2014
with Bluetooth 4.2 to improve usability. However, the security im-
plications of CTKD were not studied carefully.
This work demonstrates that CTKD is a valuable and novel Blue-
tooth attack surface. It enables, among others, to exploit BT and BLE
just by targeting one of the two (i.e., Bluetooth cross-transport ex-
ploitation). We present the design of the first cross-transport attacks
on Bluetooth. Our attacks exploit issues that we identified in the
specification of CTKD. For example, we find that CTKD enables an
adversary to overwrite pairing keys across transports. We leverage
these vulnerabilities to impersonate, machine-in-the-middle, and
establish unintended sessions with any Bluetooth device support-
ing CTKD. Since the presented attacks blur the security boundary
between BT and BLE, we name them BLUR attacks. We provide a
low-cost implementation of the attacks and test it on a broad set
of devices. In particular, we successfully attack 16 devices with 14
unique Bluetooth chips from popular vendors (e.g., Cypress, Intel,
Qualcomm, CSR, Google, and Samsung), with Bluetooth standard
versions of up to 5.2. We discuss why the countermeasures in the
Bluetooth are not effective against our attacks, and we develop and
evaluate practical and effective alternatives
Deciding Hyperproperties Combined with Functional Specifications
No full textWe study satisfiability for HyperLTL with a ∀∗∃∗ quantifier prefix, known to be highly undecidable in general. HyperLTL can express system properties that relate multiple traces (so-called hyperproperties), which are often combined with trace properties that specify functional behavior on single traces. Following this conceptual split, we first define several safety and liveness fragments of ∀∗∃∗ HyperLTL, and characterize the complexity of their (often much easier) satisfiability problem. We then add LTL trace properties as functional specifications. Though (highly) undecidable in many cases, this way of combining “simple” HyperLTL and arbitrary LTL also leads to interesting new decidable fragments. This systematic study of ∀∗∃∗ fragments is complemented by a new algorithm for ∀∃ ∗ -HyperLTL satisfiability, which is incomplete but often successful
BOCoSy: Small but Powerful Symbolic Output-Feedback Control
No full textWe present BOCoSy, a tool for bounded symbolic output-feedback controller synthesis. BOCoSy synthesizes symbolic output-feedback controllers which interact with a given plant via a pre-defined finite symbolic interface. BOCoSy solves this problem by a new lazy abstraction-refinement technique which starts with a very coarse abstraction of the external trace semantics of the given plant and iteratively removes non-admissible behavior from this abstract model until a controller is found. BOCoSy steers the search for controllers towards small and concise state space representations by utilizing ideas from bounded synthesis. As a result, BOCoSy returns small and explainable controllers that are still powerful enough to solve the given synthesis problem. We show that BOCoSy is able to synthesize small, human readable symbolic controllers quickly on a set of benchmarks
A Recursive Early-Stopping Phase King Protocol
No full textEarly-stopping consensus protocols guarantee termination within
a number of rounds that depends only on the actual number ???? of
faulty nodes in a run, not the maximum number of faults that can
be tolerated. We consider early-stopping deterministic synchro-
nous consensus with Byzantine faults in a fully connected message
passing system of ???? nodes. Many such protocols are known, but so
far none combine early-stopping in ????(???? + 1) rounds with optimal
resilience and a bit complexity of ????(????2(???? + 1)).
We provide two solutions to the above problem. The first is a low-
hanging fruit that almost matches the above requirements, but has
worst-case message and bit complexities of Θ(????2 log(???? + 2)). The
second reduces the bit complexity further to ????(????2) at the expense
of increasing the constant factor in the running time bound. It
does so by calling itself recursively at most twice on Θ(????)-sized
subsets. This presents a substantial technical hurdle, since it is
not known when the recursive call will terminate, and relying
on a worst-case bound would lose the property of stopping early.
We overcome this obstacle by introducing a (re-)synchronization
barrier in the calling routine that forces all correct nodes to proceed
in its execution within one round of each other, complemented
by a simple mechanism to simulate synchronous execution in this
almost synchronized setting. The result is the first protocol that is
simultenously optimally resilient, asymptotically optimally early-
stopping, and asymptotically bit- and message-optimal
TrustedGateway: TEE-Assisted Routing and Firewall Enforcement Using ARM TrustZone
Get PDFGateway routers are at the heart of every network infrastructure, interconnecting subnetworks and enforcing access control policies using firewalls.
However, their central position makes them high-value targets for network compromises.
Typically, gateways are erroneously assumed to be hardened against software vulnerabilities (``bastion host'').
In fact, though, they inherit the attack surface of their underlying commodity OSes which together with the wealth of auxiliary services available on both consumer and enterprise gateways---web and VoIP, file sharing, remote logins, monitoring, etc.---undermines this belief.
This is underlined by a plethora of recent CVEs for commodity OSes and services of popular routers which resulted in authentication bypass or remote code execution thus enabling attackers full control over their security policies.
We present TrustedGateway (TruGW), a new gateway architecture, which isolates ``core'' networking features---routing and firewall---from error-prone auxiliary services and gateway OSes.
TruGW leverages a TEE-assisted design to protect the network path and policies while staying compatible with commodity gateway platforms.
TruGW uses ARM TrustZone to protect the NIC and traffic processing from a fully-compromised gateway and permits policy updates only by trusted remote administrators.
That way, TruGW can readily guarantee the secure enforcement of trusted policies on commodity gateways.
TruGW's small attack surface is a key enabler to regain trust in core network infrastructures
Label-Descriptive Patterns and their Application to Characterizing Classification Errors
Get PDFState-of-the-art deep learning methods achieve human-like performance on many tasks, but make errors nevertheless. Characterizing these errors in easily interpretable terms gives insight into whether a classifier is prone to making systematic errors, but also gives a way to act and improve the classifier. We propose to discover those feature- value combinations (ie. patterns) that strongly correlate with correct resp. erroneous predictions to obtain a global and interpretable description for arbitrary classifiers. We show this is an instance of the more general label description problem, which we formulate in terms of the Minimum De- scription Length principle. To discover a good pattern set, we develop the efficient PREMISE al- gorithm. Through an extensive set of experiments we show it performs very well in practice on both synthetic and real-world data. Unlike existing solutions, it ably recovers ground truth patterns, even on highly imbalanced data over many fea- tures. Through two case studies on Visual Ques- tion Answering and Named Entity Recognition, we confirm that PREMISE gives clear and action- able insight into the systematic errors made by modern NLP classifiers
ProgFed: Effective, Communication, and Computation Efficient Federated Learning by Progressive Training
Get PDFFederated learning is a powerful distributed learning scheme that allows numerous edge devices to collaboratively train a model without sharing their data. However, training is resource-intensive for edge devices, and limited network bandwidth is often the main bottleneck. Prior work often overcomes the constraints by condensing the models or messages into compact formats, e.g., by gradient compression or distillation. In contrast, we propose ProgFed, the first progressive training framework for efficient and effective federated learning. It inherently reduces computation and two-way communication costs while maintaining the strong performance of the final models. We theoretically prove that ProgFed converges at the same asymptotic rate as standard training on full models. Extensive results on a broad range of architectures, including CNNs (VGG, ResNet, ConvNets) and U-nets, and diverse tasks from simple classification to medical image segmentation show that our highly effective training approach saves up to 20 computation and up to 63 communication costs for converged models. As our approach is also complimentary to prior work on compression, we can achieve a wide range of trade-offs by combining these techniques, showing reduced communication of up to 50× at only 0.1 loss in utility. Code is available at https://github.com/a514514772/ProgFed
DRAGON: Determining Regulatory Associations using Graphical models on multi-Omic Networks
Get PDFThe increasing quantity of multi-omic data, such as methylomic and transcriptomic profiles collected on the same specimen or even on the same cell, provides a unique opportunity to explore the complex interactions that define cell phenotype and govern cellular responses to perturbations. We propose a network approach based on Gaussian Graphical Models (GGMs) that facilitates the joint analysis of paired omics data. This method, called DRAGON (Determining Regulatory Associations using Graphical models on multi-Omic Networks), calibrates its parameters to achieve an optimal trade-off between the network’s complexity and estimation accuracy, while explicitly accounting for the characteristics of each of the assessed omics ‘layers.’ In simulation studies, we show that DRAGON adapts to edge density and feature size differences between omics layers, improving model inference and edge recovery compared to state-of-the-art methods. We further demonstrate in an analysis of joint transcriptome - methylome data from TCGA breast cancer specimens that DRAGON can identify key molecular mechanisms such as gene regulation via promoter methylation. In particular, we identify Transcription Factor AP-2 Beta (TFAP2B) as a potential multi-omic biomarker for basal-type breast cancer. DRAGON is available as open-source code in Python through the Network Zoo package (netZooPy v0.8; netzoo.github.io)
On Specifications and Proofs of Timed Circuits
Get PDFGiven a discrete-state continuous-time reactive system, like a digital circuit, the classical approach is to first model it as a state transition system and then prove its properties. Our contribution advocates a different approach: to directly operate on the input-output behavior of such systems, without identifying states and their transitions in the first place. We discuss the benefits of this approach at hand of some examples, which demonstrate that it nicely integrates with concepts of self-stabilization and fault-tolerance. We also elaborate on some unexpected artefacts of module composition in our framework, and conclude with some open research questions