Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Segmentations-Leak: Membership Inference Attacks and Defenses in Semantic Image Segmentation
No full textToday's success of state of the art methods for semantic segmentation is driven by large datasets. Data is considered an important asset that needs to be protected, as the collection and annotation of such datasets comes at significant efforts and associated costs. In addition, visual data might contain private or sensitive information, that makes it equally unsuited for public release. Unfortunately, recent work on membership inference in the broader area of adversarial machine learning and inference attacks on machine learning models has shown that even black box classifiers leak information on the dataset that they were trained on. We show that such membership inference attacks can be successfully carried out on complex, state of the art models for semantic segmentation. In order to mitigate the associated risks, we also study a series of defenses against such membership inference attacks and find effective counter measures against the existing risks with little effect on the utility of the segmentation method. Finally, we extensively evaluate our attacks and defenses on a range of relevant real-world datasets: Cityscapes, BDD100K, and Mapillary Vistas
Inclusive GAN: Improving Data and Minority Coverage in Generative Models
No full textGenerative Adversarial Networks (GANs) have brought about rapid progress towards generating photorealistic images. Yet the equitable allocation of their modeling capacity among subgroups has received less attention, which could lead to potential biases against underrepresented minorities if left uncontrolled. In this work, we first formalize the problem of minority inclusion as one of data coverage, and then propose to improve data coverage by harmonizing adversarial training with reconstructive generation. The experiments show that our method outperforms the existing state-of-the-art methods in terms of data coverage on both seen and unseen data. We develop an extension that allows explicit control over the minority subgroups that the model should ensure to include, and validate its effectiveness at little compromise from the overall performance on the entire dataset. Code, models, and supplemental videos are available at https://github.com/ningyu1991/InclusiveGAN.git
AdamMC: A Model Checker for Petri Nets with Transits against Flow-LTL
Get PDFThe correctness of networks is often described in terms of the individual data flow of components instead of their global behavior. In software-defined networks, it is far more convenient to specify the correct behavior of packets than the global behavior of the entire network. Petri nets with transits extend Petri nets and Flow-LTL extends LTL such that the data flows of tokens can be tracked. We present the tool AdamMC as the first model checker for Petri nets with transits against Flow-LTL. We describe how AdamMC can automatically encode concurrent updates of software-defined networks as Petri nets with transits and how common network specifications can be expressed in Flow-LTL. Underlying AdamMC is a reduction to a circuit model checking problem. We introduce a new reduction method that results in tremendous performance improvements compared to a previous prototype. Thereby, AdamMC can handle software-defined networks with up to 82 switches
Realizing Omega-regular Hyperproperties
Get PDFWe study the expressiveness and reactive synthesis problem of HyperQPTL, a logic that specifies omega-regular hyperproperties. HyperQPTL is an extension of linear-time temporal logic (LTL) with explicit trace and propositional quantification and therefore truly combines trace relations and omega-regularity. As such, HyperQPTL can express promptness, which states that there is a common bound on the number of steps up to which an event must have happened. We demonstrate how the HyperQPTL formulation of promptness differs from the type of promptness expressible in the logic Prompt-LTL. Furthermore, we study the realizability problem of HyperQPTL by identifying decidable fragments, where one decidable fragment contains formulas for promptness. We show that, in contrast to the satisfiability problem of HyperQPTL, propositional quantification has an immediate impact on the decidability of the realizability problem. We present a reduction to the realizability problem of HyperLTL, which immediately yields a bounded synthesis procedure. We implemented the synthesis procedure for HyperQPTL in the bounded synthesis tool BoSy. Our experimental results show that a range of arbiter satisfying promptness can be synthesized
Planning in the Browser
Get PDFTraditionally, planning tools are designed as applications that users need to install, taking care of the specificities of their operating system, packages, etc. This often places a significant burden on users, especially due to the academic nature of the software. To remedy this situation, here we propose for planning to jump onto the growing trend of light-weight software use: We demonstrate the possibility to run planning tools directly in the browser. We used the emscripten framework to port Fast Downward into WebAssembly (WASM) code, which allows for in-browser execution at near-native speeds. This allows for in-browser PDDL editing and planner execution without the need for server-side resource management. Moreover, it opens up a host of new possibilities, ranging from the interactive presentation of planning-based analysis to new applications exploiting the availability of planning in browsers to perform user-centric analyses
Deep gaze pooling: Inferring and visually decoding search intents from human gaze fixations
No full textPredicting the target of visual search from human eye fixations (gaze) is a difficult problem with many applications, e.g. in human-computer interaction. While previous work has focused on predicting specific search target instances, we propose the first approach to predict categories and attributes of search intents from gaze data and to visually reconstruct plausible targets. However, state-of-the-art models for categorical recognition, in general, require large amounts of training data, which is prohibitive for gaze data. To address this challenge, we further propose a novel Gaze Pooling Layer that combines gaze information with visual representations from Deep Learning approaches. Our scheme incorporates both spatial and temporal aspects of human gaze behavior as well as the appearance of the fixated locations. We propose an experimental setup and novel dataset and demonstrate the effectiveness of our method for gaze-based search target prediction and reconstruction. We highlight several practical advantages of our approach, such as compatibility with existing architectures, no need for gaze training data, and robustness to noise from common gaze sources
MAC-in-the-Box: Verifying a Minimalistic Hardware Design for MAC Computation
Get PDFWe study the verification of security properties at the state machine level of a minimalistic device, called the MAC-in-the-Box (MITB). This device computes a message authentication code based on the SHA-3 hash function and a key that is stored on device, but never output directly. It is designed for secure password storage, but may also be used for secure key-exchange and second-factor authentication. We formally verify, in the HOL4 theorem prover, that no outside observer can distinguish this device from an ideal functionality that provides only access to a hashing oracle. Furthermore, we propose protocols for the MITB’s use in password storage, key-exchange and second-factor authentication, and formally show that it improves resistance against host-compromise in these three application scenarios
What is Normal, What is Strange, and What is Missing in an Knowledge Graph
Get PDFKnowledge graphs (KGs) store highly heterogeneous information about the world in the structure of a graph, and are useful for tasks such as question answering and reasoning. However, they often contain errors and are missing information. Vibrant research in KG refinement has worked to resolve these issues, tailoring techniques to either detect specific types of errors or complete a KG.
In this work, we introduce a \textit{unified solution} to KG characterization by formulating the problem as \emph{unsupervised KG summarization} with a set of inductive, \textit{soft rules}, which describe what is \emph{normal} in a KG, and thus can be used to identify what is \emph{abnormal}, whether it be strange or missing. Unlike first-order logic rules, our rules are labeled, rooted graphs, i.e., patterns that describe the expected neighborhood around a (seen or unseen) node, based on its type and information in the KG. Stepping away from the traditional support/confidence-based rule mining techniques, we propose \method, \emph{Knowledge Graph Inductive SummarizaTion}, which learns a summary of inductive rules that best compress the KG according to the Minimum Description Length principle---a formulation that we are the first to use in the context of KG rule mining. We apply our rules to three large KGs (\NELL{}, \DBpedia{}, and \Yago{}), and tasks such as compression, various types of error detection, and identification of incomplete information. We show that \method outperforms task-specific, supervised and unsupervised baselines in error detection and incompleteness identification, (identifying the location of up to 93\% of missing entities---over 10\% more than baselines), while also being efficient for large knowledge graphs
Candidate iO from Homomorphic Encryption Schemes
Get PDFWe propose a new approach to construct general-purpose indistinguishability obfuscation
(iO). Our construction is obtained via a new intermediate primitive that we call split fullyhomomorphic encryption (split FHE), which we show to be sufficient for constructing iO.
Specifically, split FHE is FHE where decryption takes the following two-step syntactic form:
(i) A secret decryption step uses the secret key and produces a hint which is (asymptotically)
shorter than the length of the encrypted message, and (ii) a public decryption step that only
requires the ciphertext and the previously generated hint (and not the entire secret key),
and recovers the encrypted message. In terms of security, the hints for a set of ciphertexts
should not allow one to violate semantic security for any other ciphertexts.
Next, we show a generic candidate construction of split FHE based on three building
blocks: (i) A standard FHE scheme with linear decrypt-and-multiply (which can be instantiated with essentially all LWE-based constructions), (ii) a linearly homomorphic encryption
scheme with short decryption hints (such as the Damg˚ard-Jurik encryption scheme, based
on the DCR problem), and (iii) a cryptographic hash function (which can be based on a variety of standard assumptions). Our approach is heuristic in the sense that our construction
is not provably secure and makes implicit assumptions about the interplay between these
underlying primitives. We show evidence that this construction is secure by providing an
argument in an appropriately defined oracle model.
We view our construction as a big departure from the state-of-the-art constructions, and
it is in fact quite simple
Simulating Strong Practical Proof Systems with Extended Resolution
No full textProof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution—introduced by Tseitin in the sixties—allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extended-resolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that — from the viewpoint of proof complexity — these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show how Kullmann’s proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems