-
Threat Repair with Optimization Modulo Theories
Authors:
Thorsten Tarrach,
Masoud Ebrahimi,
Sandra König,
Christoph Schmittner,
Roderick Bloem,
Dejan Nickovic
Abstract:
We propose a model-based procedure for automatically preventing security threats using formal models. We encode system models and potential threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security questions as satisfiability queries. We formulate threat prevention as an optimization problem over the same formulas. The outcome of our threat prevention procedure i…
▽ More
We propose a model-based procedure for automatically preventing security threats using formal models. We encode system models and potential threats as satisfiability modulo theory (SMT) formulas. This model allows us to ask security questions as satisfiability queries. We formulate threat prevention as an optimization problem over the same formulas. The outcome of our threat prevention procedure is a suggestion of model attribute repair that eliminates threats. Whenever threat prevention fails, we automatically explain why the threat happens. We implement our approach using the state-of-the-art Z3 SMT solver and interface it with the threat analysis tool THREATGET. We demonstrate the value of our procedure in two case studies from automotive and smart home domains, including an industrial-strength example.
△ Less
Submitted 6 October, 2022;
originally announced October 2022.
-
The analysis approach of ThreatGet
Authors:
Korbinian Christl,
Thorsten Tarrach
Abstract:
Nowadays, almost all electronic devices include a communication interface that allows to interact with them, exchange data, or operate their services remotely. The trend toward increased interconnectivity simultaneously increases the vulnerability of these systems. Due to the high costs associated with comprehensive security analysis, many manufacturers neglect the safety aspect of a product in or…
▽ More
Nowadays, almost all electronic devices include a communication interface that allows to interact with them, exchange data, or operate their services remotely. The trend toward increased interconnectivity simultaneously increases the vulnerability of these systems. Due to the high costs associated with comprehensive security analysis, many manufacturers neglect the safety aspect of a product in order to avoid costs. However, the importance of secure IT systems is growing, as the security of a system can also influence safety-critical aspects. Standard security analysis approaches are nowadays still mainly based on time-intensive and error-prone manual activities. In this paper, we present the formal concepts of the automatic threat and vulnerability analysis tool ThreatGet. Therefore, we introduce the concept of the Extended Data-Flow Diagram that is used to represent the system under investigation in an abstracted form, and we highlight the formal analysis language of the tool. This domain-specific language is used to formulate so-called anti-patterns. These anti-patterns that can be interpreted by the tool for an automatic security analysis of the system. Besides the language declaration, we present the entire semantic evaluation of the language during the analysis. Parts of the definitions and elaborations of the diagram model and the analysis language were developed in the context of the master thesis of Korbinian Christl, in cooperation with the University of Vienna.
△ Less
Submitted 21 July, 2021;
originally announced July 2021.
-
Language Inclusion for Finite Prime Event Structures
Authors:
Andreas Fellner,
Thorsten Tarrach,
Georg Weissenbacher
Abstract:
We study the problem of language inclusion between finite, labeled prime event structures. Prime event structures are a formalism to compactly represent concurrent behavior of discrete systems. A labeled prime event structure induces a language of sequences of labels produced by the represented system. We study the problem of deciding inclusion and membership for languages encoded by finite prime…
▽ More
We study the problem of language inclusion between finite, labeled prime event structures. Prime event structures are a formalism to compactly represent concurrent behavior of discrete systems. A labeled prime event structure induces a language of sequences of labels produced by the represented system. We study the problem of deciding inclusion and membership for languages encoded by finite prime event structures and provide complexity results for both problems. We provide a family of examples where prime event structures are exponentially more succinct than formalisms that do not take concurrency into account. We provide a decision algorithm for language inclusion that exploits this succinctness. Furthermore, we provide an implementation of the algorithm and an evaluation on a series of benchmarks. Finally, we demonstrate how our results can be applied to mutation-based test case generation.
△ Less
Submitted 14 November, 2019;
originally announced November 2019.
-
Optimizing Solution Quality in Synchronization Synthesis
Authors:
Pavol Černý,
Edmund M. Clarke,
Thomas A. Henzinger,
Arjun Radhakrishna,
Leonid Ryzhyk,
Roopsha Samanta,
Thorsten Tarrach
Abstract:
Given a multithreaded program written assuming a friendly, non-preemptive scheduler, the goal of synchronization synthesis is to automatically insert synchronization primitives to ensure that the modified program behaves correctly, even with a preemptive scheduler. In this work, we focus on the quality of the synthesized solution: we aim to infer synchronization placements that not only ensure cor…
▽ More
Given a multithreaded program written assuming a friendly, non-preemptive scheduler, the goal of synchronization synthesis is to automatically insert synchronization primitives to ensure that the modified program behaves correctly, even with a preemptive scheduler. In this work, we focus on the quality of the synthesized solution: we aim to infer synchronization placements that not only ensure correctness, but also meet some quantitative objectives such as optimal program performance on a given computing platform.
The key step that enables solution optimization is the construction of a set of global constraints over synchronization placements such that each model of the constraints set corresponds to a correctness-ensuring synchronization placement. We extract the global constraints from generalizations of counterexample traces and the control-flow graph of the program. The global constraints enable us to choose from among the encoded synchronization solutions using an objective function. We consider two types of objective functions: ones that are solely dependent on the program (e.g., minimizing the size of critical sections) and ones that are also dependent on the computing platform. For the latter, given a program and a computing platform, we construct a performance model based on measuring average contention for critical sections and the average time taken to acquire and release a lock under a given average contention.
We empirically evaluated that our approach scales to typical module sizes of many real world concurrent programs such as device drivers and multithreaded servers, and that the performance predictions match reality. To the best of our knowledge, this is the first comprehensive approach for optimizing the placement of synthesized synchronization.
△ Less
Submitted 23 November, 2015;
originally announced November 2015.
-
From Non-preemptive to Preemptive Scheduling using Synchronization Synthesis
Authors:
Pavol Černý,
Edmund M. Clarke,
Thomas A. Henzinger,
Arjun Radhakrishna,
Leonid Ryzhyk,
Roopsha Samanta,
Thorsten Tarrach
Abstract:
We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls…
▽ More
We present a computer-aided programming approach to concurrency. The approach allows programmers to program assuming a friendly, non-preemptive scheduler, and our synthesis procedure inserts synchronization to ensure that the final program works even with a preemptive scheduler. The correctness specification is implicit, inferred from the non-preemptive behavior. Let us consider sequences of calls that the program makes to an external interface. The specification requires that any such sequence produced under a preemptive scheduler should be included in the set of such sequences produced under a non-preemptive scheduler. The solution is based on a finitary abstraction, an algorithm for bounded language inclusion modulo an independence relation, and rules for inserting synchronization. We apply the approach to device-driver programming, where the driver threads call the software interface of the device and the API provided by the operating system. Our experiments demonstrate that our synthesis method is precise and efficient, and, since it does not require explicit specifications, is more practical than the conventional approach based on user-provided assertions.
△ Less
Submitted 18 May, 2015;
originally announced May 2015.
-
Regression-free Synthesis for Concurrency
Authors:
Pavol Černý,
Thomas A. Henzinger,
Arjun Radhakrishna,
Leonid Ryzhyk,
Thorsten Tarrach
Abstract:
While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in for repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate so…
▽ More
While fixing concurrency bugs, program repair algorithms may introduce new concurrency bugs. We present an algorithm that avoids such regressions. The solution space is given by a set of program transformations we consider in for repair process. These include reordering of instructions within a thread and inserting atomic sections. The new algorithm learns a constraint on the space of candidate solutions, from both positive examples (error-free traces) and counterexamples (error traces). From each counterexample, the algorithm learns a constraint necessary to remove the errors. From each positive examples, it learns a constraint that is necessary in order to prevent the repair from turning the trace into an error trace. We implemented the algorithm and evaluated it on simplified Linux device drivers with known bugs.
△ Less
Submitted 14 July, 2014;
originally announced July 2014.
