Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Improving Automated Symbolic Analysis of Ballot Secrecy for E-voting Protocols: A Method Based on Sufficient Conditions
Get PDFWe advance the state-of-the-art in automated symbolic analysis for e-voting protocols by introducing three conditions that together are sufficient to guarantee ballot secrecy. There are two main advantages to using our conditions, compared to existing automated approaches. The first is a substantial expansion of the class of protocols and threat models that can be automatically analysed: we can systematically deal with (a) honest authorities present in different phases, (b) threat models in which no dishonest voters occur, and (c) protocols whose ballot secrecy depends on fresh data coming from other phases. The second advantage is that it can significantly improve verification efficiency, as the individual conditions are often simpler to verify. E.g., for the LEE protocol, we obtain a speedup of over two orders of magnitude. We show the scope and effectiveness of our approach using ProVerif in several case studies, including FOO, LEE, JCJ, and Belenios. In these case studies, our approach does not yield any false attacks, suggesting that our conditions are tight
ConfLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code
No full textWe present a compiler-based scheme for protecting the confidentiality of sensitive data in low-level applications (e.g. those written in C) in the presence of an active adversary. In our scheme, the programmer marks sensitive data by writing lightweight annotations on the top-level definitions in the source code. The compiler then uses a combination of static dataflow analysis and runtime instrumentation to prevent data leaks even in the presence of low-level attacks. To reduce runtime overheads, the compiler uses a novel memory layout and a taint-aware form of control flow integrity. We formalize our scheme and prove its security. We have also implemented our scheme within the LLVM compiler and evaluated it on the CPU-intensive SPEC micro-benchmarks, and on larger, real-world applications, including the NGINX webserver and the OpenLDAP directory server. We find that performance overheads introduced by our instrumentation are moderate (average 12% on SPEC), and the programmer effort to port the applications is minimal
Efficient Information-Flow Verification under Speculative Execution
Get PDFWe study the formal verification of information-flow properties in the presence of speculative execution and side-channels. First, we present a formal model of speculative execution semantics. This model can be parameterized by the depth of speculative execution and is amenable to a range of verification techniques. Second, we introduce a novel notion of information leakage under speculation, which is parameterized by the information that is available to an attacker through side-channels. Finally, we present one verification technique that uses our formalism and can be used to detect information leaks under speculation through cache side-channels, and can decide whether these are only possible under speculative execution. We implemented an instance of this verification technique that combines taint analysis and safety model checking.
We evaluated this approach on a range of examples that have been proposed as benchmarks for mitigations of the Spectre vulnerability, and show that our approach correctly
identifies all information leaks
Leveraging Linear Decryption: Rate-1 Fully-Homomorphic Encryption and Time-Lock Puzzles
Get PDFWe show how to combine a fully-homomorphic encryption scheme with linear decryption and a
linearly-homomorphic encryption schemes to obtain constructions with new properties. Specifically,
we present the following new results.
(1) Rate-1 Fully-Homomorphic Encryption: We construct the first scheme with message-to-ciphertext
length ratio (i.e., rate) 1 − σ for σ = o(1). Our scheme is based on the hardness of the Learning
with Errors (LWE) problem and σ is proportional to the noise-to-modulus ratio of the assumption.
Our building block is a construction of a new high-rate linearly-homomorphic encryption.
One application of this result is the first general-purpose secure function evaluation protocol in the
preprocessing model where the communication complexity is within additive factor of the optimal
insecure protocol.
(2) Fully-Homomorphic Time-Lock Puzzles: We construct the first time-lock puzzle where one can
evaluate any function over a set of puzzles without solving them, from standard assumptions. Prior
work required the existence of sub-exponentially hard indistinguishability obfuscation
Truth Assignments as Conditional Autarkies
No full textAn autarky for a formula in propositional logic is a truth assignment that satisfies every clause it touches, i.e., every clause for which the autarky assigns at least one variable. In this paper, we present how conditional autarkies, a generalization of autarkies, give rise to novel preprocessing techniques for SAT solving. We show that conditional autarkies correspond to a new type of redundant clauses, termed globally-blocked clauses, and that the elimination of these clauses can simulate existing circuit-simplification techniques on the CNF level
Systematically Covering Input Structure
Get PDFGrammar-based testing uses a given grammar to produce syntactically valid inputs. To cover program features, it is necessary to also cover input features - say, all URL variants for a URL parser. Our k-path algorithm for grammar production systematically covers syntactic elements as well as their combinations. In our evaluation, we show that this results in a significantly higher code coverage than state of the art
Parameterized synthesis of self-stabilizing protocols in symmetric networks
Get PDFSelf-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric networks, including ring, line, mesh, and torus. First, we develop cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimate states. We also develop a sufficient condition for convergence in self-stabilizing systems. Since some of our cutoffs grow with the size of the local state space of processes, scalability of the synthesis procedure is still a problem. We address this problem by introducing a novel SMT-based technique for counterexample-guided synthesis of self-stabilizing algorithms in symmetric networks. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems for ring and line topologies
Don’t Trust The Locals: Investigating the Prevalence of Persistent Client-Side Cross-Site Scripting in the Wild.
Get PDFThe Web has become highly interactive and an
important driver for modern life, enabling information retrieval,
social exchange, and online shopping. From the security perspective, Cross-Site Scripting (XSS) is one of the most nefarious
attacks against Web clients. Research has long since focused
on three categories of XSS: Reflected, Persistent, and DOMbased XSS. In this paper, we argue that our community must
consider at least four important classes of XSS, and present
the first systematic study of the threat of Persistent Client-Side
XSS, caused by the insecure use of client-side storage. While
the existence of this class has been acknowledged, especially by
the non-academic community like OWASP, prior works have
either only found such flaws as side effects of other analyses or
focused on a limited set of applications to analyze. Therefore, the
community lacks in-depth knowledge about the actual prevalence
of Persistent Client-Side XSS in the wild.
To close this research gap, we leverage taint tracking to
identify suspicious flows from client-side persistent storage (Web
Storage, cookies) to dangerous sinks (HTML, JavaScript, and
script.src). We discuss two attacker models capable of
injecting malicious payloads into storage, i.e., a Network Attacker
capable of temporarily hijacking HTTP communication (e.g., in
a public WiFi), and a Web Attacker who can leverage flows into
storage or an existing reflected XSS flaw to persist their payload.
With our taint-aware browser and these models in mind, we
study the prevalence of Persistent Client-Side XSS in the Alexa
Top 5,000 domains. We find that more than 8% of them have
unfiltered data flows from persistent storage to a dangerous sink,
which showcases the developers’ inherent trust in the integrity
of storage content. Even worse, if we only consider sites that
make use of data originating from storage, 21% of the sites are
vulnerable. For those sites with vulnerable flows from storage
to sink, we find that at least 70% are directly exploitable by
our attacker models. Finally, investigating the vulnerable flows
originating from storage allows us to categorize them into four
disjoint categories and propose appropriate mitigations
Detection of Threats to IoT Devices using Scalable VPN-forwarded Honeypots
Get PDFAttacks on Internet of Things (IoT) devices, exploiting inherent vulnerabilities,
have intensified over the last few years. Recent large-scale attacks, such as Persirai, Hakai, etc. corroborate concerns about the security of IoT devices. In this work, we propose an approach that allows easy integration of commercial off-the-shelf IoT devices into a general honeypot architecture. Our approach projects a small number of heterogeneous IoT devices (that are physically at one location) as many (geographically distributed) devices on the Internet, using connections to commercial and private VPN services. The goal is for those devices to be discovered and exploited by
attacks on the Internet, thereby revealing unknown vulnerabilities. For detection and examination of potentially malicious traffic, we devise two analysis strategies: (1) given an outbound connection from honeypot, backtrack into network traffic to detect the corresponding attack command that caused the malicious connection and use it to download malware,
(2) perform live detection of unseen URLs from HTTP requests using adaptive clustering.
We show that our implementation and analysis strategies are able to detect recent large-scale attacks targeting IoT devices (IoT Reaper, Hakai, etc.) with overall low cost and maintenance effort
Adversarial Initialization - when your network performs the way I want -
Get PDFThe increase in computational power and available data has fueled a wide deployment of deep learning in production environments. Despite their successes, deep architectures are still poorly understood and costly to train. We demonstrate in this paper how a simple recipe enables a market player to harm or delay the development of a competing product. Such a threat model is novel and has not been considered so far. We derive the corresponding attacks and show their efficacy both formally and empirically. These attacks only require access to the initial, untrained weights of a network. No knowledge of the problem domain and the data used by the victim is needed. On the initial weights, a mere permutation is sufficient to limit the achieved accuracy to for example 50% on the MNIST dataset or double the needed training time. While we can show straightforward ways to mitigate the attacks, the respective steps are not part of the standard procedure taken by developers so far