Erratum to: R. Gorrieri and H. Wehrheim (Eds.) Formal Methods for Open Object-Based Distributed Systems DOI: 10.1007/978-3-540-34895-5 The book was inadvertently published with an incorrect name of the copyright holder. The name of the copyright holder for this book is: © IFIP International Federation for Information Processing. The book has been updated with the changes.
Runtime security policy enforcement systems are crucial to limit the risks associated with running untrustworthy (malicious or buggy) code. The inlined reference monitor approach to policy enforcement, pioneered by Erlingsson and Schneider, implements runtime enforcement through program rewriting: security checks are inserted inside untrusted programs. Ensuring complete mediation – the guarantee that every security-relevant event is actually intercepted by the monitor – is non-trivial when the program rewriter operates on an object-oriented intermediate language with state-of-the-art features such as virtual methods and delegates. This paper proposes a caller-side rewriting algorithm for MSIL – the bytecode of the .NET virtual machine – where security checks are inserted around calls to security-relevant methods. We prove that this algorithm achieves sound and complete mediation and transparency for a simplified model of MSIL, and we report on our experiences with the implementation of the algorithm for full MSIL.
Concurrent programming in object-oriented languages is a notoriously difficult task. We propose coboxes – a novel language concept which combines and generalizes active objects and techniques for heap structuring. CoBoxes realize a data-centric approach that guarantees mutual-exclusion for groups of objects. This is important for more complex data structures with invariants ranging over several objects. CoBoxes support multiple entry objects, several cooperating tasks in a cobox, and nesting of coboxes for composition and internal parallelism. Communication between coboxes is handled by asynchronous method calls with futures, which is in particular suitable for distributed programming. In this paper, we explain how aspects of concurrent programming can be solved by coboxes. We develop a core language for coboxes and present a formal operational semantics for this language.
In this work, novel symbolic step encodings of the transition relation for object based communicating state machines are presented. This class of systems is tailored to capture the essential data manipulation features of UML state machines when enriched with a Java-like object oriented action language. The main contribution of the work is the generalization of the $\exists$ -step semantics approach, which Rintanen has used for improving the efficiency of SAT based AI planning, to a much more complex class of systems. Furthermore, the approach is extended to employ a dynamic notion of independence. To evaluate the encodings, UML state machine models are automatically translated into NuSMV models and then symbolically model checked with NuSMV. Especially in bounded model checking (BMC), the $\exists$ -step semantics often significantly outperforms the traditional interleaving semantics without any substantial blowup in the BMC encoding as a SAT formula.
The distributed information systems we use every day are becoming more complex and interconnected. Can we trust them with our information? Currently there is no good way to check that distributed software uses information securely, even if we have the source code. Many mechanisms are available, but are error-prone: for example, encryption, various cryptographic protocols, access control, and replication. But it is hard to know when we are using these mechanisms in a way that correctly enforces application security requirements. This talk describes a higher-level approach to programming secure systems. Instead of using security mechanisms directly, the programming language incorporates explicit security policies specifying the confidentiality, integrity, and availability of information. The compiler then automatically transforms the source code to run securely on the available host machines, and uses a variety of security mechanisms in order to satisfy security policies. The result is systems that are secure by construction. We look at two applications of this approach: building secure web applications using partitioning beween clients and servers, and building more general secure systems by synthesizing fault-tolerance protocols for availability. Joint work with Steve Chong, Jed Liu, Nate Nystrom, Xin Qi, K. Vikram, Steve Zdancewic, Lantian Zheng, and Xin Zheng.
Service-oriented computing is calling for novel computational models and languages with primitives for client-server interaction, orchestration and unexpected events handling. We present CaSPiS, a process calculus where the notions of session and pipelining play a central role. Sessions are two-sided and can be equipped with protocols executed by each side. Pipelining permits orchestrating the flow of data produced by different sessions. The calculus is also equipped with operators for handling (unexpected) termination of the partner's side of a session. Several examples are presented to provide evidence for the flexibility of the chosen set of primitives. Our main result shows that in CaSPiSit is possible to program a "graceful termination" of nested sessions, which guarantees that no session is forced to hang forever after the loss of its partner.
The local minimum spanning tree (LMST) topology control protocol tries to maintain connectivity in an ad-hoc wireless sensor network while minimizing power consumption and maximizing data bandwidth. Our formal, statistical model checking analysis of LMST under realistic deployment conditions shows that the invariant of maintaining network connectivity is easily lost. We then propose a formally-based system redesign methodology in which quantitative temporal logic formulas and further statistical model checking can be used to identify the causes of bugs, and to reach a correct system redesign. We show this methodology effective in the redesign of a version of LMST that ensures network connectivity under realistic deployment conditions.
This paper presents a minimal and complete set of structural refactoring rules for the Object-Z specification language that allow for the derivation of arbitrary object-oriented architectures. The rules are equivalence preserving and work in concert with existing class refinement theory, so that any design derived using the rule set can be shown to be equivalent to, or a refinement of, the original specification.
The complexity of middleware leads to complex Application Programming Interfaces (APIs) and semantics, supported by configurable components in the middleware. Those components are selected to provide the desired semantics. Yet, incorrect configuration can lead to faulty middleware executions, detected late in the development cycle.We use formals methods to tackle this problem. They allow us to find appropriate composition of middleware components and the use of their APIs, and to detect valid or faulty sequences. To provide reusable results, we modeled a canonical middleware architecture using Z.We propose a validation scenario to verify middleware's invariants. We define invariants to exhibit inconsistent usage of these APIs. The specification has been checked with the Z/EVES [13] theorem prover.
This paper proposes a semantics-based automatic null pointer analysis for inferring non-null annotations of fields in object-oriented programs. The analysis is formulated for a minimalistic OO language and is expressed as a constraint-based abstract interpretation of the program which for each field of a class infers whether the field is definitely non-null or possibly null after object initialization. The analysis is proved correct with respect to an operational semantics of the minimalistic OO language. This correctness proof has been machine checked using the Coq proof assistant. We also prove the analysis complete with respect to the non-null type system proposed by Fähndrich and Leino, in the sense that for every typable program the analysis is able to prove the absence of null dereferences without any hand-written annotations. Experiments with a prototype implementation of the analysis show that the inference is feasible for large programs.
We analyse the relationship between object-oriented modelling and session-based, service-oriented modelling, starting from a typical UML Sequence Diagram and providing a program transformation into a service-oriented model. We also provide a similar transformation from session-based specifications into request-response specifications. All transformations are specified in SSCC--a process calculus for modelling and analysing service-oriented systems--and proved correct with respect to a suitable form of behavioural equivalence (full weak bisimilarity). Since the equivalence is proved to be compositional, results remain valid in arbitrary contexts.
Software product line engineering combines the individual developments of systems to the development of a family of systems consisting of common and variable assets.In this paper we introduce the process algebra PL-CCS as a product line extension of CCS and show how to model the overall behavior of an entire family within PL-CCS. PL-CCS models incorporate behavioral variability and allow the derivation of individual systems in a systematic way due to a semantics given in terms of multi-valued modal Kripke structures. Furthermore, we introduce multi-valued modal μ-calculus as a property specification language for system families specified in PL-CCS and show how model checking techniques operate on such structures. In our setting the result of model checking is no longer a simple yesor noanswer but the set of systems of the product line that do meet the specified properties.
Current research on verifying security properties of communication protocols has focused on proving integrity and confidentiality using models that include a strong Man-in-the-Middle (MitM) threat. By contrast, protection measures against Denial-of-Service (DoS) must assume a weaker model in which an adversary has only limited ability to interfere with network communications. In this paper we demonstrate a modular reasoning framework in which a protocol 𝒫 that satisfies certain security properties can be assured to retain these properties after it is “wrapped” in a protocol 𝒲[𝒫] that adds DoS protection. This modular wrapping is based on the “onion skin” model of actor reflection. In particular, we show how a common DoS protection mechanism based on cookies can be applied to a protocol while provably preserving safety properties (including confidentiality and integrity) that it was shown to have in a MitM threat model.
Termination analysis has received considerable attention, traditionally in the context of declarative programming, and recently also for imperative languages. In existing approaches, termination is performed on source programs. However, there are many situations, including mobile code, where only the compiled code is available. In this work we present an automatic termination analysis for sequential Java Bytecode programs. Such analysis presents all of the challenges of analyzing a low-level language as well as those introduced by object-oriented languages. Interestingly, given a bytecode program, we produce a constraint logicprogram, CLP, whose termination entails termination of the bytecode program. This allows applying the large body of work in termination of CLP programs to termination of Java bytecode. A prototype analyzer is described and initial experimentation is reported.
Reasoning about object-oriented programs is hard, due to aliasing, dynamic binding and the need for data abstraction and framing. Reasoning about concurrent object-oriented programs is even harder, since in general interference by other threads has to be taken into account at each program point. In this paper, we propose an approach to the automatic verification of concurrent Java-like programs. The cornerstone of the approach is a programming model, a set of rules, which limits thread inference to synchronization points such that one can reason sequentially about most code. In particular, programs conforming to the programming model are guaranteed to be data race free. Compared to previous incarnations of the programming model, our approach is more flexible in describing the set of memory locations protected by an object’s lock. In addition, we combine the model with an approach for data abstraction and framing based on dynamic frames. To the best of our knowledge, this is the first paper combining dynamic frames and concurrency. We implemented the approach in a tool, called VeriCool, and used it to verify several small concurrent programs.
Distributed algorithms are inherently complex to verify. In this paper we show how to verify that a concurrent lock-free implementation of a stack is correct by mechanizing the proof that it is linearizable, linearizability being a correctness notion for concurrent objects. Our approach consists of two parts: the first part is independent of the example and derives proof obligations local for one process which imply linearizabilty. The conditions establish a (special sort of non-atomic) refinement relationshipbetween the specification and the concurrent implementation. These are used in the second part to verify the lock-free stack implementation. We use the specification language Z to describe the algorithms and the KIV theorem prover to mechanize the proof.
The success of distributed event-based infrastructures such as SIENA and Elvin is partially due to their ease of use. Even novice users of these infrastructures not versed in distributed programming can quickly comprehend the small and intuitive interfaces that these systems typically feature. However, if these users make incorrect assumptions about how the infrastructure services work, a mismatch between the infrastructure and its client applications occurs, which may manifest itself in erroneous client behaviour. We propose a framework for automatically model checking distributed event-based systems in order to discover mismatch between the infrastructure and its clients. Using the SIENA event service as an example, we implemented and evaluated our framework by customizing the Bandera/Bogor tool pipeline. Two realistic Java applications are implemented to test and evaluate the framework.
Refactoring is a method for improving the structure of programs/ specifications as to enhance readability, modularity and reusability. Refactorings are required to be behaviour-preserving in that - to an external observer - no difference between the program before and after refactoring is visible. In this paper, we develop refactorings for an object-oriented specification formalism combining a state-based language (Object-Z) with a process algebra (CSP). In contrast to OO-programming languages, refactorings moving methods or attributes up and down the class hierarchy, in addition, need to change CSP processes. We formally prove behaviour preservation with respect to the failures-divergences model of CSP.
The Pict programming language is an implementation of the π-calculus in which executions of π-calculus terms are specified via an abstract machine. An important property of any concurrent programming language implementation is the fair execution of threads. After defining fairness for the π-calculus, we show that Pict abstract machine executions implement fair π-calculus executions. We also give new proofs of soundness and liveness for the Pict abstract machine.
