An Analysis of Operation-Refinement in an Abortive Paradigm

This paper begins a new strand of investigation which complements our previous investigation of refinement for specifications whose semantics is given by partial relations (using Z as a linguistic vehicle for this semantics). It revolves around extending our mathematical apparatus so as to continue our quest for examining mathematically the essence of the lifted-totalisation semantics (which underlies the de facto standard notion of refinement in Z) and the role of the semantic elements in model-theoretic refinement, but this time in the abortive paradigm. We conside the simpler framework of operation-refinement and, thus, (at least at this stage) abstract from the complications emerging when data simulations are involved: we examine the (de facto) standard account of operation-refinement in this regime by introducing a simpler, normative theory (SP-refinement) which captures the notion of firing conditions refinement directly in the language and in terms of the natural properties of preconditions and postconditions; we then summarise our observations and link them to the particular role each of the possible extreme specifications in Z plays in the abortive paradigm - this lays the foundations to a more intricate future investigation of data-refinement in this paradigm. We conclude by providing a detailed account of future work which generalises Miarka, Boiten and Derrick's work of combining the abortive and chaotic paradigms for refinement, in our mathematical framework of and .     

An analysis of refinement in an abortive paradigm

This paper presents a new strand of investigation which complements our previous investigation of refinement for specifications whose semantics is given by partial relations (using Z as a linguistic vehicle for this semantics). It revolves around extending our mathematical apparatus so as to continue our quest for examining mathematically the essence of the lifted-totalisation semantics (which underlies the de facto standard notion of refinement in Z) and the role of the semantic elements in model-theoretic refinement, but this time in the abortive paradigm. The analysis is given in two salient parts. In the first part, we consider the simpler framework of operation-refinement: we examine the (de facto) standard account of operation-refinement in this regime by introducing a simpler, normative theory which captures the notion of firing-conditions refinement directly in the language and in terms of the natural properties of preconditions and postconditions. In the second part, we generalise our analysis to a more intricate investigation of simulation-based data-refinement. The proof-theoretic approach we undertake in the formal analysis provides us with a mathematical apparatus which enables us to examine precisely the relationships amongst the various theories of refinement. This enables us to examine the general mathematical role that the values play in model-theoretic refinement in the abortive paradigm, as well as the significance of the unique interaction of these values with the notions of lifting (of data simulations) and lifted-totalisation (of operations) in this regime. Furthermore, we generalise this mathematical analysis to a more conceptual one which also involves extreme specifications.     

A process algebraic framework for specification and validation of real-time systems

Following the trend to combine techniques to cover several facets of the development of modern systems, an integration of Z and CSP, called Circus, has been proposed as a refinement language; its relational model, based on the unifying theories of programming (UTP), justifies refinement in the context of both Z and CSP. In this paper, we introduce Circus Time, a timed extension of Circus, and present a new UTP time theory, which we use to give semantics to Circus Time and to validate some of its laws. In addition, we provide a framework for validation of timed programs based on FDR, the CSP model-checker. In this technique, a syntactic transformation strategy is used to split a timed program into two parallel components: an untimed program that uses timer events, and a collection of timers. We show that, with the timer events, it is possible to reason about time properties in the untimed language, and so, using FDR. Soundness is established using a Galois connection between the untimed UTP theory of Circus (and CSP) and our time theory.     

Automatically Detecting and Visualising Errors in UML Diagrams

UML has become the de facto standard for object-oriented modelling. Currently, UML comprises several different notations with no formal semantics attached to the individual diagrams or their integration, thus preventing rigorous analysis of the diagrams. Previously, we developed a formalisation framework that attaches formal semantics to a subset of UML diagrams used to model embedded systems. This paper describes automated structural and behavioural analyses applicable to UML diagrams using our formalisation framework. In addition to intra- and inter-diagram consistency checks, we discuss how simulation and model checking can be used in tandem for behavioural analysis of the UML diagrams. Our tools also visually interpret the analysis results in terms of the original UML diagrams, thereby facilitating their correction and refinement. We illustrate these capabilities through the modelling and analysis of UML diagrams for an automotive industrial case study. Correspondence and offprint requests to: Dr B. Cheng, Software Engineering and Network Systems Laboratory, Department of Computer Science and Engineering, Michigan State University, 3115 Engineering Building, East Lansing, MI 48824, USA. Tel.: +1 517 355 8344; Fax: +1 517 432 1061; Email: chengb@cse.msu.edu     

Local abstraction–refinement for the <Emphasis Type="Italic">μ</Emphasis>-calculus

