The Compositional Security Checker: a tool for the verification ofinformation flow security properties

The Compositional Security Checker (CoSeC for short) is a semantic-based tool for the automatic verification of some compositional information flow properties. The specifications given as inputs to CoSeC are terms of the Security Process Algebra, a language suited for the specification of concurrent systems where actions belong to two different levels of confidentiality. The information flow security properties which can be verified by CoSeC are some of those classified in (Focardi and Gorrieri, 1994). They are derived from some classic notions, e.g., noninterference. The tool is based on the same architecture as the Concurrency Workbench, from which some modules have been imported unchanged. The usefulness of the tool is tested with the significant case-study of an access-monitor, presented in several versions in order to illustrate the relative merits of the various information flow properties that CoSeC can check. Finally, we present an application in the area of network security: we show that the theory (and the tool) can be reasonably applied also for singling out security flaws in a simple, yet paradigmatic, communication protocol     

基于DTE策略的安全域隔离Z形式模型

基于DTE策略的安全域隔离技术是构造可信系统的基本技术之一.但现有DTE实现系统存在安全目标不明确、缺乏对系统及其安全性质的形式定义和分析的缺点,导致系统安全性难以得到保证.定义了一个基于DTE策略的安全域隔离模型,采用Z语言形式定义了系统状态、基于信息流分析的不变量和安全状态,并借助Z/EVES工具给出验证系统安全的形式分析方法.解决了DTE系统的形式化建模问题,为安全域隔离技术的实现和验证奠定了基础.     

Language-Emptiness Checking of Alternating Tree Automata Using Symbolic Reachability Analysis

Alternating tree automata and AND/OR graphs provide elegant formalisms that enable branching- time logics to be verified in linear time. The seminal work of Kupferman et al. [Orna Kupferman, Moshe Y. Vardi, and Pierre Wolper. An automata-theoretic approach to branching-time model checking. J. ACM, 47(2):312–360, 2000] showed that 1) branching-time model checking is reducible to the language non-emptiness checking of the product of two alternating automata representing the model and property under verification, and 2) the non-emptiness problem can be solved by performing a search on an AND/OR graph representing this product. Their algorithm, however, can only be implemented in an explicit-state model checker because it needs stacks to detect accept and reject runs. In this paper, we propose a BDD-based approach to check the language non-emptiness of the product automaton. We use a technique called “state recording” from Schuppan and Biere [Viktor Schuppan and Armin Biere. Efficient reduction of finite state model checking to reachability analysis. Int. Journal on Software Tools for Technology Transfer (STTT), 5(2–3):185–204, 2004] to emulate the stack mechanism from explicit-state model checking. This technique allows us to transform the product automaton into a well-defined AND/OR graph. We develop a BDD-based reachability algorithm to efficiently determine whether a solution graph for the AND/OR graph exists and thereby solve the model-checking problem. While “state recording” increases the size of the state space, the advantage of our approach lies in the memory saving BDDs can offer and the potential it opens up for optimisation of the reachability analysis. We remark that this technique always detects the shortest counter-example.     

Using Web resources to construct multilingual medical thesaurus for cross-language medical information retrieval

Due to the language barrier, non-English users are unable to retrieve the most updated medical information from the U.S. authoritative medical websites, such as PubMed and MedlinePlus. However, currently, there is no any cross-language medical information retrieval (CLMIR) system that can help Chinese-speaking consumers cross the language barrier in finding useful English medical information. A few CLMIR systems utilize MeSH (Medical Subject Headings) to help overcome the language barrier. Unfortunately, the traditional Chinese version of MeSH is currently unavailable.In this paper, we employ a semi-automatic term translation method to construct a Chinese–English MeSH by exploiting abundant multilingual Web resources, including Web anchor texts and search–result pages. Through this method, we have developed a Chinese–English Mesh Compilation System to assist knowledge engineers in compiling a Chinese–English medical thesaurus with more than 19,000 entries. Furthermore, this thesaurus has been used to develop a prototypical system for cross-language medical information retrieval, MMODE, which can help consumers retrieve top-quality English medical information using Chinese terms.     

A simplification of a real‐time verification problem

We revisit the problem of real‐time verification with dense‐time dynamics using timeout and calendar‐based models and simplify this to a finite state verification problem. We introduce a specification formalism for these models and capture their behaviour in terms of semantics of timed transition systems. We discuss a technique, which reduces the problem of verification of qualitative temporal properties on infinite state space of a large fragment of these timeout and calender‐based transition systems into that on clock‐less finite state models through a two‐step process comprising of digitization and finitary reduction. This technique enables us to verify safety invariants for real‐time systems using finite state model checking avoiding the complexity of infinite state (bounded) model checking and scale up models without applying techniques from induction‐based proof methodology. In the same manner, we verify timeliness properties. Moreover, we can verify liveness for real‐time systems, which are not possible by using induction with infinite state model checkers. Copyright © 2016 John Wiley & Sons, Ltd.     

