Search

Usage control concerns how data is used post-access. In existing work on usage control enforcement, policies are assumed to exist at the implementation-level: their derivation from specification-level policies has not been looked into. The expected behavior of a usage controlled system may therefore differ from the actual behavior. This research fills this gap with a policy derivation framework that uses a model-based refinement of domain-specific abstractions, data and actions, in terms of technical constructs viz. events and states of systems., Existierende Arbeiten zur Datennutzungskontrolle setzen die Existenz von Datennutzungsrichtlinien auf der Implementierungsebene voraus. Die Ableitung dieser Datennutzungsrichtlinien von der umgangssprachlichen Spezifikationsebene zur Implementierungsebene wurde in bisherigen Arbeiten jedoch noch nicht untersucht. Entsprechend beschreibt diese Doktorarbeit eine solche Ableitung von Datennutzungsrichtlinien mit Hilfe von Regeln die auf einer modellbasierten Verfeinerung der domänenspezifischen Daten und Aktionen basiert.

Usage control (UC) specifies what happens to data after access to it has been granted. Within the system, data (e.g. “a picture”) exists in form of various representations, possibly located at different levels of abstraction (e.g. a file, a set of pixels or a Java object). To control data, one must control the usage of all its different representations.This work (1) presents a generic UC model and a policy specification language that capture the distinction between data and representations of data and (2) discusses how to improve the model’s precision leveraging additional information about the system., Datennutzungskontrolle (DNK) spezifiziert, was mit Daten passiert, nachdem der initiale Zugriff auf diese gewährt wurde. Dazu muss die Nutzung der Daten (z.B. "ein Bild") in allen verschiedenen Repräsentationen (z.B. eine Datei, ein Java Objekt) innerhalb eines Systems kontrolliert werden. Die vorliegende Arbeit 1) präsentiert ein generisches DNK-Modell und eine Richtlinienspezifikationssprache, die den Unterschied zwischen Daten und ihren Repräsentation erfasst und 2) diskutiert wie durch Zusatzinformationen über das System die Präzision des Modells erhöht werden kann.

This dissertation presents an approach that enables the automatic extraction and selection of workload specifications for session-based application systems. A domain-specific language (DSL) is introduced allowing tool- and system independent specification of workloads. Instances of this DSL are extracted from system logs and are transformed into executable workload specifications of load testing tools and workload specifications of performance models. A multi-objective optimization applied on the performance models enables the selection of workload specifications following given performance objectives. The developed methods are evaluated using a representative application system., Diese Dissertation stellt einen Ansatz vor, der die automatische Extraktion und Auswahl von Workload-Spezifikationen (WS) für Session-basierte Anwendungssysteme ermöglicht. Es wird eine domänenspezifische Sprache (DSL) eingeführt, die eine werkzeug- und systemunabhängige Spezifikation von Workloads ermöglicht. Instanzen dieser DSL werden aus Systemlogs extrahiert und in ausführbare WS von Lasttest-Tools sowie in WS von Performance-Modellen transformiert. Eine auf die Performance-Modelle angewendete mehrkriterielle Optimierung ermöglicht die Auswahl von WS innerhalb vorgegebener Ziele. Die entwickelten Methoden werden mit einem repräsentativen Anwendungssystem evaluiert.

This thesis deals with the automated detection of common software weaknesses in C programs. The approach is selective symbolic execution on the source code level with interpolation based path merging. Interpolation and path merging are used to reduce the necessary computational effort without reduction in bug detection accuracy compared to path coverage, the symbolic execution then achieves error and branch coverage. Interpolation is also used to further reduce the computational effort and to achieve a selectable coverage criterion (e.g., branch coverage), at the expense of false negative detections. The interpolation consists in a removal of constraints from the path constraint. It is shown that the considered algorithms yield an interpolation and coverage hierarchy with respect to subsets of constraints and subsets of program paths, and with respect to the implication of coverage criteria, respectively. Modification of source code is not necessary for analysis. Symbolic execution with Satisfiability Modulo Theories Solver is combined with binary instrumentation to efficiently detect different bug types. The implementation is a plug-in extension to the Eclipse C/C++ development tools and uses a debugger machine interface. It is evaluated by detecting memory access errors, infinite loops, information exposures, dead code and data race conditions in test programs from the Juliet test suite for program analyzers., Die vorliegende Arbeit beschäftigt sich mit der automatischen Erkennung von Fehlern (Common Weaknesses) in C Programmen. Der Ansatz ist eine selektive symbolische Ausführung auf der Quelltext-Ebene mit interpolationsbasierter Pfadverschmelzung. Interpolation und Pfadverschmelzung werden einerseits zur Verringerung der nötigen Rechenleistung ohne Genauigkeitsverlust der Fehlererkennung im Vergleich zu Path Coverage eingesetzt, erzielt wird dann ”Error and Branch Coverage”. Andererseits kann die Interpolation zur Erreichung eines wählbaren Coverage-Kriteriums (z.B. Branch Coverage) angepasst werden, um die nötige Rechenleistung noch weiter zur reduzieren, allerdings bei verminderter Genauigkeit der Erkennung. Die Interpolation besteht in einer Entfernung von Constraints aus dem Pfad-Constraint. Es wird gezeigt, dass die betrachteten Algorithmen eine Interpolations- und Coverage-Hierarchie ergeben, bezüglich Teilmengen von Constraints bzw. Teilmengen von Programmpfaden und Implikation von Coverage-Kriterien. Anpassungen des Quelltextes sind zur Analyse nicht erforderlich. Symbolische Ausführung mit Satisfiability Modulo Theories Solver wird mit Instrumentierung von Binärcode kombiniert, um verschiedene Fehlerarten effizient zu erkennen. Die Implementierung ist eine plug-in Erweiterung der Eclipse C/C++ Development Tools und verwendet ein Debugger Machine Interface. Sie wird mit Testprogrammen der Juliet Suite für Speicherzugriffsfehler, Endlosschleifen, Information Exposures, Dead Code und Race Conditions bewertet.