A key technique for the verification of programs is counterexample-guided abstraction–refinement (CEGAR). Grumberg et al. (LNCS, vol 3385, pp. 233–249. Springer, Berlin, 2005; Inf Comput 205(8):1130–1148, 2007) developed a CEGAR-based algorithm for the modal μ-calculus. There, every abstract state is split in a refinement step. In this paper, the work of Grumberg et al. is generalized by presenting a new CEGAR-based algorithm for the μ-calculus. It is based on a more expressive abstract model and applies refinement only locally (at a single abstract state), i.e., the lazy abstraction technique for safety properties is adapted to the μ-calculus. Furthermore, it separates refinement determination from the (3-valued based) model checking. Three different heuristics for refinement determination are presented and illustrated.     

Strongly secure identity-based authenticated key agreement protocols in the escrow mode

Escrowable identity-based authenticated key agreement(AKA) protocols are desirable under certain circumstances especially in certain closed groups applications.In this paper,we focus on two-party identitybased AKA schemes in the escrow mode,and present a strongly secure escrowable identity-based AKA protocol which captures all basic desirable security properties including perfect forward secrecy,ephemeral secrets reveal resistance and so on.The protocol is provably secure in the extended Canetti-Krawczyk model,and its security can be reduced to the standard computational bilinear Diffie-Hellman assumption in the random oracle model.Assuming no adversary can obtain the master private key for the escrow mode,our scheme is secure as long as each party has at least one uncompromised secret.Also,we present two strongly secure variants of the protocol,which are computationally more efficient than the original scheme.     

A Per Model of Secure Information Flow in Sequential Programs

This paper proposes an extensional semantics-based formal specification of secure information-flow properties in sequential programs based on representing degrees of security by partial equivalence relations (pers). The specification clarifies and unifies a number of specific correctness arguments in the literature and connections to other forms of program analysis. The approach is inspired by (and in the deterministic case equivalent to) the use of partial equivalence relations in specifying binding-time analysis, and is thus able to specify security properties of higher-order functions and partially confidential data. We also show how the per approach can handle nondeterminism for a first-order language, by using powerdomain semantics and show how probabilistic security properties can be formalised by using probabilistic powerdomain semantics. We illustrate the usefulness of the compositional nature of the security specifications by presenting a straightforward correctness proof for a simple type-based security analysis.     

Magic-sets for localised analysis of Java bytecode

Static analyses based on denotational semantics can naturally model functional behaviours of the code in a compositional and completely context and flow sensitive way. But they only model the functional i.e., input/output behaviour of a program P, not enough if one needs P’s internal behaviours i.e., from the input to some internal program points. This is, however, a frequent requirement for a useful static analysis. In this paper, we overcome this limitation, for the case of mono-threaded Java bytecode, with a technique used up to now for logic programs only. Namely, we define a program transformation that adds new magic blocks of code to the program P, whose functional behaviours are the internal behaviours of P. We prove the transformation correct w.r.t. an operational semantics and define an equivalent denotational semantics, devised for abstract interpretation, whose denotations for the magic blocks are hence the internal behaviours of P. We implement our transformation and instantiate it with abstract domains modelling sharing of two variables, non-cyclicity of variables, nullness of variables, class initialisation information and size of the values bound to program variables. We get a static analyser for full mono-threaded Java bytecode that is faster and scales better than another operational pair-sharing analyser. It has the same speed but is more precise than a constraint-based nullness analyser. It makes a polyhedral size analysis of Java bytecode scale up to 1300 methods in a couple of minutes and a zone-based size analysis scale to still larger applications.     

Set based logic programming

In a previous paper (Blair et al. 2001), the authors showed that the mechanism underlying Logic Programming can be extended to handle the situation where the atoms are interpreted as subsets of a given space X. The view of a logic program as a one-step consequence operator along with the concepts of supported and stable model can be transferred to such situations. In this paper, we show that we can further extend this paradigm by creating a new one-step consequence operator by composing the old one-step consequence operator with a monotonic idempotent operator (miop) in the space of all subsets of X, 2 ^X . We call this extension set based logic programming. We show that such a set based formalism for logic programming naturally supports a variety of options. For example, if the underlying space has a topology, one can insist that the new one-step consequence operator always produces a closed set or always produces an open set. The flexibility inherent in the semantics of set based logic programs is due to both the range of natural choices available for specifying the semantics of negation, as well as the role of monotonic idempotent operators (miops) as parameters in the semantics. This leads to a natural type of polymorphism for logic programming, i.e. the same logic program can produce a variety of outcomes depending on the miop associated with the semantics. We develop a general framework for set based programming involving miops. Among the applications, we obtain integer-based representations of real continuous functions as stable models of a set based logic program.      