χSuds-SDL: A Tool for Testing Software Architecture Specifications

Available statistical data shows that the cost of repairing software faults rises dramatically in later development stages. In particular, the new technology of generating implementation code from architectural specifications requires highly reliable designs. Much research has been done at this stage using verification and validation techniques to prove correctness in terms of certain properties. A prominent approach of this category is model checking (Atlee, J.M., and Gannon, J. 1993. State-based model checking of event-driven systems requirements. IEEE Trans. Software Eng., 19(1): 24–40.) Such approaches and the approach of software testing are complementary. Testing reveals some errors that cannot be easily identified through verification, and vice versa. This paper presents the technology and the accompanying tool suite to the testing of software architecture specifications. We apply our state-of-the-art technology in software coverage testing, program diagnosis and understanding to software architectural designs. Our technology is based on both the control flow and the data flow of the executable architectural specifications. It first generates a program flow diagram from the specification and then automatically analyses the coverage features of the diagram. It collects the corresponding flow data during the design simulation to be mapped to the flow diagram. The coverage information for the original specification is then obtained from the coverage information of the flow diagram. This technology has been used for C, C++, and Java, and has proven effective (Agrawal, H., Alberti, J., Li, J.J., et al. 1998. Mining system tests to aid software maintenance, IEEE Computer July, pp. 64–73.)     

Process expressions and Hoare's logic: Showing an irreconcilability of context-free recursion with Scott's induction rule

In this paper processes specifiable over a non-uniform language are considered. The language contains constants for a set of atomic actions and constructs for alternative and sequential composition. Furthermore it provides a mechanism for specifying processes recursively (including nested recursion). We consider processes as having a state: atomic actions are to be specified in terms of observable behaviour (relative to initial states) and state transformations. Any process having some initial state can be associated with a transition system representing all possible courses of execution. This leads to an operational semantics in the style of Plotkin. The partial correctness assertion {α} p{β} expresses that for any transition system associated with the process p and having some initial state satisfying α, its final states representing successful execution satisfy β. A logic in the style of Hoare, containing a proof system for deriving partial correctness assertions, is presented. This proof system is sound and relatively complete, so any partial correctness assertion can be evaluated by investigating its derivability. Included is a short discussion about the extension of the process language with “guarded recursion”. It appears that such an extension violates the completeness of the Hoare logic. This reveals a remarkable property of Scott's induction rule in the context of non-determinism: only regular recursion allows a completeness result.     

An Algorithm for General Set Unification and Its Complexity

In this paper, an algorithm for set unification – which is a restricted case of the associative-commutative-idempotent (ACI) unification – is presented. The algorithm is able to unify finite sets containing arbitrary terms. It is nondeterministic and can easily be implemented in Prolog. Because of the simplicity of the algorithm, the computation of a single solution is quite fast, and the exact complexity of the algorithm and of the set unification problem itself can be analyzed easily. The algorithm is compared with some other set unification algorithms. All algorithms have single exponential complexity, because the set unification problem is NP-complete, but our exact complexity analysis provides more details. It is shown how the algorithm presented here can be used to solve a generalized set unification problem where sets with tails are admissible. The algorithm can be used in any logic programming language embedding (finite) sets, or in other contexts where set unification is needed, for example, in some unification-based grammar formalisms.     

Design of effective automaton-reduction algorithms for some equivalence relations

The design of fast minimization algorithms of finite automata is considered for two equivalence relations. The design is carried out in formal terms utilizing the properties of the functions used for minimization.Translated from Kibernetika, No. 6, pp. 54–61, November–December, 1989.     

Design and analysis of two stream ciphers based on chaotic coupling and multiplexing techniques

In this paper, we design and implement two new stream ciphers based on Pseudo Chaotic Number Generators (PCNGs) which integrate discrete chaotic maps, namely, Piecewise Linear Chaotic Map (PWLCM), Skewtent and Logistic map. They are weakly coupled by a predefined matrix A for the first PCNG and they are coupled by a binary diffusion matrix D for the second one. Each PCNG includes a chaotic multiplexing technique that allows the enhancement of the robustness of the system. The structure is implemented with finite precision N = 32 bits in C language. Security performance of the proposed stream ciphers is analysed and several cryptanalytic and statistical tests are applied. Experimental results highlight robustness as well as efficiency in terms of computation time of these two stream ciphers.     

