Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Towards Plausible Graph Anonymization
Get PDFSocial graphs derived from online social interactions contain a wealth of information that is nowadays extensively used by both industry and academia. However, as social graphs contain sensitive information, they need to be properly anonymized before release. Most of the existing graph anonymization mechanisms rely on the perturbation of the original graph's edge set. In this paper, we identify a fundamental weakness of these mechanisms: They neglect the strong structural proximity between friends in social graphs, thus add implausible fake edges for anonymization.
To exploit this weakness, we first propose a metric to quantify an edge's plausibility by relying on graph embedding. Extensive experiments on three real-life social network datasets demonstrate that our plausibility metric can very effectively differentiate fake edges from original edges with AUC (area under the ROC curve) values above 0.95 in most of the cases. We then rely on a Gaussian mixture model to automatically derive the threshold on the edge plausibility values to determine whether an edge is fake, which enables us to recover to a large extent the original graph from the anonymized graph. We further demonstrate that our graph recovery attack jeopardizes the privacy guarantees provided by the considered graph anonymization mechanisms.
To mitigate this vulnerability, we propose a method to generate fake yet plausible edges given the graph structure and incorporate it into the existing anonymization mechanisms. Our evaluation demonstrates that the enhanced mechanisms decrease the chances of graph recovery, reduce the success of graph de-anonymization (up to 30\%), and provide even better utility than the existing anonymization mechanisms
Automatic Uncovering of Hidden Behaviors from Input Validation in Mobile Apps
Get PDFMobile applications (apps) have exploded in popularity, with billions of smartphone users using millions of apps available through markets such as the Google Play Store or the Apple App Store. While these apps have rich and useful functionality that is publicly exposed to end users, they also contain hidden behaviors that are not disclosed, such as backdoors and blacklists designed to block unwanted content. In this paper, we show that the input validation behavior—the way the mobile apps process and respond to data entered by users—can serve as a powerful tool for uncovering such hidden functionality. We therefore have developed a tool, InputScope, that automatically detects both the execution context of user input validation and also the content involved in the validation, to automatically expose the secrets of interest. We have tested InputScope with over 150,000 mobile apps, including popular apps from major app stores and pre- installed apps shipped with the phone, and found 12,706 mobile apps with backdoor secrets and 4,028 mobile apps containing blacklist secrets
Promptness and Bounded Fairness in Concurrent and Parameterized Systems
Get PDFWe investigate the satisfaction of specifications in Prompt
Linear Temporal Logic (Prompt-LTL) by concurrent systems. Prompt-LTL is an extension of LTL that allows to specify parametric bounds onthe satisfaction of eventualities, thus adding a quantitative aspect to the specification language. We establish a connection between bounded fairness, bounded stutter equivalence, and the satisfaction of Prompt-LTL\X
formulas. Based on this connection, we prove the first cutoff results for different classes of systems with a parametric number of components and quantitative specifications, thereby identifying previously unknown
decidable fragments of the parameterized model checking problem
Stellungnahme zur Anhörung der Enquêtekommission „Digitalisierung im Saarland“ zur wirtschaftlichen Entwicklung im Zuge der Digitalisierung
Get PDFStellungnahme zur Anhörung der Enquêtekommission „Digitalisierung im Saarland“ zur wirtschaftlichen Entwicklung im Zuge der Digitalisierun
Learning Input Tokens for Effective Fuzzing
Get PDFModern fuzzing tools like AFL operate at a lexical level: They explore the input space of tested programs one byte after another. For inputs with complex syntactical properties, this is very inefficient, as keywords and other tokens have to be composed one character at a time. Fuzzers thus allow to specify dictionaries listing possible tokens the input can be composed from; such dictionaries speed up fuzzers dramatically. Also, fuzzers make use of dynamic tainting to track input tokens and infer values that are expected in the input validation phase. Unfortunately, such tokens are usually implicitly converted to program specific values which causes a loss of the taints attached to the input data in the lexical phase.
In this paper we present a technique to extend dynamic tainting to not only track explicit data flows but also taint implicitly converted data without suffering from taint explosion. This extension makes it possible to augment existing techniques and automatically infer a set of tokens and seed inputs for the input language of a program given nothing but the source code. Specifically targeting the lexical analysis of an input processor, our lFuzzer test generator systematically explores branches of the lexical analysis, producing a set of tokens that fully cover all decisions seen. The resulting set of tokens can be directly used as a dictionary for fuzzing. Along with the token extraction seed inputs are generated which give further fuzzing processes a head start. In our experiments, the lFuzzer-AFL combination achieves up to 17% more coverage on complex input formats like JSON, LISP, tinyC, and JavaScript compared to AFL
PMForce: Systematically Analyzing PostMessage Handlers at Scale
Get PDFThe Web has become a platform in which sites rely on intricate interactions that span across the boundaries of origins. While the Same-Origin Policy prevents direct data exchange with documents from other origins, the postMessage API offers one relaxation that allows developers to exchange data across these boundaries. While prior manual analysis could show the presence of issues within postMessage handlers, unfortunately, a steep increase in postMessage usage makes any manual approach intractable.To deal with this increased work load, we set out to automatically find issues in postMessage handlers that allow an attacker to execute code in the vulnerable sites, alter client-side state, or leak sensitive information.
To achieve this goal, we present an automated analysis framework running inside the browser, which uses selective forced execution paired with lightweight dynamic taint tracking to find traces in the analyzed handlers that end in sinks allowing for code-execution or state alterations. We use path constraints extracted from the program traces and augment them with Exploit Templates, i.e., additional constraints, ascertaining that a valid assignment that solves all these constraints produces a code-invoking or state-manipulating behavior. Based on these constraints, we use Z3 to generate postMessages aimed at triggering the insecure functionality to prove exploitability, and validate our findings at scale.
We use this framework to conduct the most comprehensive experiment studying the security issues of postMessage handlers found throughout the top 100,000 most influential sites yet, which allows us to find potentially exploitable data flows in 252 unique handlers out of which 111 were automatically exploitable
How to Build Optimally Secure PRFs Using Block Ciphers
Get PDFIn EUROCRYPT '96, Aiello and Venkatesan proposed two candidates for -bit to -bit pseudorandom functions (PRFs), called Benes and modified Benes (or mBenes), based on -bit to -bit PRFs. While Benes is known to be secure up to queries (Patarin, AFRICACRYPT '08), the security of mBenes has only been proved up to queries for all by Patarin and Montreuil in ICISC '05. In this work, we show that the composition of a -bit hash function with mBenes is a secure variable input length (VIL) PRF up to queries (given appropriate hash function bounds). We extend our analysis with block ciphers as the underlying primitive and obtain two optimally secure VIL PRFs using block ciphers. The first of these candidates requires calls to the block cipher. The second candidate requires just calls to the block cipher, but here the proof is based on Patarin's mirror theory. Further, we instantiate the hash function with a PMAC+/LightMAC+ like hash, to get six candidates for deterministic message authentication codes with optimal security
Simplex Architecture Meets RTLola
Get PDFDesigning controllers for safety-critical cyber-physical systems is a challenging task due to their complex dynamics and only partial access to information. Despite these difficulties, machine learned controllers show remarkable success. Their outstanding performance is tarnished by an opaque structure that prohibits reasoning about their internals. A remedy for this problem is the Simplex architecture. It embeds an arbitrarily complex controller into a verifiable structure that monitors controller decisions. Upon detection of potentially harmful commands, the architecture falls back to a simple and safe controller. While validation of control decisions is easier than finding them, it still has to account for complex temporal dependencies. At the same time, deployment in embedded safety-critical system requires the monitor to be formally verifiable and to cope with strict resource limitations. In this talk we will discuss the monitoring module of the Simplex architecture on the example of an artificial pancreas and propose using the RTLOLA monitoring framework
Dependency-based Compositional Synthesis
Get PDFDespite many recent advances, reactive synthesis is still not really a practical technique. The grand challenge is to scale from small transition systems, where synthesis performs well, to complex multi-component designs. Compositional methods, such as the construction of dominant strategies for individual components, reduce the complexity significantly, but are usually not applicable without extensively rewriting the specification. In this paper, we present a refinement of compositional synthesis that does not require such an intervention. Our algorithm decomposes the system into a sequence of components, such that every component has a strategy that is dominant, i.e., performs at least as good as any possible alternative, provided that the preceding components follow their (already synthesized) strategies. The decomposition of the system is based on a dependency analysis, for which we provide semantic and syntactic techniques. We establish the soundness and completeness of the approach and report on encouraging experimental results
Body Shape Privacy in Images: Understanding Privacy and Preventing Automatic Shape Extraction
No full textModern approaches to pose and body shape estimation have recently achieved strong performance even under challenging real-world conditions. Even from a single image of a clothed person, a realistic looking body shape can be inferred that captures a users' weight group and body shape type well. This opens up a whole spectrum of applications -- in particular in fashion -- where virtual try-on and recommendation systems can make use of these new and automatized cues. However, a realistic depiction of the undressed body is regarded highly private and therefore might not be consented by most people. Hence, we ask if the automatic extraction of such information can be effectively evaded. While adversarial perturbations have been shown to be effective for manipulating the output of machine learning models -- in particular, end-to-end deep learning approaches -- state of the art shape estimation methods are composed of multiple stages. We perform the first investigation of different strategies that can be used to effectively manipulate the automatic shape estimation while preserving the overall appearance of the original image