Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Efficient Non-Interactive Zero-Knowledge Proofs in Cross-Domains without Trusted Setup
No full textWith the recent emergence of efficient zero-knowledge (ZK) proofs for general circuits, while efficient zero-knowledge proofs of algebraic statements have existed for decades, a natural challenge arose to combine algebraic and non-algebraic statements. Chase et al. (CRYPTO 2016) proposed an interactive ZK proof system for this cross-domain problem. As a use case they show that their system can be used to prove knowledge of a RSA/DSA signature on a message m with respect to a publicly known Pedersen commitment g^m h^r . One drawback of their system is that it requires interaction between the prover and the verifier. This is due to the interactive nature of garbled circuits, which are used in their construction. Subsequently, Agrawal et al. (CRYPTO 2018) proposed an efficient non-interactive ZK (NIZK) proof system for cross-domains based on SNARKs, which however require a trusted setup assumption.
In this paper, we propose a NIZK proof system for cross-domains that requires no trusted setup and is efficient both for the prover and the verifier. Our system constitutes a combination of Schnorr based ZK proofs and ZK proofs for general circuits by Giacomelli et al. (USENIX 2016). The proof size and the running time of our system are comparable to the approach by Chase et al. Compared to Bulletproofs (SP 2018), a recent NIZK proofs system on committed inputs, our techniques achieve asymptotically better performance on prover and verifier, thus presenting a different trade-off between the proof size and the running time
Short Text, Large Effect: Measuring the Impact of User Reviews on Android App Security & Privacy
Get PDFApplication markets streamline the end-users' task of finding and installing applications. They also form an immediate communication channel between app developers and their end-users in form of app reviews, which allow users to provide developers feedback on their apps. However, it is unclear to which extent users employ this channel to point out their security and privacy concerns about apps, about which aspects of apps users express concerns, and how developers react to such security- and privacy-related reviews. In this paper, we present the first study of the relationship between end-user reviews and security- & privacy-related changes in apps. Using natural language processing on 4.5M user reviews for the top 2,583 apps in Google Play, we identified 5,527 security and privacy relevant reviews (SPR). For each app version mentioned in the SPR, we use static code analysis to extract permission-protected features mentioned in the reviews. We successfully mapped SPRs to privacy-related changes in app updates in 60.77% of all cases. Using exploratory data analysis and regression analysis we are able to show that preceding SPR are a significant factor for predicting privacy-related app updates, indicating that user reviews in fact lead to privacy improvements of apps. Our results further show that apps that adopt runtime permissions receive a significantly higher number of SPR, showing that runtime permissions put privacy-jeopardizing actions better into users' minds. Further, we can attribute about half of all privacy-relevant app changes exclusively to third-party library code. This hints at larger problems for app developers to adhere to users' privacy expectations and markets' privacy regulations. Our results make a call for action to make app behavior more transparent to users in order to leverage their reviews in creating incentives for developers to adhere to security and privacy best practices, while our results call at the same time for better tools to support app developers in this endeavor
DroidCap: OS Support for Capability-based Permissions in Android
Get PDFWe present DroidCap, a retrofitting of Android’s central Binder IPC mechanism to change the way how permissions are being represented and managed in the system. In DroidCap, permissions are per-process Binder object capabilities. DroidCap's design removes Android’s UID-based ambient authority and allows the delegation of capabilities between processes to create least-privileged protection domains efficiently. With DroidCap, we show that object capabilities as underlying access control model integrates naturally and backward-compatible into Android’s stock permission model and application management. Thus, our Binder capabilities provide app developers with a new path to gradually adopting app compartmentalization, which we showcase at two favorite examples from the literature, privilege separated advertisement libraries and least privileged app components
Stellungnahme gegenüber dem Landtag des Saarlandes in der Anhörung zur Drucksache 16/761 „Informationssicherheitsgesetz Saarland – IT-SiG SL“ sowie Änderung weiterer Vorschriften
Get PDFContinuous Non-Malleable Codes in the 8-Split-State Model
Get PDFNon-malleable codes (NMCs), introduced by Dziembowski, Pietrzak and Wichs [20], provide a useful message integrity guarantee in situations where traditional error-correction (and even error-detection) is impossible; for example, when the attacker can completely overwrite the encoded message. NMCs have emerged as a fundamental object at the intersection of coding theory and cryptography. In particular, progress in the study of non-malleable codes and the related notion of non-malleable extractors has led to new insights and progress on even more fundamental problems like the construction of multi-source randomness extractors. A large body of the recent work has focused on various constructions of non-malleable codes in the split-state model. Many variants of NMCs have been introduced in the literature, e.g., strong NMCs, super strong NMCs and continuous NMCs. The most general, and hence also the most useful notion among these is that of continuous non-malleable codes, that allows for continuous tampering by the adversary. We present the first efficient information-theoretically secure continuously non-malleable code in the constant split-state model. We believe that our main technical result could be of independent interest and some of the ideas could in future be used to make progress on other related questions
Seems Legit: Automated Analysis of Subtle Attacks on Protocols that use Signatures
Get PDFThe standard definition of security for digital signatures—existential unforgeability—does not ensure certain properties that protocol designers might expect. For example, in many modern signature schemes, one signature may verify against multiple different public keys. It is left to protocol designers to ensure that these properties
do not break protocol security goals, often without success.
Modern automated protocol analysis tools are able to prove the absence of large classes of attacks on complex real-world protocols such as TLS 1.3 and 5G. However, their abstraction of signatures assumes much more than existential unforgeability, thereby missing several classes of practical attacks.
We give a hierarchy of new symbolic models for signature schemes that captures these subtleties, and thereby allows us to analyse (often unexpected) behaviours of real-world protocols that were previously out of reach of symbolic analysis. We implement our models in the Tamarin Prover, yielding the first way to perform these analyses automatically, and validate them on several case studies. In the process, we find new attacks on DRKey and SOAP’s WS-Security, both protocols which were previously proven secure
in traditional symbolic models
Towards Reverse-Engineering Black-Box Neural Networks
No full textMuch progress in interpretable AI is built around scenarios where the user, one who interprets the model, has a full ownership of the model to be diagnosed. The user either owns the training data and computing resources to train an interpretable model herself or owns a full access to an already trained model to be interpreted post-hoc. In this chapter, we consider a less investigated scenario of diagnosing black-box neural networks, where the user can only send queries and read off outputs. Black-box access is a common deployment mode for many public and commercial models, since internal details, such as architecture, optimisation procedure, and training data, can be proprietary and aggravate their vulnerability to attacks like adversarial examples. We propose a method for exposing internals of black-box models and show that the method is surprisingly effective at inferring a diverse set of internal information. We further show how the exposed internals can be exploited to strengthen adversarial examples against the model. Our work starts an important discussion on the security implications of diagnosing deployed models with limited accessibility. The code is available at goo.gl/MbYfsv
Synthesizing functional reactive programs
Get PDFFunctional Reactive Programming (FRP) is a paradigm that
has simplified the construction of reactive programs. There
are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows.
However, finding a good control flow, that correctly manages
state and switches behaviors at the right times, still poses a
major challenge to developers.
An attractive alternative is specifying the behavior instead
of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has
not been explored so far how Control Flow Models (CFMs),
resulting from TSL synthesis, are turned into executable code
that is compatible with libraries building on FRP. We bridge
this gap, by showing that CFMs are a suitable formalism to
be turned into Applicative, Monadic, and Arrowized FRP.
We demonstrate the effectiveness of our translations on a
real-world kitchen timer application, which we translate to a
desktop application using the Arrowized FRP library Yampa, a
web application using the Monadic Threepenny-GUI library,
and to hardware using the Applicative hardware description
language ClaSH
Approximate Automata for Omega-Regular Languages
Get PDFAutomata over infinite words, also known as omega-automata, play a key role in the verification and synthesis of reactive systems. The spectrum of omega-automata is defined by two characteristics: the acceptance condition (e.g. Büchi or parity) and the determinism (e.g., deterministic or nondeterministic) of an automaton. These characteristics play a crucial role in applications of automata theory. For example, certain acceptance conditions can be handled more efficiently than others by dedicated tools and algorithms. Furthermore, some applications, such as synthesis and probabilistic model checking, require that properties are represented as some type of deterministic omega-automata. However, properties cannot always be represented by automata with the desired acceptance condition and determinism. In this paper we study the problem of approximating linear-time properties by automata in a given class. Our approximation is based on preserving the language up to a user-defined precision given in terms of the size of the finite lasso representation of infinite executions that are preserved. We study the state complexity of different types of approximating automata, and provide constructions for the approximation within different automata classes, for example, for approximating a given automaton by one with a simpler acceptance condition
The Fuzzing Book
No full textSoftware has bugs, and catching bugs can involve lots of effort. This book addresses this problem by automating software testing, specifically by generating tests automatically. Recent years have seen the development of novel techniques that lead to dramatic improvements in test generation and software testing. They now are mature enough to be assembled in a book – even with executable code