For behavior models expressed in statechart-like formalisms, we show how to compute semantically equivalent yet structurally different models. These refactorings are defined by user-provided logical predicates that partition the system's state space and that characterize coherent parts - modes or control states-of the behavior. We embed the refactorings into an incremental development process that uses a combination of both tables and graphically represented state machines for describing systems

In this thesis, we develop a framework for the characterization of software obfuscation strength by formalizing automated analysis attacks as search problems. This helps developers to choose obfuscating transformations, which change those software characteristics, such that heuristics are no longer applicable or to increase the search effort to an extent that it is no longer economically attractive. We present multiple experiments involving various software applications, obfuscating transformations and an automated attack based on symbolic execution, whose results support our hypothesis., In dieser Dissertation entwickeln wir eine Grundstruktur, in der wir die automatische Analyse als Suchprobleme formalisieren, deren Komplexität von Eigenschaften der Software abhängt. Dies hilft Entwicklern dabei, die Verschleierungtransformationen auszuwählen, die die Eigenschaften der Software so verändern, dass Heuristiken nicht mehr angewendet werden können oder der benötigte Aufwand für die Suche aus wirtschaftlicher Sicht nicht mehr attraktiv ist. Wir stellen mehrere Fallstudien unter Einbezug von verschiedenen Software-Anwendungen, Verschleierungstransformationen und einem automatisierten Angriff bassierend auf symbolischer Ausführung vor, die unsere Hypothese untermauern.

This thesis explores the benefit of knowledge about which parts of software systems were executed in business information systems. We analyze, how this knowledge can support the activities software maintenance and test. We contribute a series of studies to gain insights into the actual execution of source code and its implications, approaches that transfer knowledge about execution to other artifacts, and we embed the approaches into the maintenance process., Diese Dissertation untersucht die Vorteile von Wissen darüber, welche Teile eines Business Information Systems ausgeführt werden. Wir analysieren, wie dieses Wissen die Aktivitäten Softwarewartung und Softwaretest unterstützen kann. Wir präsentieren Studien, die Einblicke in die tatsächliche Ausführung von Code, und die daraus entstehenden Effekte geben, Ansätze, die Wissen über Ausführung zu anderen Entwicklungsartefakten übertragen und betten diese Ansätze in bestehende Wartungsprozesse ein.

This thesis is concerned with controlling the usage of sensitive data once it has been disseminated to multiple systems. To this end a formal model for distributed data usage control is proposed, allowing to track data flows across systems and to enforce distributed data usage policies in a decentral manner. The correctness of the provided formal methods is proven. Further, the proposed ideas are implemented and evaluated in terms of security as well as communication and performance overheads., Diese Arbeit beschäftigt sich mit der Kontrolle der Nutzung sensibler Daten in verteilten Systemen. Hierzu wird ein formales Modell entwickelt, das es ermöglicht die Verbreitung geschützter Daten systemübergreifend zu verfolgen sowie globale Datennutzungsanforderungen in dezentraler Weise durchzusetzen. Die Korrektheit der entwickelten Methoden wird bewiesen. Ferner werden die Vorschläge implementiert und im Hinblick auf Sicherheit und Leistungseinbußen evaluiert.

Usage control concerns how data is used post-access. In existing work on usage control enforcement, policies are assumed to exist at the implementation-level: their derivation from specification-level policies has not been looked into. The expected behavior of a usage controlled system may therefore differ from the actual behavior. This research fills this gap with a policy derivation framework that uses a model-based refinement of domain-specific abstractions, data and actions, in terms of technical constructs viz. events and states of systems., Existierende Arbeiten zur Datennutzungskontrolle setzen die Existenz von Datennutzungsrichtlinien auf der Implementierungsebene voraus. Die Ableitung dieser Datennutzungsrichtlinien von der umgangssprachlichen Spezifikationsebene zur Implementierungsebene wurde in bisherigen Arbeiten jedoch noch nicht untersucht. Entsprechend beschreibt diese Doktorarbeit eine solche Ableitung von Datennutzungsrichtlinien mit Hilfe von Regeln die auf einer modellbasierten Verfeinerung der domänenspezifischen Daten und Aktionen basiert.