Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Model Checking Data Flows in Concurrent Network Updates
Get PDFWe present a model checking approach for the verification of data flow correctness in networks during concurrent updates of the network configuration. This verification problem is of great importance for software-defined networking (SDN), where errors can lead to packet loss, black holes, and security violations. Our approach is based on a specification of temporal properties of individual data flows, such as the requirement that the flow is free of cycles. We check whether these properties are simultaneously satisfied for all active data flows while the network configuration is updated. To represent the behavior of the concurrent network controllers and the resulting evolutions of the configurations, we introduce an extension of Petri nets with a transit relation, which characterizes the data flow caused by each transition of the Petri net. For safe Petri nets with transits, we reduce the verification of temporal flow properties to a circuit model checking problem that can be solved with effective verification techniques like IC3, interpolation, and bounded model checking. We report on encouraging experiments with a prototype implementation based on the hardware model checker ABC
How to Prove Your Model Belongs to You: A Blind-Watermark based Framework to Protect Intellectual Property of DNN
Get PDFDeep learning techniques have made tremendous progress in a variety of challenging tasks, such as image recognition and machine translation, during the past decade. Training deep neural networks is computationally expensive and requires both human and intellectual resources. Therefore, it is necessary to protect the intellectual property of the model and externally verify the ownership of the model. However, previous studies either fail to defend against the evasion attack or have not explicitly dealt with fraudulent claims of ownership by adversaries. Furthermore, they can not establish a clear association between the model and the creator’s identity.
To fill these gaps, in this paper, we propose a novel intellectual
property protection (IPP) framework based on blind-watermark for watermarking deep neural networks that meet the requirements of security and feasibility. Our framework accepts ordinary samples and the exclusive logo as inputs, outputting newly generated samples as watermarks, which are almost indistinguishable from the origin, and infuses these watermarks into DNN models by assigning specific labels, leaving the backdoor as the basis for our copyright claim. We evaluated our IPP framework on two benchmark datasets and 15 popular deep learning models. The results show that our framework successfully verifies the ownership of all the models without a noticeable impact on their primary task. Most importantly, we are the first to successfully design and implement a blind-watermark based framework, which can achieve state-of-art performances on undetectability against evasion attack and unforgeability against fraudulent claims of ownership. Further, our framework shows remarkable robustness and establishes a clear association between the model and the author’s identity
Fashion is Taking Shape: Understanding Clothing Preference Based on Body Shape From Online Sources
Get PDFTo study the correlation between clothing garments and
body shape, we collected a new dataset (Fashion Takes
Shape), which includes images of female users with clothing
category annotations. Despite the progress in body shape
estimation from images, it turns out to be challenging to infer
body shape from such diverse, real-world photos. Hence, we
propose a novel and robust multi-photo approach to estimate
body shapes of each user and build a conditional model of
clothing categories given body-shape. We demonstrate that
in real-world data, clothing categories and body-shapes are
correlated and show that our multi-photo approach leads to
a better predictive model for clothing categories compared
to models based on single-view shape estimates or manually
annotated body types. We see our method as the first step towards the large-scale understanding of clothing preferences
from body shape
Incremental Proofs of Sequential Work
Get PDFA proof of sequential work allows a prover to convince a verifier that a certain amount of sequential
steps have been computed. In this work we introduce the notion of incremental proofs of sequential work where a
prover can carry on the computation done by the previous prover incrementally, without affecting the resources of
the individual provers or the size of the proofs.
To date, the most efficient instance of proofs of sequential work [Cohen and Pietrzak, Eurocrypt 2018] for N steps
require the prover to have √
N memory and to run for N +
√
N steps. Using incremental proofs of sequential work
we can bring down the prover’s storage complexity to log N and its running time to N.
We propose two different constructions of incremental proofs of sequential work: Our first scheme requires a single
processor and introduces a poly-logarithmic factor in the proof size when compared with the proposals of Cohen and
Pietrzak. Our second scheme assumes log N parallel processors but brings down the overhead of the proof size to a
factor of 9. Both schemes are simple to implement and only rely on hash functions (modelled as random oracles)
JStap: A Static Pre-Filter for Malicious JavaScript Detection
Get PDFGiven the success of the Web platform, attackers have abused its main programming language, namely JavaScript, to mount different types of attacks on their victims. Due to the large volume of such malicious scripts, detection systems rely on static analyses to quickly process the vast majority of samples. These static approaches are not infallible though and lead to misclassifications. Also, they lack semantic information to go beyond purely syntactic approaches. In this paper, we propose JStap, a modular static JavaScript detection system, which extends the detection capability of existing lexical and AST-based pipelines by also leveraging control and data flow information. Our detector is composed of ten modules, including five different ways of abstracting code, with differing levels of context and semantic information, and two ways of extracting features. Based on the frequency of these specific patterns, we train a random forest classifier for each module. In practice, JStap outperforms existing systems, which we reimplemented and tested on our dataset totaling over 270,000 samples. To improve the detection, we also combine the predictions of several modules. A first layer of unanimous voting classifies 93% of our dataset with an accuracy of 99.73%, while a second layer--based on an alternative modules' combination--labels another 6.5% of our initial dataset with an accuracy over 99%. This way, JStap can be used as a precise pre-filter, meaning that it would only need to forward less than 1% of samples to additional analyses. For reproducibility and direct deployability of our modules, we make our system publicly available (https://github.com/Aurore54F/JStap)
Membership Privacy for Fully Dynamic Group Signatures
Get PDFGroup signatures present a compromise between the traditional goals of digital
signatures and the need for signer privacy, allowing for the creation of
unforgeable signatures in the name of a group which reveal nothing about the
actual signer's identity beyond their group membership. An important
consideration that is absent in prevalent models is that group membership itself
may be sensitive information, especially if group membership is dynamic, i.e.
membership status may change over time.
We address this issue by introducing formal notions of membership privacy for
fully dynamic group signature schemes, which can be easily integrated into the
most expressive models of group signature security to date. We then propose a
generic construction for a fully dynamic group signature scheme with membership
privacy that is based on signatures with flexible public key (SFPK) and
signatures on equivalence classes (SPSEQ).
Finally, we devise novel techniques for SFPK to construct a highly efficient
standard model scheme (i.e. without random oracles) that provides shorter
signatures than even the non-private state-of-the-art from standard assumptions.
This shows that, although the strictly stronger security notions we introduce
have been completely unexplored in the study of fully dynamic group signatures
so far, they do not come at an additional cost in practice
Language in Our Time: An Empirical Analysis of Hashtags
Get PDFHashtags in online social networks have gained tremendous popularity during the past five years. The resulting large quantity of
data has provided a new lens into modern society. Previously, researchers mainly rely on data collected from Twitter to study either
a certain type of hashtags or a certain property of hashtags. In this
paper, we perform the first large-scale empirical analysis of hashtags shared on Instagram, the major platform for hashtag-sharing.
We study hashtags from three different dimensions including the
temporal-spatial dimension, the semantic dimension, and the social
dimension. Extensive experiments performed on three large-scale
datasets with more than 7 million hashtags in total provide a series of interesting observations. First, we show that the temporal
patterns of hashtags can be categorized into four different clusters, and people tend to share fewer hashtags at certain places and
more hashtags at others. Second, we observe that a non-negligible
proportion of hashtags exhibit large semantic displacement. We
demonstrate hashtags that are more uniformly shared among users,
as quantified by the proposed hashtag entropy, are less prone to
semantic displacement. In the end, we propose a bipartite graph
embedding model to summarize users’ hashtag profiles, and rely
on these profiles to perform friendship prediction. Evaluation results show that our approach achieves an effective prediction with
AUC (area under the ROC curve) above 0.8 which demonstrates the
strong social signals possessed in hashtags
Towards Automated Network Mitigation Analysis
Get PDFPenetration testing is a well-established practical concept for the identification of potentially exploitable security weaknesses and an important component of a security audit. Providing a holistic security assessment for networks consisting of several hundreds hosts is hardly feasible though without some sort of mechanization. Mitigation, prioritizing counter-measures subject to a given budget, currently lacks a solid theoretical understanding and is hence more art than science. In this work, we propose the first approach for conducting comprehensive what-if analyses in order to reason about mitigation in a conceptually well-founded manner. To evaluate and compare mitigation strategies, we use simulated penetration testing, i.e., automated attack-finding, based on a network model to which a subset of a given set of mitigation actions, e.g., changes to the network topology, system updates, configuration changes etc. is applied. Using Stackelberg planning, we determine optimal combinations that minimize the maximal attacker success (similar to a Stackelberg game), and thus provide a well-founded basis for a holistic mitigation strategy. We show that these Stackelberg planning models can largely be derived from network scan, public vulnerability databases and manual inspection with various degrees of automation and detail, and we simulate mitigation analysis on networks of different size and vulnerability
Towards Automated Network Mitigation Analysis (extended version)
Get PDFPenetration testing is a well-established practical concept for the identification of potentially exploitable security weaknesses and an important component of a security audit. Providing a holistic security assessment for networks consisting of several hundreds hosts is hardly feasible though without some sort of mechanization. Mitigation, prioritizing counter-measures subject to a given budget, currently lacks a solid theoretical understanding and is hence more art than science. In this work, we propose the first approach for conducting comprehensive what-if analyses in order to reason about mitigation in a conceptually well-founded manner. To evaluate and compare mitigation strategies, we use simulated penetration testing, i.e., automated attack-finding, based on a network model to which a subset of a given set of mitigation actions, e.g., changes to the network topology, system updates, configuration changes etc. is applied. Using Stackelberg planning, we determine optimal combinations that minimize the maximal attacker success (similar to a Stackelberg game), and thus provide a well-founded basis for a holistic mitigation strategy. We show that these Stackelberg planning models can largely be derived from network scan, public vulnerability databases and manual inspection with various degrees of automation and detail, and we simulate mitigation analysis on networks of different size and vulnerability
simTPM: User-centric TPM for Mobile Devices
Get PDFTrusted Platform Modules are valuable building blocks for security solutions and have also been recognized as beneficial for security on mobile platforms, like smartphones and tablets. However, strict space, cost, and power constraints of mobile devices prohibit an implementation as dedicated on-board chip and the incumbent implementations are software TPMs protected by Trusted Execution Environments. In this paper, we present simTPM, an alternative implementation of a mobile TPM based on the SIM card available in mobile platforms. We solve the technical challenge of implementing a TPM2.0 in the resource-constrained SIM card environment and integrate our simTPM into the secure boot chain of the ARM Trusted Firmware on a HiKey960 reference board. Most notably, we address the challenge of how a removable TPM can be bound to the host device’s root of trust for measurement. As such, our solution not only provides a mobile TPM that avoids additional hardware while using a dedicated, strongly protected environment, but also offers promising synergies with co-existing TEE-based TPMs. In particular, simTPM offers a user-centric trusted module. Using performance benchmarks, we show that our simTPM has competitive speed with a reported TEE-based TPM and a hardware-based TPM