Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Two-Message Statistically Sender-Private OT from LWE
Get PDF: We construct a two-message oblivious transfer (OT) protocol without setup that guarantees statistical privacy for the sender even against malicious receivers. Receiver privacy is game based and relies on the hardness of learning with errors (LWE). This flavor of OT has been a central building block for minimizing the round complexity of witness indistinguishable and zero knowledge proof systems and multi-party computation protocols, as well as for achieving circuit privacy for homomorphic encryption in the malicious setting. Prior to this work, all candidates in the literature from standard assumptions relied on number theoretic assumptions and were thus insecure in the post-quantum setting. This work provides the first (presumed) post-quantum secure candidate and thus allows to instantiate the aforementioned applications in a post-quantum secure manner.
Technically, we rely on the transference principle: Either a lattice or its dual must have short vectors. Short vectors, in turn, can be translated to information loss in encryption. Thus encrypting one message with respect to the lattice and one with respect to its dual guarantees that at least one of them will be statistically hidden
Guiding app testing with mined interaction models
No full textTest generators for graphical user interfaces must constantly choose which UI element to interact with, and how. We guide this choice by mining associations between UI elements and their interactions from the most common applications. Once mined, the resulting UI interaction model can be easily applied to new apps and new test generators. In our experiments, the mined interaction models lead to code coverage improvements of 19.41% and 43.03% on average on two state-of-the-art tools (DROIDMATE and DROIDBOT), when executing the same number of actions
Synthesizing Reactive Systems from Hyperproperties
No full textWe study the reactive synthesis problem for hyperproperties
given as formulas of the temporal logic HyperLTL. Hyperproperties generalize trace properties, i.e., sets of traces, to sets of sets of traces. Typical
examples are information-flow policies like noninterference, which stipulate that no sensitive data must leak into the public domain. Such properties cannot be expressed in standard linear or branching-time temporal
logics like LTL, CTL, or CTL∗
. We show that, while the synthesis problem is undecidable for full HyperLTL, it remains decidable for the ∃
∗
,
∃
∗∀
1
, and the linear ∀
∗
fragments. Beyond these fragments, the synthesis problem immediately becomes undecidable. For universal HyperLTL,
we present a semi-decision procedure that constructs implementations
and counterexamples up to a given bound. We report encouraging experimental results obtained with a prototype implementation on example specifications with hyperproperties like symmetric responses, secrecy,
and information-flow
Model Checking Security Protocols
No full textThe formal analysis of security protocols is a prime example of a domain where model checking has been successfully applied. Although security protocols are typically small, analysis by hand is difficult as a protocol should work even when arbitrarily many runs are interleaved and in the presence of an adversary. Specialized model-checking techniques have been developed that address both the problems of unbounded, interleaved runs and a prolific, highly nondeterministic adversary.These techniques have been implemented in model-checking tools that now scale to protocols of realistic size and can be used to aid protocol design and standardization.In this chapter, we provide an overview of the main applications of model checking in security protocol analysis. We explain the central concepts involved in the analysis of security protocols: the abstraction of messages, protocols as role automata, the adversary model, and property specification. We explain and relate the main algorithms used and describe systems based on them. We also give examples of the successful applications of model checking to protocol standards. Finally, we provide an outlook on the field: What is possible with the state of the art and what are the future challenges
Analyzing the User Interface of Android Apps
Get PDFWhen interacting with Android apps, users may not always get what they expect. For instance, when clicking on a button labeled “upload picture”, the app may actually leak the user location while uploading photos to a cloud service. In this paper we present BACKSTAGE, a static analysis framework that binds UI elements to their corresponding callbacks, and further extracts actions, in the form of Android sensitive API calls, that may be triggered by events on such UI elements. We illustrate how the analysis implemented by BACKSTAGE works, and we compare it with similar frameworks
Precise and Scalable Detection of Double-Fetch Bugs in OS Kernels
Get PDFDuring system call execution, it is common for
operating system kernels to read userspace memory multiple
times (multi-reads). A critical bug may exist if the fetched
userspace memory is subject to change across these reads, i.e.,
a race condition, which is known as a double-fetch bug. Prior
works have attempted to detect these bugs both statically and
dynamically. However, due to their improper assumptions and
imprecise definitions regarding double-fetch bugs, their multiread detection is inherently limited and suffers from significant
false positives and false negatives. For example, their approach
is unable to support device emulation, inter-procedural analysis,
loop handling, etc. More importantly, they completely leave the
task of finding real double-fetch bugs from the haystack of multireads to manual verification, which is expensive if possible at all.
In this paper, we first present a formal and precise definition of
double-fetch bugs and then implement a static analysis system—
DEADLINE—to automatically detect double-fetch bugs in OS
kernels. DEADLINE uses static program analysis techniques
to systematically find multi-reads throughout the kernel and
employs specialized symbolic checking to vet each multi-read for
double-fetch bugs. We apply DEADLINE to Linux and FreeBSD
kernels and find 23 new bugs in Linux and one new bug in
FreeBSD. We further propose four generic strategies to patch and
prevent double-fetch bugs based on our study and the discussion
with kernel maintainers
Connecting Pixels to Privacy and Utility: Automatic Redaction of Private Information in Images
No full textImages convey a broad spectrum of personal information. If such images are shared on social media platforms, this personal information is leaked which conflicts with the privacy of depicted persons. Therefore, we aim for automated approaches to redact such private information and thereby protect privacy of the individual. By conducting a user study we find that obfuscating the image regions related to the private information leads to privacy while retaining utility of the images. Moreover, by varying the size of the regions different privacy-utility trade-offs can be achieved. Our findings argue for a "redaction by segmentation" paradigm. Hence, we propose the first sizable dataset of private images "in the wild" annotated with pixel and instance level labels across a broad range of privacy classes. We present the first model for automatic redaction of diverse private information. It is effective at achieving various privacy-utility trade-offs within 83% of the performance of redactions based on ground-truth annotation
A Symbolic Algorithm for Lazy Synthesis of Eager Strategies
Get PDFWe present an algorithm for solving two-player safety games
that combines a mixed forward/backward search strategy with a symbolic representation of the state space. By combining forward and backward exploration, our algorithm can synthesize strategies that are eager in the sense that they try to prevent progress towards the error states as soon
as possible, whereas standard backwards algorithms often produce permissive solutions that only react when absolutely necessary. We provide experimental results for two new sets of benchmarks, as well as the benchmark set of the Reactive Synthesis Competition (SYNTCOMP) 2017.
The results show that our algorithm in many cases produces more eager strategies than a standard backwards algorithm, and solves a number of benchmarks that are intractable for existing tools. Finally, we observe a connection between our algorithm and a recently proposed algorithm for the synthesis of controllers that are robust against disturbances, pointing to possible future applications
Signatures with Flexible Public Key: Introducing Equivalence Classes for Public Keys
Get PDFWe introduce a new cryptographic primitive called signatures with flexible public key (SFPK). We divide the key space into equivalence classes induced by a relation R. A signer can efficiently change his or her key pair to a different representative of the same class, but without a trapdoor it is hard to distinguish if two public keys are related. Our primitive is motivated by structure-preserving signatures on equivalence classes (SPSEQ), where the partitioning is done on the message space. Therefore, both definitions are complementary and their combination has various applications.
We first show how to efficiently construct static group signatures and
self-blindable certificates by combining the two primitives. When properly instantiated, the result is a group signature scheme that has a shorter signature size than the current state-of-the-art scheme by Libert, Peters, and Yung from Crypto'15, but is secure in the same setting.
In its own right, our primitive has stand-alone applications in the cryptocurrency domain, where it can be seen as a straightforward formalization of so-called stealth addresses. Finally, it can be used to build the first ring signature scheme in the plain model without trusted setup, where signature size depends only sub-linearly on the number of ring members. Thus, solving an open problem stated by Malavolta and Schroeder at ASIACRYPT'2017