Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Translating Asynchronous Games for Distributed Synthesis
Get PDFIn distributed synthesis, a set of process implementations is generated, which together, accomplish an objective against all possible behaviors of the environment. A lot of recent work has focussed on systems with causal memory, i.e., sets of asynchronous processes that exchange their causal histories upon synchronization. Decidability results for this problem have been stated either in terms of control games, which extend Zielonka's asynchronous automata by partitioning the actions into controllable and uncontrollable, or in terms of Petri games, which extend Petri nets by partitioning the tokens into system and environment players. The precise connection between these two models was so far, however, an open question.
In this paper, we provide the first formal connection between control games and Petri games. We establish the equivalence of the two game types based on weak bisimulations between their strategies. For both directions, we show that a game of one type can be translated into an equivalent game of the other type. We provide exponential upper and lower bounds for the translations. Our translations allow to transfer and combine decidability results between the two types of games. Exemplarily, we translate decidability in acyclic communication architectures, originally obtained for control games, to Petri games, and decidability in single-process systems, originally obtained for Petri games, to control games
Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications
Get PDFWe present Syntroids, a case study for the automatic synthesis of hardware from a temporal logic specification. Syntroids is a space shooter acarde game realized on an FPGA, where the control flow architecture has been completely specified in Temporal Stream Logic (TSL) and implemented using reactive synthesis. TSL is a recently introduced temporal logic that separates control and data. This leads to scalable synthesis, because the cost of the synthesis process is independent of the complexity of the handled data. In this case study, we report on our experience with the TSL-based development of the Syntroids game and on the implementation quality obtained with synthesis in comparison to manual programming. We also discuss solved and open challenges with respect to currently available synthesis tools
From Law to Engineering: A Computer Science Perspective on Privacy & Data Protection
No full textPrivacy and data protection regulation tries to strike a balance between legitimate data use and the right to personal privacy. Nevertheless, the advances in computer science pose new challenges to this careful balance. Data-driven analytics as well as resulting data use and business models e.g. for machine learning, big data and automated decision-making threaten to make individuals, their behaviour and their decision-making completely transparent and predictable, deepening the power asymmetry between individuals and data controllers.
But the nature of computer science with regards to privacy is Janus-faced. The ever-progressing digitalization also requires digital solutions for effective privacy protection. Computer science can and has to act as an enabler of privacy-friendly data processing.
The role of privacy engineering and privacy-enhancing technologies by far exceeds just guaranteeing legal compliance. In fact, the crucial value of privacy engineering is to lessen the latent conflict arising from this power asymmetry by empowering the individual and building trust by giving technical privacy assurances.
In this chapter, we discuss the core concepts of privacy engineering, provide some examples of the state of the art, and discuss the relation between privacy principles and technical measures
Not Using the Car to See the Sidewalk: Quantifying and Controlling the Effects of Context in Classification and Segmentation
No full textImportance of visual context in scene understanding tasks is well recognized in the computer vision community. However, to what extent the computer vision models for image classification and semantic segmentation are dependent on the context to make their predictions is unclear. A model overly relying on context will fail when encountering objects in context distributions different from training data and hence it is important to identify these dependencies before we can deploy the models in the real-world. We propose a method to quantify the sensitivity of black-box vision models to visual context by editing images to remove selected objects and measuring the response of the target models. We apply this methodology on two tasks, image classification and semantic segmentation, and discover undesirable dependency between objects and context, for example that "sidewalk" segmentation relies heavily on "cars" being present in the image. We propose an object removal based data augmentation solution to mitigate this dependency and increase the robustness of classification and segmentation models to contextual variations. Our experiments show that the proposed data augmentation helps these models improve the performance in out-of-context scenarios, while preserving the performance on regular data
Parser-Directed Fuzzing
Get PDFTo be effective, software test generation needs to well cover the space of possible inputs. Traditional fuzzing generates large numbers of random inputs, which however are unlikely to contain keywords and other specific inputs of non-trivial input languages. Constraint-based test generation solves conditions of paths leading to uncovered code, but fails on programs with complex input conditions because of path explosion. In this paper, we present a test generation technique specifically directed at input parsers. We systematically produce inputs for the parser and track comparisons made; after every rejection, we satisfy the comparisons leading to rejection. This approach effectively covers the input space: Evaluated on five subjects, from CSV files to JavaScript, our pFuzzer prototype covers more tokens than both random-based and constraint-based approaches, while requiring no symbolic analysis and far fewer tests than random fuzzers
Approximating Algorithmic Conditional Independence for Discrete Data
Get PDFTesting for conditional independence is a core part of
constraint-based causal discovery. It is mainly used to find
associations, but can in special cases also be applied to infer
causal arrows. We specifically focus on discrete data. Although
commonly used tests are perfect in theory, due to data sparsity
they often fail to reject independence in practice—especially
when conditioning on multiple variables.
We propose a new conditional independence test based on
the notion of algorithmic independence. To instantiate this
ideal formulation in practice, we use stochastic complexity.
We show that our proposed test SCI is an asymptotically
unbiased estimator for conditional mutual information (CMI)
as well as L2 consistent. Further, we show that SCI can be
reformulated to find a sensible threshold for CMI that works
well given only limited data.
Empirical evaluation shows that SCI has a lower type II error
than commonly used tests, which leads to a higher recall when
we use it in causal discovery algorithms; without compromising the precision
Encoding Redundancy for Satisfaction-Driven Clause Learning
Get PDFSatisfaction-Driven Clause Learning (SDCL) is a recent SAT
solving paradigm that aggressively trims the search space of possible truth assignments. To determine if the SAT solver is currently exploring a dispensable part of the search space, SDCL uses the so-called positive reduct of a formula: The positive reduct is an easily solvable propositional formula that is satisfiable if the current assignment of the solver can be safely pruned from the search space. In this paper, we present two novel variants of the positive reduct that allow for even more aggressive pruning. Using one of these variants allows SDCL to solve harder problems, in particular the well-known Tseitin formulas and mutilated chessboard problems. For the first time, we are able to generate and automatically check clausal proofs for large instances of these problems
Discovering Robustly Connected Subgraphs with Simple Descriptions
Get PDFWe study the problem of discovering robustly connected subgraphs that have simple descriptions. Our aim is, hence, to discover vertex sets which not only a) induce a subgraph that is difficult to fragment into disconnected components, but also b) can be selected from the entire graph using just a simple conjunctive query on their vertex attributes. Since many subgraphs do not have such a simple logical description, first mining robust subgraphs and post-hoc discovering their description leads to sub-optimal results. Instead, we propose to optimise over describable subgraphs only. To do so efficiently we propose a non-redundant iterative deepening approach, which we equip with a linear-time tight optimistic estimator that allows pruning large parts of the search space. Extensive empirical evaluation shows that our method can handle large real-world graphs, and discovers easily interpretable and meaningful subgraphs
Discovering Reliable Correlations in Categorical Data
Get PDFIn many scientific tasks we are interested in discovering whether there exist any correlations in our data. This raises many questions, such as how to reliably and interpretably measure correlation between a multivariate set of attributes, how to do so without having to make assumptions on distribution of the data or the type of correlation, and, how to efficiently discover the top-most reliably correlated attribute sets from data. In this paper we answer these questions for discovery tasks in categorical data.
In particular, we propose a corrected-for-chance, consistent, and efficient estimator for normalized total correlation, by which we obtain a reliable, naturally interpretable, non-parametric measure for correlation over multivariate sets. For the discovery of the top-k correlated sets, we derive an effective algorithmic framework based on a tight bounding function. This framework offers exact, approximate, and heuristic search. Empirical evaluation shows that already for small sample sizes the estimator leads to low-regret optimization outcomes, while the algorithms are shown to be highly effective for both large and high-dimensional data. Through two case studies we confirm that our discovery framework identifies interesting and meaningful correlations
Discovering Robustly Connected Subgraphs with Simple Descriptions
Get PDFWe study the problem of discovering robustly connected subgraphs that have simple descriptions. Our aim is, hence, to discover vertex sets which not only a) induce a subgraph that is difficult to fragment into disconnected components, but also b) can be selected from the entire graph using just a simple conjunctive query on their vertex attributes. Since many subgraphs do not have such a simple logical description, first mining robust subgraphs and post-hoc discovering their description leads to sub-optimal results. Instead, we propose to optimise over describable subgraphs only. To do so efficiently we propose a non-redundant iterative deepening approach, which we equip with a linear-time tight optimistic estimator that allows pruning large parts of the search space. Extensive empirical evaluation shows that our method can handle large real-world graphs, and discovers easily interpretable and meaningful subgraphs