We present the first systematic approach to static and dynamic taint analysis for Graph APIs focusing on broken access control. The approach comprises the following. We taint nodes of the Graph API if they represent data requiring specific privileges in order to be retrieved or manipulated, and identify API calls which are related to sources and sinks. Then, we statically analyze whether a tainted information flow between API source and sink calls occurs. To this end, we model the API calls using graph transformation rules. We subsequently use Critical Pair Analysis to automatically analyze potential dependencies between rules representing source calls and rules representing sink calls. We distinguish direct from indirect tainted information flow and argue under which conditions the Critical Pair Analysis is able to detect not only direct, but also indirect tainted flow. The static taint analysis (i) identifies flows that need to be further reviewed, since tainted nodes may be created by an API call and used or manipulated by another API call later without having the necessary privileges, and (ii) can be used to systematically design dynamic security tests for broken access control. The dynamic taint analysis checks if potential broken access control risks detected during the static taint analysis really occur. We apply the approach to a part of the GitHub GraphQL API. The application illustrates that our analysis supports the detection of two types of broken access control systematically: the case where users of the API may not be able to access or manipulate information, although they should be able to do so; and the case where users (or attackers) of the API may be able to access/manipulate information that they should not.

Kein CA

Abstract In model-driven engineering, runtime monitoring of systems with complex dynamic structures is typically performed via a runtime model capturing a snapshot of the system state: the model is represented as a graph and properties of interest as graph queries which are evaluated over the model online. For temporal properties, history-aware runtime models encode a trace of timestamped snapshots, which is monitored via temporal graph queries. In this case, the query evaluation needs to consider that a trace may be incomplete, thus future changes to the model may affect current answers. So far there is no formal foundation for query-based monitoring over runtime models encoding incomplete traces. In this paper, we present a systematic and formal treatment of incomplete traces. First, we introduce a new definite semantics for a first-order temporal graph logic which only returns answers if no future change to the model will affect them. Then, we adjust the query evaluation semantics of a querying approach we previously presented, which is based on this logic, to the definite semantics of the logic. Lastly, we enable the approach to keep to its efficient query evaluation technique, while returning (the more costly) definite answers.

Abstract Optimization problems in software engineering typically deal with structures as they occur in the design and maintenance of software systems. In model-driven optimization (MDO), domain-specific models are used to represent these structures while evolutionary algorithms are often used to solve optimization problems. However, designing appropriate models and evolutionary algorithms to represent and evolve structures is not always straightforward. Domain experts often need deep knowledge of how to configure an evolutionary algorithm. This makes the use of model-driven meta-heuristic search difficult and expensive. We present a graph-based framework for MDO that identifies and clarifies core concepts and relies on mutation operators to specify evolutionary change. This framework is intended to help domain experts develop and study evolutionary algorithms based on domain-specific models and operators. In addition, it can help in clarifying the critical factors for conducting reproducible experiments in MDO. Based on the framework, we are able to take a first step toward identifying and studying important properties of evolutionary operators in the context of MDO. As a showcase, we investigate the impact of soundness and completeness at the level of mutation operator sets on the effectiveness and efficiency of evolutionary algorithms.

Abstract We introduce a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing graph repairs from which a user may select a graph repair based on non-formalized further requirements. This incremental approach features delta preservation as it allows to restrict the generation of graph repairs to delta-preserving graph repairs, which do not revert the additions and deletions of the most recent consistency-violating graph update. We specify consistency of graphs using the logic of nested graph conditions, which is equivalent to first-order logic on graphs. Technically, the incremental approach encodes if and how the graph under repair satisfies a graph condition using the novel data structure of satisfaction trees, which are adapted incrementally according to the graph updates applied. In addition to the incremental approach, we also present two state-based graph repair algorithms, which restore consistency of a graph independent of the most recent graph update and which generate additional graph repairs using a global perspective on the graph under repair. We evaluate the developed algorithms using our prototypical implementation in the tool AutoGraph and illustrate our incremental approach using a case study from the graph database domain.

Graph repair, restoring consistency of a graph, plays a prominent role in several areas of computer science and beyond: For example, in model-driven engineering, the abstract syntax of models is usually encoded using graphs. Flexible edit operations temporarily create inconsistent graphs not representing a valid model, thus requiring graph repair. Similarly, in graph databases—managing the storage and manipulation of graph data—updates may cause that a given database does not satisfy some integrity constraints, requiring also graph repair. We present a logic-based incremental approach to graph repair, generating a sound and complete (upon termination) overview of least-changing repairs. In our context, we formalize consistency by so-called graph conditions being equivalent to first-order logic on graphs. We present two kind of repair algorithms: State-based repair restores consistency independent of the graph update history, whereas delta-based (or incremental) repair takes this history explicitly into account. Technically, our algorithms rely on an existing model generation algorithm for graph conditions implemented in $$\textsc {AutoGraph}$$ . Moreover, the delta-based approach uses the new concept of satisfaction (ST) trees for encoding if and how a graph satisfies a graph condition. We then demonstrate how to manipulate these $$\mathrm {STs}$$ incrementally with respect to a graph update.

