Practical Approach in Verification of Security Systems Using Satisfiability Modulo Theories

The paper presents a novel method for the verification of security protocols’ (SPs)time properties. The new method uses a translation to satisfiability modulo theories (SMT) problem. In our approach, we model protocol users’ behaviours using networks of synchronized timed automata. Suitably specified correctness properties are defined as a reachability property of some chosen states in an automata network. Then, the network of timed automata and the property are translated to an SMT problem and checked using an SMT-solver and a BMC algorithm. We consider the most important time properties of protocol executions using specially constructed time conditions. The new method was also implemented and experimentally evaluated for six well-known SPs. We also compared our new SMT-based technique with the corresponding SAT-based approach.

SBAT: A Stochastic BPMN Analysis Tool

This paper presents SBAT, a tool framework for the modelling and analysis of complex business workflows. SBAT is applied to analyse an example from the Danish baked goods industry. Based upon the Business Process Modelling and Notation (BPMN) language for business process modelling, we describe a formalised variant of this language extended to support the addition of intention preserving stochastic branching and parameterised reward annotations. Building on previous work, we detail the design of SBAT, a software tool which allows for the analysis of BPMN models. Within SBAT, properties of interest are specified using the temporal logic Probabilistic Computation Tree Logic (PCTL) and we employ stochastic model checking, by means of the model checker PRISM, to compute their exact values. We present a simplified example of a distributed stochastic system where we determine a reachability property and the value of associated rewards in states of interest for a real-world example from a case company in the Danish baked goods industry. The developments are presented in a generalised fashion to make them relevant to the general problem of implementing quantitative probabilistic model checking of graph-based process modelling languages. This paper contains three key elements: 1. SBAT description. 2. Case company description. 3. Using SBAT on the case company. The paper concludes by indicating SBAT’s practical applicability and suggests further research directions.

Non-termination and secure information flow

In secure information flow analysis, the classic Denning restrictions allow a program's termination to be affected by the values of its H variables, resulting in potential information leaks. In an effort to quantify such leaks, in this paper we study a simple imperative language with random assignments. As a thought experiment, we propose a ‘stripping’ operation on programs, which eliminates all ‘high computation’, and prove the fundamental property that stripping cannot decrease the probability of any low outcome. To prove this property, we first introduce a new notion of fast probabilistic simulation on Markov chains and show that it implies a key reachability property. Viewing the stripping function as a binary relation, we then prove that stripping is a fast simulation. As an application, we prove that, under the Denning restrictions, well-typed probabilistic programs are guaranteed to satisfy an approximate probabilistic non-interference property, provided that their probability of non-termination is small.

Dynamical systems: stability and simulability

Computers are used extensively to simulate continuous dynamical systems. However, different conceptual and mathematical structures underlie discrete machines and continuous dynamics, so the question arises as to the ability of the computer to simulate or, more generally, to check the properties of a continuous system.We discuss and compare two notions of stability for a continuous dynamical system,viz.shadowing and robustness, and relate them to both the practical and theoretical computability of the system. We first discuss what we can learn from the stability of a system, using a finite-precision machine. We then show, following the work in Collins (2005), that shadowing fails but robustness succeeds in ensuring the checkability of a reachability property.

Summary and Outlook

Within the total of seven chapters presented here on the topic of Evolutionary Algorithms there are a number of crude but nevertheless powerful simplifications of the model of organic evolution. Chapter 1 clarified that Evolutionary Algorithms, if they are interpreted as global optimization algorithms, are not to be confused with the oversimplified concept of uniform random search. Instead, they rely on keeping the history insofar as the subsequent generation is created at each step of the evolution process from the current generation maintained by the algorithm. In other words: Evolutionary Algorithms are representatives of the mathematical concept of a Markov process (respectively chain, in discrete spaces). Concerning the convergence reliability of Evolutionary Algorithms, the theoretical property of global convergence with a probability of one holds for all variants that use an elitist selection method and guarantee a reachability property of mutation which is basically assured by working with nonzero mutation rate in Genetic Algorithms (respectively with nonzero standard deviation in Evolution Strategies and Evolutionary Programming). These results are summarized in theorem 7, 10, and 13, which are based on the general convergence theorem 3 for global random search algorithms respectively on well-known results on absorbing Markov chains. In contrast to convergence reliability investigations where the focus is on the explorative character of the search, convergence velocity analysis emphasizes the exploitation of information collected about a promising region or point in the search space. Both properties are contradictory and cause a trade-off that dominates behavior and control of Evolutionary Algorithms. Nevertheless, convergence velocity investigations so far were known only for Evolution Strategies (see section 2.1.7) but can easily be transferred to standard Evolutionary Programming as demonstrated in section 2.2.7. The result provides a clear indication that the step-size control of standard EP is useless for even moderately large dimensions of the search space and for objective functions that possess a non-vanishing global optimum. More advanced versions of Evolutionary Programming overcome this problem by a self-adaptive control of strategy parameters quite similar to the technique used in Evolution Strategies.