Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Synthesizing Approximate Implementations for Unrealizable Specifications
Get PDFThe unrealizability of a specification is often due to the assumption that the behavior of the environment is unrestricted. In this
paper, we present algorithms for synthesis in bounded environments,
where the environment can only generate input sequences that are ultimately periodic words (lassos) with finite representations of bounded
size. We provide automata-theoretic and symbolic approaches for solving this synthesis problem, and also study the synthesis of approximative
implementations from unrealizable specifications. Such implementations
may violate the specification in general, but are guaranteed to satisfy the
specification on at least a specified portion of the bounded-size lassos.
We evaluate the algorithms on different arbiter specifications
Carving Parameterized Unit Tests
Get PDFWe present a method to automatically extract ("carve") parameterized unit tests from system test executions. The unit tests execute the same functions as the system tests they are carved from, but can do so much faster as they call functions directly; furthermore, being parameterized, they can execute the functions with a large variety of randomly selected input values. If a unit-level test fails, we lift it to the system level to ensure the failure can be reproduced there. Our method thus allows to focus testing efforts on selected modules while still avoiding false alarms: In our experiments, running parameterized unit tests for individual functions was, on average, 30~times faster than running the system tests they were carved from
Modern MDL meets Data Mining Insights, Theory, and Practice
Get PDFWhen considering a data set it is often unknown how complex it is, and hence it is difficult to assess how rich a model for the data should be. Often these choices are swept under the carpet, ignored, left to the domain expert, but in practice this is highly unsatisfactory; domain experts do not know how to set , what prior to choose, or how many degrees of freedom is optimal any more than we do.
The Minimum Description Length~(MDL) principle can answer the model selection problem from an intuitively appealing and clear viewpoint of information theory and data compression. In a nutshell, it asserts that the best model is the one that best compresses both the data and that model.
It does not only imply the best strategy for model selection, but also gives a unifying viewpoint of designing optimal data mining algorithms for a wide range of issues, and has been very successfully applied to a wide range of data mining tasks, ranging from pattern mining, clustering, classification, text mining, graph mining, anomaly detection, up to causal inference.
In this tutorial we give an introduction to the basics of model selection, show important properties of MDL-based modelling, successful examples as well as pitfalls for how to apply MDL to solve data mining problems, but also introduce advanced topics on important new concepts in modern MDL (e.g, normalized maximum likelihood (NML), sequential NML, decomposed NML, and MDL change statistics) and emerging applications in dynamic settings
Component-Based Formal Analysis of 5G-AKA: Channel Assumptions and Session Confusion
Get PDFThe 5G mobile telephony standards are nearing completion; upon adoption these will be used by billions across
the globe. Ensuring the security of 5G communication is of the utmost importance, building trust in a critical component of everyday life and national infrastructure.
We perform fine-grained formal analysis of 5G’s main authentication and key agreement protocol (AKA), and provide
the first models to explicitly consider all parties defined by the protocol specification. Our analysis reveals that the security of 5G-AKA critically relies on unstated assumptions on the inner workings of the underlying channels. In practice this means that following the 5G-AKA specification, a provider can easily and ‘correctly’ implement the standard insecurely, leaving the protocol vulnerable to a security-critical race condition. We provide the first models and analysis considering component and channel compromise in 5G, whose results further demonstrate the fragility and subtle trust assumptions of the 5G-AKA protocol.
We propose formally verified fixes to the encountered issues, and have worked with 3GPP to ensure these fixes are adopted
Poster: TGX: Secure SGX enclave management using TPM
Get PDFIntel SGX provides a trusted execution environment
on commodity computing platforms. Recent micro-architectural attacks like Spectre, Meltdown, or Foreshadow, however, raise doubts about the promised isolation of SGX-protected code and data, including some of the necessary cryptographic operations and credentials, e.g., for attestation.
In this poster we present TGX, a combination of SGX and
TPM working together to provide stronger isolation of crucial cryptographic operations of SGX and a way to circumvent microarchitectural attacks against SGX. TGX enables SGX to move its signing and verification mechanism from processor to TPM making the security sensitive information never available outside TPM, removing, for instance, the possibilities of stealing them from L1 cache. In particular, TGX should motivate that SGX and TPM can form a beneficial symbiosis
Automated Verification of Accountability in Security Protocols
Get PDFAccountability is a recent paradigm in security protocol design which aims to
eliminate traditional trust assumptions on parties and hold
them accountable for their misbehavior.
It is meant to establish trust in the first place and to
recognize and react if this trust is violated.
In this work, we discuss a protocol-agnostic definition of accountability:
a protocol provides accountability (w.r.t. some security property)
if it can identify all misbehaving parties, where
misbehavior is defined as a deviation from the protocol that causes
a security violation.
We provide a mechanized method for the
verification of accountability and demonstrate its use for
verification and attack finding on various examples from the
accountability and causality literature, including Certificate Transparency and
Kroll’s Accountable Algorithms protocol.
We reach a high degree of automation by expressing accountability in terms of
a set of trace properties and show their soundness and completeness
Causality & Control flow
Get PDFCausality has been the issue of philosophic debate since
Hippocrates. It is used in formal verification and testing, e.g.,
to explain counterexamples or construct fault trees. Recent work
defines actual causation in terms of Pearl's causality framework,
but most definitions brought forward so far struggle with examples
where one event preempts another one. A key point to capturing
such examples in the context of programs or distributed systems is
a sound treatment of control flow. We discuss how causal models
should incorporate control flow and discover that much of what
Pearl/Halpern's notion of contingencies tries to capture is
captured better by an explicit modelling of the control flow in
terms of structural equations and an arguably simpler definition.
Inspired by causality notions in the security domain, we bring
forward a definition of causality that takes these
control-variables into account. This definition provides a clear
picture of the interaction between control flow and causality and
captures these notoriously difficult preemption examples without
secondary concepts. We give convincing results on a benchmark of
34 examples from the literature
We Are Not Your Real Parents: Telling Causal from Confounded using MDL
Get PDFGiven data over variables (X1,...,Xm,Y) we consider the problem of finding out whether X jointly causes Y or whether they are all confounded by an unobserved latent variable Z. To do so, we take an information-theoretic approach based on Kolmogorov complexity. In a nutshell, we follow the postulate that first encoding the true cause, and then the effects given that cause, results in a shorter description than any other encoding of the observed variables.
The ideal score is not computable, and hence we have to approximate it. We propose to do so using the Minimum Description Length (MDL) principle. We compare the MDL scores under the models where X causes Y and where there exists a latent variables Z confounding both X and Y and show our scores are consistent. To find potential confounders we propose using latent factor modeling, in particular, probabilistic PCA (PPCA).
Empirical evaluation on both synthetic and real-world data shows that our method, CoCa, performs very well -- even when the true generating process of the data is far from the assumptions made by the models we use. Moreover, it is robust as its accuracy goes hand in hand with its confidence
Prime, Order Please! Revisiting Small Subgroup and Invalid Curve Attacks on Protocols using Diffie-Hellman
Get PDFDiffie-Hellman groups are a widely used component in cryptographic protocols in which a
shared secret is needed. These protocols are typically proven to be secure under the assumption they
are implemented with prime order Diffie Hellman groups. However, in practice, many implementations
either choose to use non-prime order groups for reasons of efficiency, or can be manipulated into
operating in non-prime order groups. This leaves a gap between the proofs of protocol security, which
assume prime order groups, and the real world implementations. This is not merely a theoretical
possibility: many attacks exploiting small subgroups or invalid curve points have been found in the
real world.
While many advances have been made in automated protocol analysis, modern tools such as Tamarin
and ProVerif represent DH groups using an abstraction of prime order groups. This means they, like
many cryptographic proofs, may miss practical attacks on real world protocols.
In this work we develop a novel extension of the symbolic model of Diffie-Hellman groups. By more
accurately modelling internal group structure, our approach captures many more differences between
prime order groups and their actual implementations. The additional behaviours that our models
capture are surprisingly diverse, and include not only attacks using small subgroups and invalid curve
points, but also a range of proposed mitigation techniques, such as excluding low order elements,
single coordinate ladders, and checking the elliptic curve equation. Our models thereby capture a
large family of attacks that were previously outside the symbolic model.
We implement our improved models in the Tamarin prover. We find a new attack on the Secure
Scuttlebutt Gossip protocol, independently discover a recent attack on Tendermint’s secure handshake,
and evaluate the effectiveness of the proposed mitigations for recent Bluetooth attacks
Privacy-aware eye tracking using differential privacy
No full textWith eye tracking being increasingly integrated into virtual and augmented reality (VR/AR) head-mounted displays, preserving users’ privacy is an ever more important, yet under-explored, topic in the eye tracking community. We report a large-scale online survey (N=124) on privacy aspects of eye tracking that provides the first comprehensive account of with whom, for which services,
and to what extent users are willing to share their gaze data. Using these insights, we design a privacy-aware VR interface that uses differential privacy, which we evaluate on a new 20-participant dataset for two privacy sensitive tasks: We show that our method can prevent user re-identification and protect gender information while maintaining high performance for gaze-based document type
classification. Our results highlight the privacy challenges particular to gaze data and demonstrate that differential privacy is a potential means to address them. Thus, this paper lays important foundations for future research on privacy-aware gaze interfaces