Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Formal Verification of Integrity-Preserving Countermeasures Against Cache Storage Side-Channels
No full textStrengthening the Security of Authenticated Key Exchange against Bad Randomness
Get PDFRecent history has revealed that many random number generators (RNGs) used in cryptographic algorithms and protocols were not providing appropriate randomness, either by accident or on purpose. Subsequently, researchers have proposed new algorithms and protocols that are less dependent on the random number generator. One exception is that all prominent authenticated key exchange (AKE) protocols are insecure given bad randomness, even when using good long-term keying material.
We analyse the security of AKE protocols in the presence of adversaries that can perform attacks based on chosen randomness, i. e., attacks in which the adversary controls the randomness used in protocol sessions. We propose novel stateful protocols, which modify memory shared among a user’s sessions, and show in what sense they are secure against this worst case randomness failure. We develop a stronger security notion for AKE protocols that captures the security that we can achieve under such failures, and prove that our main protocol is correct in this model. Our protocols make substantially weaker assumptions on the RNG than existing protocols
An Automata-Theoretic Approach to Model-Checking Systems and Specifications Over Infinite Data Domains
No full textData-parameterized systems model systems with finite control over an infinite data domain. VLTL is an extension of LTL that uses variables in order to specify properties of computations over infinite data, and as such, VLTL is suitable for specifying properties of data-parameterized systems. We present alternating variable Büchi word automata (AVBWs), a new model of automata over infinite alphabets, capable of modeling a significant fragment of VLTL. While alternating and non-deterministic Büchi automata over finite alphabets have the same expressive power, we show that this is not the case for infinite data domains, as we prove that AVBWs are strictly stronger than the previously defined non-deterministic variable Büchi word automata (NVBWs). However, while the emptiness problem is easy for NVBWs, it is undecidable for AVBWs. We present an algorithm for translating AVBWs to NVBWs in cases where such a translation is possible. Additionally, we characterize the structure of AVBWs that can be translated to NVBWs with our algorithm. We then rely on the natural iterative behavior of our translation algorithm to describe a bounded model-checking procedure for the logic that we consider. Furthermore, we present several fragments of the logic that can be expressed by NVBWs, as well as a fragment that cannot be expressed by NVBWs, yet whose satisfiability is decidable
Stackelberg Planning: Towards Effective Leader-Follower State Space Search
Get PDFInspired by work on Stackelberg security games, we introduce Stackelberg planning, where a leader player in a classical planning task chooses a minimum-cost action sequence aimed at maximizing the plan cost of a follower player in the same task. Such Stackelberg planning can provide useful analyses not only in planning-based security applications like network penetration testing, but also to measure robustness against perturbances in more traditional planning applications (eg with a leader sabotaging road network connections in transportation-type domains). To identify all equilibria–exhibiting the leader's own-cost-vs.-follower-cost tradeoff–we design leader-follower search, a state space search at the leader level which calls in each state an optimal planner at the follower level. We devise simple heuristic guidance, branch-and-bound style pruning, and partial-order reduction techniques for this setting. We run experiments on Stackelberg variants of IPC and pentesting benchmarks. In several domains, Stackelberg planning is quite feasible in practice
The Limitations of Model Uncertainty in Adversarial Settings
No full textMachine learning models are vulnerable to adversarial examples: minor perturbations to input samples intended to deliberately cause misclassification. Many defenses have led to an arms race-we thus study a promising, recent trend in this setting, Bayesian uncertainty measures. These measures allow a classifier to provide principled confidence and uncertainty for an input, where the latter refers to how usual the input is. We focus on Gaussian processes (GP), a classifier providing such principled uncertainty and confidence measures. Using correctly classified benign data as comparison, GP's intrinsic uncertainty and confidence deviate for misclassified benign samples and misclassified adversarial examples. We therefore introduce high-confidence-low-uncertainty adversarial examples: adversarial examples crafted maximizing GP confidence and minimizing GP uncertainty. Visual inspection shows HCLU adversarial examples are malicious, and resemble the original rather than the target class. HCLU adversarial examples also transfer to other classifiers. We focus on transferability to other algorithms providing uncertainty measures, and find that a Bayesian neural network confidently misclassifies HCLU adversarial examples. We conclude that uncertainty and confidence, even in the Bayesian sense, can be circumvented by both white-box and black-box attackers
WADAC: Privacy-Preserving Anomaly Detection and Attack Classification on Wireless Traffic
No full textMGHyper: Checking Satisfiability of HyperLTL Formulas Beyond the \exists* \forall* Fragment
No full textHyperproperties are properties that refer to multiple computation traces. This includes many information-flow security policies,
such as observational determinism, (generalized) noninterference, and
noninference, and other system properties like symmetry or Hamming
distances between in error-resistant codes. We introduce MGHyper, a
tool for automatic satisfiability checking and model generation for hyperproperties expressed in HyperLTL. Unlike previous satisfiability checkers, MGHyper is not limited to the decidable ∃
∗∀
∗
fragment of HyperLTL, but provides a semi-decisionprocedure for the full logic. An
important application of MGHyper is to automatically check equivalences between different hyperproperties (and different formalizations of
the same hyperproperty) and to build counterexamples that disprove
a certain claimed implication. We describe the semi-decisionprocedure
implemented in MGHyper and report on experimental results obtained
both with typical hyperproperties from the literature and with randomly
generated HyperLTL formulas
