Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
DPIFuzz: A Differential Fuzzing Frameworkto Detect DPI Elusion Strategies for QUIC
Get PDFQUIC is an emerging transport protocol that has the potential to replace TCP in the near future.
As such, QUIC will become an important target for Deep Packet Inspection (DPI). Reliable DPI is essential, e.g., for corporate environments, to monitor traffic entering and leaving their networks. However, elusion strategies threaten the validity of DPI systems, as they allow attackers to carefully design traffic to fool and thus evade on-path DPI systems. While such elusion strategies for TCP are well documented, it is unclear if attackers will be able to elude QUIC-based DPI systems. In this paper, we systematically explore elusion methodologies for QUIC. To this end, we present DPIFuzz: a differential fuzzing framework which can automatically detect strategies to elude stateful DPI systems for QUIC. We use DPIFuzz to generate and mutate QUIC streams in order to compare (and find differences in) the server-side interpretations of five popular open-source QUIC implementations. We show that DPIFuzz successfully reveals DPI elusion strategies, such as using packets with duplicate packet numbers or exploiting the diverging handling of overlapping stream offsets by QUIC implementations. DPIFuzz additionally finds four security-critical vulnerabilities in these QUIC implementations
Incompressibility of H-Free Edge Modification Problems: Towards a Dichotomy
Get PDFGiven a graph G and an integer k, the H-free Edge Editing problem is to find whether there exist at most k pairs of vertices in G such that changing the adjacency of the pairs in G results in a graph without any induced copy of H. The existence of polynomial kernels for H-free Edge Editing (that is, whether it is possible to reduce the size of the instance to k^O(1) in polynomial time) received significant attention in the parameterized complexity literature. Nontrivial polynomial kernels are known to exist for some graphs H with at most 4 vertices (e.g., path on 3 or 4 vertices, diamond, paw), but starting from 5 vertices, polynomial kernels are known only if H is either complete or empty. This suggests the conjecture that there is no other H with at least 5 vertices were H-free Edge Editing admits a polynomial kernel. Towards this goal, we obtain a set ℋ of nine 5-vertex graphs such that if for every H ∈ ℋ, H-free Edge Editing is incompressible and the complexity assumption NP ⊈ coNP/poly holds, then H-free Edge Editing is incompressible for every graph H with at least five vertices that is neither complete nor empty. That is, proving incompressibility for these nine graphs would give a complete classification of the kernelization complexity of H-free Edge Editing for every H with at least 5 vertices. We obtain similar result also for H-free Edge Deletion. Here the picture is more complicated due to the existence of another infinite family of graphs H where the problem is trivial (graphs with exactly one edge). We obtain a larger set ℋ of nineteen graphs whose incompressibility would give a complete classification of the kernelization complexity of H-free Edge Deletion for every graph H with at least 5 vertices. Analogous results follow also for the H-free Edge Completion problem by simple complementation
Probabilistic Hyperproperties of Markov Decision Processes
Get PDFHyperproperties are properties that describe the correctness of a system as a relation between multiple executions. Hyperproperties generalize trace properties and include information-flow security requirements, like noninterference, as well as requirements like symmetry, partial observation, robustness, and fault tolerance. We initiate the study of the specification and verification of hyperproperties of Markov decision processes (MDPs). We introduce the temporal logic PHL (Probabilistic Hyper Logic), which extends classic probabilistic logics with quantification over schedulers and traces. PHL can express a wide range of hyperproperties for probabilistic systems, including both classical applications, such as probabilistic noninterference, and novel applications in areas such as
robotics and planning. While the model checking problem for PHL is in
general undecidable, we provide methods both for proving and for refuting
formulas from a fragment of the logic. The fragment includes many
probabilistic hyperproperties of interest
Assume, Guarantee or Repair
Get PDFWe present Assume-Guarantee-Repair (AGR) – a novel framework which not only verifies that a program satisfies a set of properties, but also repairs the program in case the verification fails. We consider communicating programs – these are simple C-like programs, extended with synchronous communication actions over communication channels. Our method, which consists of a learning-based approach to assume-guarantee reasoning, performs verification and repair simultaneously. In every iteration, AGR either makes another step towards proving that the (current) system satisfies the specification, or alters the system in a way that brings it closer to satisfying the specification. We manage handling infinite-state systems by using a finite abstract representation, and reduce the semantic problems in hand – satisfying complex specifications that also contain first-order constraints – to syntactic ones, namely membership and equivalence queries for regular languages. We implemented our algorithm and evaluated it on various examples. Our experiments present compact proofs of correctness and quick repairs
A Combinatorial Approach to Quantum Random Functions
Get PDFQuantum pseudorandom functions (QPRFs) extend the classical security of a PRF by allowing the adversary to issue queries on input superpositions. Zhandry [Zhandry, FOCS 2012] showed a separation between the two notions and proved that common construction paradigms are also quantum secure, albeit with a new ad-hoc analysis. In this work we revisit the question of constructing QPRFs and propose a new method starting from small-domain (classical) PRFs: At the heart of our approach is a new domain-extension technique based on bipartite expanders. Interestingly, our analysis is almost entirely classical.
As a corollary of our main theorem, we obtain the first (approximate) key-homomorphic quantum PRF based on the quantum intractability of the learning with errors problem
Controller Synthesis for Hyperproperties
No full textWe investigate the problem of controller synthesis for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple execution traces. Hyperproperties can elegantly express information-flow policies like noninterference and observational determinism. The controller synthesis problem is to automatically design a controller for a plant that ensures satisfaction of a given specification in the presence of the environment or adversarial actions. We show that the controller synthesis problem is decidable for HyperLTL specifications and finite-state plants. We provide a rigorous complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general graphs
xOSSig: Leveraging OS Diversity to Automatically Extract Malware Code Signatures
Get PDFWe present an automated approach to extract code signatures that serve as the forensic fingerprint of a given malware program. Our high-level idea is to compare the memory contents of a sandbox before and after infection by a malware. To pinpoint the actual memory changes caused by the malware, and ignore all others, we use a novel concept called Cross OS Execution. That is, we execute a malware program on multiple different but compatible operating systems (OSes) to identify its memory commonalities, while neglecting OS-specific noise. The commonalities of the dumps therefore contain patterns whose presence is the consequence of executing the malware, i.e., the forensic fingerprint of the malware. We show that we can use two different versions Windows to accurately extract fingerprints of all 17 popular Windows malware families in our test set. These signatures serve to re-identify malware infections in memory dumps with a TPR of 93% and an FPR of 0.15%
Heaps’n’Leaks: How Heap Snapshots Improve Android Taint Analysis
Get PDFThe assessment of information flows is an essential part of analyzing Android apps, and is frequently supported by static taint analysis. Its precision, however, can suffer from the analysis not being able to precisely determine what elements a pointer can (and can not) point to. Recent advances in static analysis suggest that incorporating dynamic heap snapshots, taken at one point at runtime, can significantly improve general static analysis. In this paper, we investigate to what extent this also holds for taint analysis, and how various design decisions, such as when and how many snapshots are collected during execution, and how exactly they are used, impact soundness and precision. We have extended FlowDroid to incorporate heap snapshots, yielding our prototype Heapster, and evaluated it on DroidMacroBench, a novel benchmark comprising real-world Android apps that we also make available as an artifact. The results show (1) the use of heap snapshots lowers analysis time and memory consumption while increasing precision; (2) a very good trade-off between precision and recall is achieved by a mixed-mode in which the analysis falls back to static points-to relations for objects for which no dynamic data was recorded; and (3) while a single heap snapshot (ideally taken at the end of the execution)suffices to improve performance and precision, a better trade-off can be obtained by using multiple snapshots
LEAF: A Faster Secure Search Algorithm via Localization, Extraction, and Reconstruction
Get PDFSecure search looks for and retrieves records from a (possibly cloudhosted) encrypted database while ensuring the confidentiality of
the queries. Researchers are paying increasing attention to secure
search in recent years due to the growing concerns about database
privacy. However, the low efficiency of (especially multiplicative)
homomorphic operations in secure search has hindered its deployment in practice. To address this issue, Akavia et al. [CCS 2018, PETS
2019] proposed new protocols that bring down the number of multiplications in the search algorithm from ????(????
2
) to ????(???? log2 ????), and
then to ????(???? log????), where ???? is the size of the database. In this paper,
we present the first secure search protocol – LEAF and its variant
LEAF+– which only requires ????(????) multiplications. Specifically, at
the core of LEAF are three novel methods we propose, referred to
as Localization, Extraction, and Reconstruction. In addition, LEAF
enjoys low communication complexity and only requires the client
to perform decryption, which adds its advantage in deployment on
weak-power devices such as mobile phones