Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Learning User Interface Element Interactions
When generating tests for graphical user interfaces, one central problem is to identify how individual UI elements can be interacted with---clicking, long- or right-clicking, swiping, dragging, typing, or more. We present an approach based on reinforcement learning that automatically learns which interactions can be used for which elements, and uses this information to guide test generation.
We model the problem as an instance of the multi-armed bandit problem (MAB) from probability theory and show how its traditional solutions work on test generation, with and without relying on previous knowledge.
The resulting guidance yields higher coverage. In our evaluation, our approach shows improvements in statement coverage between 18% (when not using any previous knowledge) and 20% (when reusing previously generated models)
Identifiability of Cause and Effect using Regularized Regression
We consider the problem of telling apart cause from effect between
two univariate continuous-valued random variables X and Y. In
general, it is impossible to make definite statements about causality
without making assumptions on the underlying model; one of the
most important aspects of causal inference is hence to determine
under which assumptions are we able to do so.
In this paper we show under which general conditions we can
identify cause from effect by simply choosing the direction with the
best regression score. We define a general framework of identifiable
regression-based scoring functions, and show how to instantiate it
in practice using regression splines. Compared to existing methods
that either give strong guarantees, but are hardly applicable in
practice, or provide no guarantees, but do work well in practice, our
instantiation combines the best of both worlds; it gives guarantees,
while empirical evaluation on synthetic and real-world data shows
that it performs at least as well as the state of the art
Highly Efficient Key Exchange Protocols with Optimal Tightness: Enabling real-world deployments with theoretically sound parameters
In this paper we give nearly-tight reductions for modern implicitly authenticated Diffie-Hellman protocols in the style of the Signal and Noise protocols which are extremely simple and efficient. Unlike previous approaches, the combination of nearly-tight proofs and efficient protocols enables the first real-world instantiations for which the parameters can be chosen in a theoretically sound manner.
Our reductions have only a linear loss in the number of users, implying that our protocols are more efficient than the state of the art when instantiated with theoretically sound parameters. We also prove that our security proofs are optimal: a linear loss in the number of users is unavoidable for our protocols for a large and natural class of reductions
A symbolic algorithm for lazy synthesis of eager strategies
We present an algorithm for solving two-player safety games that combines a mixed forward/backward search strategy with a symbolic representation of the state space. By combining forward and backward exploration, our algorithm can synthesize strategies that are eager in the sense that they try to prevent progress towards the error states as soon as possible, whereas standard backwards algorithms often produce permissive solutions that only react when absolutely necessary. We provide experimental results for two classes of crafted benchmarks, the benchmark set of the Reactive Synthesis Competition (SYNTCOMP) 2017, as well as a set of randomly generated benchmarks. The results show that our algorithm in many cases produces more eager strategies than a standard backwards algorithm, and solves a number of benchmarks that are intractable for existing tools. Finally, we observe a connection between our algorithm and a recently proposed algorithm for the synthesis of controllers that are robust against disturbances, pointing to possible future applications
Poster: simFIDO – FIDO2 User Authentication with simTPM
WebAuthn as part of FIDO2 is a new standard for two-factor and even password-less user authentication to web-services. Leading browsers, like Google Chrome, Microsoft Edge, and Mozilla Firefox, support the WebAuthn API. Unfortunately, the availability of hardware authenticators that support FIDO2 authentication is still focused heavily on desktop computers, while for mobile devices, only a limited choice of suitable authenticators is available to users (few roaming authenticators with wireless connectivity and even
fewer built-in platform authenticators on mobile devices). This creates a void for users, in particular users of older device generations that lack platform authenticators and the right connectivity, to authenticate themselves with WebAuthn to web-services.
In this poster, we present the idea of simFIDO, a FIDO2 setup using a recently developed simTPM as (platform) authenticator for mobile devices and even as roaming authenticator offered by mobile devices to connected computers. The move-ability property of the key storage of simTPM makes the users’ lives easier for credential
portability between devices. In particular, a seamless integration of simTPM with non-mobile devices through phones will help to create a kind of universal authentication setup using FIDO2.
Although we present the concrete design and implementation
of a SIM card-based FIDO2 authenticator, we hope this poster will contribute to the discussion about how and in which form hardware authenticators can be made available to users
Discovering Reliable Dependencies from Data: Hardness and Improved Algorithms (Extended Abstract)
Finding (functional) dependencies between attributes in databases is a well-known problem with applications in knowledge discovery, feature selection, and database management. While the recently introduced reliable fraction of information measure allows to soundly quantify dependence in a way that avoids overfitting when optimizing over high-dimensional spaces, the algorithmic implications of using this score have not yet been systematically explored. This includes the computational complexity of the resulting optimization problem.
To this end, this paper provides the following contributions: We show that the problem of maximizing the reliable fraction of information is NP-hard, which justifies the usage of worst-case exponential-time as well as heuristic search methods that do not guarantee optimal solutions. We then greatly improve the practical performance for both of these optimization styles by deriving a novel admissible bounding function, which has an unbounded potential for additional pruning over the previously proposed one. Finally, we empirically investigate for the first time the approximation ratio of the greedy algorithm and show that in fact it produces highly competitive results in a fraction of time needed for complete branch-and-bound style search. All findings are evaluated on a wide range of real-world datasets that are publicly available along with the implementation of the algorithmic contributions.
Our results suggest that in scenarios where no hard optimality guarantees are required, greedy optimization is a good alternative to branch-and-bound for dependency discovery. Also, the definition of the tighter bounding function is potentially more generally applicable than just to the reliable fraction of information and might be transferrable to other dependency measures
MPIIGaze: Real-World Dataset and Deep Appearance-Based Gaze Estimation
Learning-based methods are believed to work well for unconstrained gaze estimation, i.e. gaze estimation from a
monocular RGB camera without assumptions regarding user, environment, or camera. However, current gaze datasets were collected
under laboratory conditions and methods were not evaluated across multiple datasets. Our work makes three contributions towards
addressing these limitations. First, we present the MPIIGaze dataset, which contains 213,659 full face images and corresponding
ground-truth gaze positions collected from 15 users during everyday laptop use over several months. An experience sampling
approach ensured continuous gaze and head poses and realistic variation in eye appearance and illumination. To facilitate
cross-dataset evaluations, 37,667 images were manually annotated with eye corners, mouth corners, and pupil centres. Second, we
present an extensive evaluation of state-of-the-art gaze estimation methods on three current datasets, including MPIIGaze. We study
key challenges including target gaze range, illumination conditions, and facial appearance variation. We show that image resolution
and the use of both eyes affect gaze estimation performance, while head pose and pupil centre information are less informative. Finally,
we propose GazeNet, the first deep appearance-based gaze estimation method. GazeNet improves on the state of the art by 22%
(from a mean error of 13.9 degrees to 10.8 degrees) for the most challenging cross-dataset evaluation
Zero Residual Attacks on Industrial Control Systems and Stateful Countermeasures
In this paper, we discuss the practical implementation of stealthy attacks on industrial control systems. We start by reviewing the attacks proposed in prior works. Then, we offer Zero-Residual Attacks (ZeRA), which allow the attacker to launch stealthy attacks leveraging estimation of the stateful anomaly detector and matching of residuals as a fraction of actual estimation residual. To perform the zero residual attack, the attacker will require the use of two state estimators each for the physical system state and the detector system state, adding complexity that was so far not discussed. We implement ZeRA and demonstrate its efficacy. Then, we propose to use a Stateful Detector (SD) to precisely detect such stealthy attacks. We design and implement the SD detector. The obtained results from the performance evaluation demonstrate that we can detect stealthy attacks such as the ZeRA, with precision above 99%, sensitivity above 99%, and Matthews correlation coefficient above 0.98
Verifying Hyperliveness
yperLTL is an extension of linear-time temporal logic for the specification of hyperproperties, i.e., temporal properties that relate multiple computation traces. HyperLTL can express information flow policies as well as properties like symmetry in mutual exclusion algorithms or Hamming distances in error-resistant transmission protocols. Previous work on HyperLTL model checking has focussed on the alternation-free fragment of HyperLTL, where verification reduces to checking a standard trace property over an appropriate self-composition of the system. The alternation-free fragment does, however, not cover general hyperliveness properties. Universal formulas, for example, cannot express the secrecy requirement that for every possible value of a secret variable there exists a computation where the value is different while the observations made by the external observer are the same. In this paper, we study the more difficult case of hyperliveness properties expressed as HyperLTL formulas with quantifier alternation. We reduce existential quantification to strategic choice and show that synthesis algorithms can be used to eliminate the existential quantifiers automatically. We furthermore show that this approach can be extended to reactive system synthesis, i.e., to automatically construct a reactive system that is guaranteed to satisfy a given HyperLTL formula