Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Automatic Optimizations for Stream-based Monitoring Languages
Get PDFRuntime monitors that are specified in a stream-based monitoring language tend to be easier to understand, maintain, and reuse than those written in a standard programming language. Because of their formal semantics, such specification languages are also a natural choice for safety-critical applications. Unlike for standard programming languages, there is, however, so far very little support for automatic code optimization. In this paper, we present the first collection of code transformations for the stream-based monitoring language RTLola. We show that classic compiler optimizations, such as Sparse Conditional Constant Propagation and Common Subexpression Elimination, can be adapted to monitoring specifications. We also develop new transformations — Pacing Type Refinement and Filter Refinement — which exploit the specific modular structure of RTLola as well as the implementation freedom afforded by a declarative specification language. We demonstrate the significant impact of the code transformations on benchmarks from the monitoring of unmanned aircraft systems (UAS)
Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS
Get PDFThe control logic of complex systems is based on experience: Trained experts steer a machine directly until they help develop an automated controller. Recently, this process was further improved by successfully incorporating machine learning techniques, where the controller was learned from tremendous amounts of empirical data. The resulting controller excels most of the time, especially in situations similar to ones occurring in the training data. In a safety-critical context, however, this is not enough, so formal guarantees about the behavior of the controller become crucial. When a full static analysis and subsequent verification is infeasible due to the complexity of the system, runtime monitoring is still applicable. It acts as a connecting link between the efficiency of trained controllers and formally verifiable guarantees. A runtime monitor assesses the system health based on sensor readings by using a specification that contains information about desired system states and their expected evolution over time. When the monitor encounters a violation of the specification, it raises an alarm. For complex systems, characterizing the desired behavior requires an expressive language. Moreover, provably correct behavior requires formal semantics and an evaluation algorithm with static guarantees on resource consumption to prevent crashes during runtime. This thesis presents formal semantics for the specification language RTLola and shows that it satisfies the aforementioned criteria by introducing an evaluation algorithm with static time and space bounds. The approach is evaluated based on examples from health monitoring and aircraft controllers
GS-WGAN: A Gradient-Sanitized Approach for Learning Differentially Private Generators
No full textThe wide-spread availability of rich data has fueled the growth of machine learning applications in numerous domains. However, growth in domains with highly-sensitive data (e.g., medical) is largely hindered as the private nature of data prohibits it from being shared. To this end, we propose Gradient-sanitized Wasserstein Generative Adversarial Networks (GS-WGAN), which allows releasing a sanitized form of the sensitive data with rigorous privacy guarantees. In contrast to prior work, our approach is able to distort gradient information more precisely, and thereby enabling training deeper models which generate more informative samples. Moreover, our formulation naturally allows for training GANs in both centralized and federated (i.e., decentralized) data scenarios. Through extensive experiments, we find our approach consistently outperforms state-of-the-art approaches across multiple metrics (e.g., sample quality) and datasets
Up2Dep: Android Tool Support to Fix Insecure Code Dependencies
Get PDFThird-party libraries, especially outdated versions, can introduce and multiply security & privacy related issues to Android applications. While prior work has shown the need for tool support for developers to avoid libraries with security problems, no such a solution has yet been brought forward to Android. It is unclear how such a solution would work and which challenges need to be solved in realizing it.
In this work, we want to make a step forward in this direction. We propose Up2Dep, an Android Studio extension that supports Android developers in keeping project dependencies up-to-date and in avoiding insecure libraries. To evaluate the technical feasibility of Up2Dep, we publicly released Up2Dep and tested it with Android developers (N=56) in their daily tasks. Up2Dep has delivered quick-fixes that mitigate 108 outdated dependencies and 8 outdated dependencies with security problems in 34 real projects. It was perceived by those developers as being helpful. Our results also highlight technical challenges in realizing such support, for which we provide solutions and new insights.
Our results emphasize the urgent need for designated tool support to detect and update insecure outdated third-party libraries in Android apps. We believe that Up2Dep has provided a valuable step forward to improving the security of the Android ecosystem and encouraging results for tool support with a tangible impact as app developers have an easy means to fix their outdated and insecure dependencies
SampleFix: Learning to Correct Programs by Sampling Diverse Fixes
No full textAutomatic program correction is an active topic of research, which holds the potential of dramatically improving productivity of programmers during the software development process and correctness of software in general. Recent advances in machine learning, deep learning and NLP have rekindled the hope to eventually fully automate the process of repairing programs. A key challenge is ambiguity, as multiple codes -- or fixes -- can implement the same functionality. In addition, datasets by nature fail to capture the variance introduced by such ambiguities. Therefore, we propose a deep generative model to automatically correct programming errors by learning a distribution of potential fixes. Our model is formulated as a deep conditional variational autoencoder that samples diverse fixes for the given erroneous programs. In order to account for ambiguity and inherent lack of representative datasets, we propose a novel regularizer to encourage the model to generate diverse fixes. Our evaluations on common programming errors show for the first time the generation of diverse fixes and strong improvements over the state-of-the-art approaches by fixing up to 65% of the mistakes
Cross-Origin State Inference (COSI) Attacks: Leaking Web Site States through XS-Leaks
Get PDFIn a Cross-Origin State Inference (COSI) attack, an attacker convinces a victim into visiting an attack web page, which leverages the cross-origin interaction features of the victim's web browser to infer the victim's state at a target web site. Multiple instances of COSI attacks have been found in the past under different names such as login detection or access detection attacks. But, those attacks only consider two states (e.g., logged in or not) and focus on a specific browser leak method (or XS-Leak). This work shows that mounting more complex COSI attacks such as deanonymizing the owner of an account, determining if the victim owns sensitive content, and determining the victim's account type often requires considering more than two states. Furthermore, robust attacks require supporting a variety of browsers since the victim's browser cannot be predicted apriori. To address these issues, we present a novel approach to identify and build complex COSI attacks that differentiate more than two states and support multiple browsers by combining multiple attack vectors, possibly using different XS-Leaks. To enable our approach, we introduce the concept of a COSI attack class. We propose two novel techniques to generalize existing COSI attack instances into COSI attack classes and to discover new COSI attack classes. We systematically apply our techniques to existing attacks, identifying 40 COSI attack classes. As part of this process, we discover a novel XS-Leak based on window.postMessage. We implement our approach into Basta-COSI, a tool to find COSI attacks in a target web site. We apply Basta-COSI to test four stand-alone web applications and 58 popular web sites, finding COSI attacks against each of them
On the Parameterized Approximability of Contraction to Classes of Chordal Graphs
Get PDFA graph operation that contracts edges is one of the fundamental operations in the theory of graph minors. Parameterized Complexity of editing to a family of graphs by contracting k edges has recently gained substantial scientific attention, and several new results have been obtained. Some important families of graphs, namely the subfamilies of chordal graphs, in the context of edge contractions, have proven to be significantly difficult than one might expect. In this paper, we study the F-Contraction problem, where F is a subfamily of chordal graphs, in the realm of parameterized approximation. Formally, given a graph G and an integer k, F-Contraction asks whether there exists X ⊆ E(G) such that G/X ∈ F and |X| ≤ k. Here, G/X is the graph obtained from G by contracting edges in X. We obtain the following results for the F-Contraction problem. - Clique Contraction is known to be FPT. However, unless NP ⊆ coNP/poly, it does not admit a polynomial kernel. We show that it admits a polynomial-size approximate kernelization scheme (PSAKS). That is, it admits a (1 + ε)-approximate kernel with {O}(k^{f(ε)}) vertices for every ε > 0. - Split Contraction is known to be W[1]-Hard. We deconstruct this intractability result in two ways. Firstly, we give a (2+ε)-approximate polynomial kernel for Split Contraction (which also implies a factor (2+ε)-FPT-approximation algorithm for Split Contraction). Furthermore, we show that, assuming Gap-ETH, there is no (5/4-δ)-FPT-approximation algorithm for Split Contraction. Here, ε, δ > 0 are fixed constants. - Chordal Contraction is known to be W[2]-Hard. We complement this result by observing that the existing W[2]-hardness reduction can be adapted to show that, assuming FPT ≠ W[1], there is no F(k)-FPT-approximation algorithm for Chordal Contraction. Here, F(k) is an arbitrary function depending on k alone. We say that an algorithm is an h(k)-FPT-approximation algorithm for the F-Contraction problem, if it runs in FPT time, and on any input (G, k) such that there exists X ⊆ E(G) satisfying G/X ∈ F and |X| ≤ k, it outputs an edge set Y of size at most h(k) ⋅ k for which G/Y is in F. We find it extremely interesting that three closely related problems have different behavior with respect to FPT-approximation
A Framework for Exponential-Time-Hypothesis--Tight Algorithms and Lower Bounds in Geometric Intersection Graphs
Get PDFWe give an algorithmic and lower bound framework that facilitates the construction of subexponential algorithms and matching conditional complexity bounds. It can be applied to intersection graphs of similarly-sized fat objects, yielding algorithms with running time for any fixed dimension for many well-known graph problems, including Independent Set, -Dominating Set for constant , and Steiner Tree. For most problems, we get improved running times compared to prior work; in some cases, we give the first known subexponential algorithm in geometric intersection graphs. Additionally, most of the obtained algorithms are representation-agnostic, i.e., they work on the graph itself and do not require the geometric representation. Our algorithmic framework is based on a weighted separator theorem and various treewidth techniques. The lower bound framework is based on a constructive embedding of graphs into -dimensional grids, and it allows us to derive matching lower bounds under the exponential time hypothesis even in the much more restricted class of -dimensional induced grid graphs
Parameterized Verification of Systems with Global Synchronization and Guards
Get PDFInspired by distributed applications that use consensus or
other agreement protocols for global coordination, we define a new computational model for parameterized systems that is based on a general global synchronization primitive and allows for global transition guards. Our model generalizes many existing models in the literature, including
broadcast protocols and guarded protocols. We show that reachability properties are decidable for systems without guards, and give sufficient conditions under which they remain decidable in the presence of guards. Furthermore, we investigate cutoffs for reachability properties and provide sufficient conditions for small cutoffs in a number of cases that are inspired by our target applications