Gaussian Laws for the Main Parameters of the Euclid Algorithms

We provide sharp estimates for the probabilistic behaviour of the main parameters of the Euclid Algorithms, both on polynomials and on integer numbers. We study in particular the distribution of the bit-complexity which involves two main parameters: digit-costs and length of remainders. We first show here that an asymptotic Gaussian law holds for the length of remainders at a fraction of the execution, which exhibits a deep regularity phenomenon. Then, we study in each framework—polynomials (P) and integer numbers (I)—two gcd algorithms, the standard one (S) which only computes the gcd, and the extended one (E) which also computes the Bezout pair, and is widely used for computing modular inverses. The extended algorithm is more regular than the standard one, and this explains that our results are more precise for the Extended algorithm: we exhibit an asymptotic Gaussian law for the bit-complexity of the extended algorithm, in both cases (P) and (I). We also prove that an asymptotic Gaussian law for the bit-complexity of the standard gcd in case (P), but we do not succeed obtaining a similar result in case (I). The integer study is more involved than the polynomial study, as it is usually the case. In the polynomial case, we deal with the central tools of the distributional analysis of algorithms, namely bivariate generating functions. In the integer case, we are led to dynamical methods, which heavily use the dynamical system underlying the number Euclidean algorithm, and its transfer operator. Baladi and Vallée (J. Number Theory 110(2):331–386, 2005) have recently designed a general framework for “distributional dynamical analysis”, where they have exhibited asymptotic Gaussian laws for a large family of parameters. However, this family does not contain neither the bit-complexity cost nor the size of remainders, and we have to extend their methods for obtaining our results. Even if these dynamical methods are not necessary in case (P), we explain how the polynomial dynamical system can be also used for proving our results. This provides a common framework for both analyses, which well explains the similarities and the differences between the two cases (P) and (I), for the algorithms themselves, and also for their analysis. An extended abstract of this paper can be found in Lhote and Vallée (Proceedings of LATIN’06, Lecture Notes in Computer Science, vol. 3887, pp. 689–702, 2006).     

Formal methods for security in the Xenon hypervisor

This paper reports on the Xenon project’s use of formal methods. Xenon is a higher-assurance secure hypervisor based on re-engineering the Xen open-source hypervisor. The Xenon project used formal specifications both for assurance and as guides for security re-engineering. We formally modelled the fundamental definition of security, the hypercall interface behaviour, and the internal modular design. We used three formalisms: CSP, Z, and Circus for this work. Circus is a combination of Standard Z, CSP with its semantics given in Hoare and He’s unifying theories of programming. Circus is suited for both event-based and state-based modelling. Here, we report our experiences to date with using these formalisms for assurance.     

Mechanised support for sound refinement tactics

ArcAngel is a tactic language devised to facilitate and automate program developments using Morgan’s refinement calculus. It is especially well suited for the specification of high-level refinement strategies, and equipped with a formal semantics that additionally permits reasoning about tactics. In this paper, we present an implementation of ArcAngel for the ProofPower theorem prover. We discuss the underlying design, explain how it implements the semantics of ArcAngel, and examine the interplay between ArcAngel tactics and the native reasoning support of the prover. We also discuss several extensions of ArcAngel that have been entailed by our implementation effort. They are of practical importance and provide a unification of the related tactic languages Angel and ArcAngel C. Our main result is a mechanisation that reflects directly the ArcAngel semantics, and can be used with any programming model for refinement. The approach can be used to support other formal tactic languages using other theorem provers.     

Compositional noninterference from first principles

The recently formulated Shadow Semantics for noninterference-style security of sequential programs avoids the Refinement Paradox by preserving demonic nondeterminism in those cases where reducing it would compromise security. The construction (originally) of the semantic domain for The Shadow, and the interpretation of programs in it, relied heavily on intuition, guesswork and the advice of others. That being so, it is natural after the fact to try to reconstruct an idealised “inevitable” path from first principles to where we actually ended up: not only does one learn (more) about semantic principles by doing so, but the “rational reconstruction” helps to expose the choices made, along the way, and to legitimise the decisions that resolved them. Unlike our other papers on noninterference, this one does not contain a significant case study: instead its aim is to provide the most accessible account we can of the methods we use and why our model, in its details, has turned out the way it has. In passing, it might give some insight into the general role and significance of compositionality and testing-with-context for program semantics. Finally, a technical contribution here is a new “Transfer Principle” that captures uniformly a large class of classical refinements that remain valid when noninterference is taken into account in our style.     

Information-flow control on ARM and POWER multicore processors