Although Model-Based Software Engineering (MBE) is a widely accepted Software Engineering (SE) discipline, no agreed-upon core set of concepts and practices (i.e., a Body of Knowledge) has been defined for it yet. With the goals of characterizing the contents of the MBE discipline, promoting a global consistent view of it, clarifying its scope with regard to other SE disciplines, and defining a foundation for the development of educational curricula on MBE, this paper proposes the contents for a Body of Knowledge for MBE. We also describe the methodology that we have used to come up with the proposed list of contents, as well as the results of a survey study that we conducted to sound out the opinion of the community on the importance of the proposed topics and their level of coverage in the existing SE curricula.

The correctness of model transformations is a crucial element for model-driven engineering of high-quality software. In particular, behavior preservation is an important correctness property avoiding the introduction of semantic errors during the model-driven engineering process. Behavior preservation verification techniques show some kind of behavioral equivalence or refinement between source and target model of the transformation. Automatic tool support is available for verifying behavior preservation at the instance level, i.e., for a given source and target model specified by the model transformation. However, until now there is no sound and automatic verification approach available at the transformation level, i.e., for all source and target models. In this article, we extend our results presented in earlier work (Giese and Lambers, in: Ehrig et al (eds) Graph transformations, Springer, Berlin, 2012 ) and outline a new transformation-level approach for the sound and automatic verification of behavior preservation captured by bisimulation resp. simulation for outplace model transformations specified by triple graph grammars and semantic definitions given by graph transformation rules. In particular, we first show how behavior preservation can be modeled in a symbolic manner at the transformation level and then describe that transformation-level verification of behavior preservation can be reduced to invariant checking of suitable conditions for graph transformations. We demonstrate that the resulting checking problem can be addressed by our own invariant checker for an example of a transformation between sequence charts and communicating automata.

Conflict and dependency analysis (CDA) of graph transformation has been shown to be a versatile foundation for understanding interactions in many software engineering domains, including software analysis and design, model-driven engineering, and testing. In this paper, we propose a novel static CDA technique that is multi-granular in the sense that it can detect all conflicts and dependencies on multiple granularity levels. Specifically, we provide an efficient algorithm suite for computing binary, coarse-grained, and fine-grained conflicts and dependencies: Binary granularity indicates the presence or absence of conflicts and dependencies, coarse granularity focuses on root causes for conflicts and dependencies, and fine granularity shows each conflict and dependency in full detail. Doing so, we can address specific performance and usability requirements that we identified in a literature survey of CDA usage scenarios. In an experimental evaluation, our algorithm suite computes conflicts and dependencies rapidly. Finally, we present a user study, in which the participants found our coarse-grained results more understandable than the fine-grained ones reported in a state-of-the-art tool. Our overall contribution is twofold: (i) we significantly speed up the computation of fine-grained and binary CDA results and, (ii) complement them with coarse-grained ones, which offer usability benefits for numerous use cases.

Nested application conditions generalise the well-known negative application conditions and are important for several application domains. In this paper, we present Local Church–Rosser, Parallelism, Concurrency and Amalgamation Theorems for rules with nested application conditions in the framework of $\mathcal{M}$ -adhesive categories, where $\mathcal{M}$ -adhesive categories are slightly more general than weak adhesive high-level replacement categories. Most of the proofs are based on the corresponding statements for rules without application conditions and two shift lemmas stating that nested application conditions can be shifted over morphisms and rules.

Graph transformation systems have been studied extensively and applied to several areas of computer science like formal language theory, the modeling of databases, concurrent or distributed systems, and visual, logical, and functional programming. In

Applying an attributed graph transformation rule to a given object graph always implies some kind of constraint solving. In many cases, the given constraints are almost trivial to solve. For instance, this is the case when a rule describes a transfor

Flexibility and interoperability make web services well suited for designing highly-customizable reactive service-based ap-plications, that is interactive applications that can be rapidly adapted to new requirements and environmental conditions. This is the case, for example of personal data managers that many users tailor to their needs to meet different usage con-ditions and requests. In this paper, we propose a model-based approach that provides users with the ability of rapidly developing, adapt-ing and reconfiguring reactive service-based applications to meet new requirements and needs. Users specify their needs by describing sample executions that include interactions with web services through an intuitive interface. Interac-tions are stored in a visual formalism that integrates live sequence charts with graph transformation systems. Mod-els can be visualized, modified, executed and automatically analyzed to identify inconsistencies.