A subclass of deterministic context-free languages with a decidable inclusion problem

A new subclass of deterministic context-free languages with a decidable inclusion problem is described in terms of finite automata on the direct product of free semigroups. The decidability proof exploits the structural properties of the automata.Translated from Kibernetika, No. 2, pp. 12–17, March–April, 1990.     

Integration testing of object‐oriented components using finite state machines

In object‐oriented terms, one of the goals of integration testing is to ensure that messages from objects in one class or component are sent and received in the proper order and have the intended effect on the state of the objects that receive the messages. This research extends an existing single‐class testing technique to integration testing of multiple classes. The single‐class technique models the behaviour of a single class as a finite state machine, transforms the representation into a data flow graph that explicitly identifies the definitions and uses of each state variable of the class, and then applies conventional data flow testing to produce test case specifications that can be used to test the class. This paper extends those ideas to inter‐class testing by developing flow graphs, finding paths between pairs of definitions and uses, detecting some infeasible paths and automatically generating tests for an arbitrary number of classes and components. It introduces flexible representations for message sending and receiving among objects and allows concurrency among any or all classes and components. Data flow graphs are stored in a relational database and database queries are used to gather def‐use information. This approach is conceptually simple, mathematically precise, quite powerful and general enough to be used for traditional data flow analysis. This testing approach relies on finite state machines, database modelling and processing techniques and algorithms for analysis and traversal of directed graphs. The paper presents empirical results of the approach applied to an automotive system. This work was prepared by U.S. Government employees as part of their official duties and is, therefore, a work of the U.S. Government and not subject to copyright. Published in 2006 by John Wiley & Sons, Ltd.     

Performance analysis of a mobile agent prototype system based on VIRGO P2P protocols

The mobile agent technique has been broadly used in next generation distributed systems. The system performance measurement and simulation are required before the system can be deployed on a large scale. In this paper, we address performance analysis on a finite state mobile agent prototype on the basis of Virtual Hierarchical Tree Grid Organizations (VIRGO). The finite states refer to the migration, execution, and searching of the mobile agent. We introduce a novel evaluation model for the finite state mobile agent. The experimental results based on this evaluation model show that the finite mobile agents can perform well under multiple agent conditions and are superior to the traditional client/server approach. Copyright © 2013 John Wiley & Sons, Ltd.     

A Temporal Logic for Proving Properties of Topologically General Executions

We present a generalization of the temporal propositional logic of linear time which is useful for stating and proving properties of the generic execution sequence of a parallel program or a non-deterministic program. The formal system we present is exactly that same as the third of three logics presented by Lehmann and Shelah (Information and Control53, 165–198 (1982)), but we give it a different semantics. The models are tree models of arbitrary size similar to those used in branching time temporal logic. The formulation we use allows us to state properties of the “co-meagre” family of paths, where the term “co-meagre” refers to a set whose complement is of the first category in Baire's classification looking at the set of paths in the model as a metric space. Our system is decidable, sound, and, complete for models of arbitrary size, but it has the finite model property; namely, every sentence having a model has a finite model.     

On Probabilistic Techniques for Data Flow Analysis

We present a semantics-based technique for analysing probabilistic properties of imperative programs. This consists in a probabilistic version of classical data flow analysis. We apply this technique to pWhile programs, i.e programs written in a probabilistic version of a simple While language. As a first step we introduce a syntax based definition of a linear operator semantics (LOS) which is equivalent to the standard structural operational semantics of While. The LOS of a pWhile program can be seen as the generator of a Discrete Time Markov Chain and plays a similar role as a collecting or trace semantics for classical While. Probabilistic Abstract Interpretation techniques are then employed in order to define data flow analyses for properties like Parity and Live Variables.     

A Single-Server Queueing System with Background Customers

A single-server queueing system with a Markov flow of primary customers and a flow of background customers from a bunker containing unbounded number of customers, i.e., the background customer flow is saturated, is studied. There is a buffer of finite capacity for primary customers. Service processes of primary as well as background customers are Markovian. Primary customers have a relative service priority over background customers, i.e., a background customer is taken for service only if the buffer is empty upon completion of service of a primary customer. A matrix algorithm for computing the stationary state probabilities of the system at arbitrary instants and at instants of arrival and completion of service of primary customers is obtained. Main stationary performance indexes of the system are derived. The Laplace—Stieltjes transform of the stationary waiting time distribution for primary customers is determined.__________Translated from Avtomatika i Telemekhanika, No. 6, 2005, pp. 74–88.Original Russian Text Copyright © 2005 by Bocharov, Shlumper.