Weak memory models implemented on modern multicore processors are known to affect the correctness of concurrent code. They can also affect whether or not the concurrent code is secure. This is particularly the case in programs where the security levels of variables are value-dependent, i.e., depend on the values of other variables. In this paper, we illustrate how instruction reordering allowed by ARM and POWER multicore processors leads to vulnerabilities in such programs, and present a compositional, flow-sensitive information-flow logic which can be used to detect such vulnerabilities. The logic allows step-local reasoning (one instruction at a time) about a thread’s security by tracking information about dependencies between instructions which guarantee their order of occurrence. Program security can then be established from individual thread security using rely/guarantee reasoning. The logic has been proved sound with respect to existing operational semantics using Isabelle/HOL, and implemented in an automatic symbolic execution tool.

     

Comparing Syntactic and Semantic Action Refinement

The semantic definition of action refinement on labelled configuration structures is compared with the notion ofsyntactic substitution, which can be used as another notion of action refinement in a process algebraic setting. The comparison is done by studying a process algebra equipped with sequential composition, parallel composition with an explicit synchronisation set, and an operator for action refinement. On the one hand, the language (including the refinement operator) is given a configuration structure semantics. On the other hand, a reduction procedure transforms a process termPinto aflatterm (i.e., with the refinement operator not occurring in it)red(P) by means of syntactic substitution, defined in a structural inductive way. The main aim of the paper is to investigate general conditions under which the termsPandred(P) have the same semantics. The results we present are essentially dependent on the question whether the refined action can be synchronised or not. In the latter case,Pandred(P) give rise to isomorphic configuration structures under mild assumptions. The former case is considerably more difficult, since then refinement cannot be expected to distribute over parallel composition. We give necessary and sufficientsemanticconditions under which distribution still holds up to semantic equivalence. Subsequently, we also give sufficient (but not necessary)syntacticconditions for reducible terms. Finally, we generalise these results to a language with recursion.     

A trace-based service semantics guaranteeing deadlock freedom

We revise the accordance preorder in the context of deadlock freedom for asynchronously communicating services. Accordance considers all controllers of a service—that is, all environments that can interact with the service without deadlocking. A service Impl accords with a service Spec if every controller of Spec is also a controller of Impl. We model finite-state and infinite-state services as Petri nets and formalize the semantics of such models with a traditional concurrency semantics, a trace-based semantics. As benefits, we get an easier characterization of the accordance preorder, prove that it is a fully abstract precongruence, and present an algorithm to decide refinement of two finite-state services. Previously, operating guidelines have been introduced to study the behavior of finite-state services; they characterize all controllers of a given service and can be used to decide accordance. An operating guideline is a finite automaton annotated with Boolean formulae that describes the semantics of a service from the perspective of its controllers rather than from the perspective of the service. We show that our trace-based semantics can be translated back and forth into operating guidelines, thereby providing a more conceptual understanding of operating guidelines.     

Using transition set sequences to partition behaviors of petri nets

The transition set semantics (Wang and Jiao, LNCS 6128:84–103, 2010) partitions the Petri net behaviors in a canonical way such that behaviors in an equivalence class have the same canonical transition set sequence. This article extends the semantics in two ways: firstly, the semantics is parameterized by the basic relation on the structural transitions to define different variants; secondly, the semantics for the infinite firing sequences of the net is defined. We prove that these extensions still preserve the well-definedness, soundness and completeness of the semantics. Furthermore, we show how to recognize some infinite sequences called back-loops in the view of this new semantics.     

Modeling security-relevant data semantics

The use of an extended data model which represents both integrity and secrecy aspects of data is demonstrated. This Semantic Data Model for Security (SDMS) provides a technique that assists domain experts, security officers, and database designers in first understanding their security requirements, and then translating them into a good database design. Identifying security requirements at this semantic level provides the basis for analyzing the security requirements and the database design for inference and signaling vulnerabilities. Another contribution is a comprehensive taxonomy of security-relevant data semantics that must be captured and understood to implement a multilevel secure automated information system     

Formal logical language to set requirements for secure code execution

Presently, a special attention is paid to the problem of information security when designing and using objects of critical information infrastructure. One of the most common approaches used to secure the information processed on these objects is the creation of an isolated program environment (sandbox). The security of the environment is determined by its invariability. However, the evolutionary development of data processing systems makes it necessary to implement new components and software in this environment on the condition that the security requirements are met. In this case, the most important requirement is trust in a new program code. This paper is devoted to developing a formal logical language to describe functional requirements for program code that allows one to impose further constraints at the stage of static analysis, as well as to control their fulfillment in dynamics.