Information Flow Security for Boxed Ambients

We study the problem of secure information flow for Boxed Ambients in terms of non-interference. We develop a sound type system that provides static guarantees of absence of unwanted flow of information for well typed processes. Non-interference is stated, and proved, in terms of a typed notion of contextual equivalence for Boxed Ambients akin to the corresponding equivalence defined for Mobile Ambients.     

Guardians for Ambient-Based Monitoring

In the Mobile Ambients of Cardelli and Gordon an ambient is a unit for mobility, which may contain processes (data) and sub-ambients. Since the seminal work of Cardelli and Gordon, several ambient-based calculi have been proposed (Seal, Box-π, Safe Ambients, Secure Safe Ambients, Boxed Ambients), mainly for supporting security. At the operational level these (box- and) ambient-based calculi differ only in the capabilities of processes. We propose a way of extending ambient-based calculi, which embodies two principles: an ambient is a unit for monitoring and coordination, the name of an ambient determines its (monitoring and coordination) policy. More specifically, to each ambient we attach a guardian, which monitors the activity of sub-components (i.e. processes and sub-ambients) and the interaction with the external environment. In our proposal, guardians and processes play a dual role: guardians are centralized entities monitoring and inhibiting actions, while processes are decentralized entities performing actions. We exemplify the use of guardians for enforcing security properties.     

Leader Election in Rings of Ambient Processes

Palamidessi has shown that the π-calculus with mixed choice is powerful enough to solve the leader election problem on a symmetric ring of processes. We show that this is also possible in the calculus of Mobile Ambients (MA), without using communication or restriction. Following Palamidessi's methods, we deduce that there is no encoding satisfying certain conditions from MA into CCS. We also show that the calculus of Boxed Ambients is more expressive than its communication-free fragment.     

The Calculus of Context-aware Ambients

We present the Calculus of Context-aware Ambients (CCA in short) for the modelling and verification of mobile systems that are context-aware. This process calculus is built upon the calculus of mobile ambients and introduces new constructs to enable ambients and processes to be aware of the environment in which they are being executed. This results in a powerful calculus where both mobility and context-awareness are first-class citizens. We present the syntax and a formal semantics of the calculus. We propose a new theory of equivalence of processes which allows the identification of systems that have the same context-aware behaviours. We prove that CCA encodes the π-calculus which is known to be a universal model of computation. Finally, we illustrate the pragmatics of the calculus through many examples and a real-world case study of a context-aware hospital bed.     

Fair ambients

Based on an analysis of the capability operators of the Calculus of Mobile Ambients, three fairness principles are proposed to safeguard the interactions of the ambients. The Calculus of Fair Ambient is designed to meet these fairness principles. A labeled transition semantics for the calculus is defined to support structural investigation. The bisimulation theory of the fair ambients is studied and two coincidence results are established. An expressiveness result of the calculus is formally established by proving that it contains the pi calculus as a sub-calculus.     

A typed encoding of boxed into safe ambients

We present: (i) an encoding of Boxed Ambients into a variant of Safe Ambients; and (ii) a new type system for multi-level security of Safe Ambients in the style of Cardelli et al. (Information and Computation 177(2), 160–194 (2002)) and Dezani-Ciancaglini and Salvo (Security types for mobile safe ambients. In: Proceedings of ASIAN '00, LNCS 1961, pp. 215–236. Springer Verlag (2000)). Then, we show that the types, when applied to the encoded BA proceses, permits to accurately verify Mandatory Access Control policies of the source processes.     

Refusal testing

When manipulating concurrent processes it is desirable to suppress their internal details and to consider two processes to be equivalent if their external behaviours are equivalent. Following Milner and De Nicola & Hennessy we take this external equivalence to mean that an observer cannot tell the processes apart by testing their responses to the same stimuli. We introduce a form of testing (refusal testing) which is more powerful than that of De Nicola & Hennessy in that the observer not only tests whether a process will perform an action but is also allowed under certain circumstances to discover in a finite amount of time that the process will not perform an action. The equivalence associated with refusal testing is compared with De Nicola & Hennessy's testing equivalence and Milner's observation equivalence, and a sound and complete proof system is provided for refusal equivalence when applied to CCS processes.     

Stochastic Ambient Calculus

Mobile Ambients (MA) have acquired a fundamental role in modelling mobility in systems with mobile code and mobile devices, and in computation over administrative domains. We present the stochastic version of Mobile Ambients, called Stochastic Mobile Ambients (SMA), where we extend MA with time and probabilities. Inspired by previous models, PEPA and Sπ, we enhance the prefix of the capabilities with a rate and the ambient with a linear function that operates on the rates of processes executing inside it. The linear functions associated with ambients represent the delays that govern particular administrative domains. We derive performance measures from the labelled transition semantics as in standard models. We also define a strong Markov bisimulation in the style of reduction semantics known as barbed bisimulation. We argue that performance measures are of vital importance in designing any kind of distributed system, and that SMA can be useful in the design of the complicated mobile systems.     

On abstract interpretation of Mobile Ambients

We introduce an abstract interpretation framework for Mobile Ambients, based on a new semantics called normal semantics. Then, we derive within this setting two analyses computing a safe approximation of the run-time topological structure of processes. Such a static information can be successfully used to establish interesting security properties.     

Algebraic theory of probabilistic processes

In this paper we extend de Nicola and Hennessy’s testing theory to deal with probabilities. We say that two processes are testing equivalent if the probabilities with which they pass any test are equal. We present three alternative semantic views of our testing equivalence. First, we introduce adequate extensions of acceptance sets (inducing an operational characterization) and acceptance trees (inducing a denotational semantics). We also present a sound and complete axiomatization of our testing equivalence. So, this paper represents a complete study of the adaptation of the classical testing theory for probabilistic processes.     

Probabilistic may/must testing: retaining probabilities by restricted schedulers

This paper considers the probabilistic may/must testing theory for processes having external, internal, and probabilistic choices. We observe that the underlying testing equivalence is too strong and distinguishes between processes that are observationally equivalent. The problem arises from the observation that the classical compose-and-schedule approach yields unrealistic overestimation of the probabilities, a phenomenon that has been recently well studied from the point of view of compositionality, in the context of randomized protocols and in probabilistic model checking. To that end, we propose a new testing theory, aiming at preserving the probability information in a parallel context. The resulting testing equivalence is insensitive to the exact moment the internal and the probabilistic choices occur. We also give an alternative characterization of the testing preorder as a probabilistic ready-trace preorder.     

Barbs and Congruences for Safe Mobile Ambients

The Ambient Calculus offers many ways in which processes can interact and be observed. In the context of Levi and Sangiorgi's Safe Mobile Ambients (SA), the extra co-capabilities required for interaction complicate the fundamental observations. We show that different formulations of barbs lead to the same barbed congruence. We prove this by following Honda and Yoshida's approach for the π-calculus by defining the insensitive terms of SA.     

Trace,failure and testing equivalences for communicating processes

A basic question in the theory of communicating processes is “When should two processes be considered equivalent?”. Attempts to answer this question have led to the concepts of observation equivalence, bisimulations, testing equivalence, failure equivalence, etc. The main point of this paper is to increase the understanding and motivation for two of these equivalences, namely failure and testing equivalences. The approach starts with the idea that the equivalence of processes should be reducible to the visible sequences of actions which a process performs in various contexts. This idea is implemented by a string-based semantic order for communicating processes where divergence is catastrophic. Under some assumptions about contexts, the resulting semantics is shown to be equivalent to theimproved failure semantics of Brookes and Roscoe⁽¹⁾ and also to themust testing-semantics of Hennessy and DeNicola.^(2–4) This characterization gives independent support for the appropriateness of failures and testing.     

Probabilistic Mobile Ambients

The calculus of Mobile Ambients has been introduced for expressing mobility and mobile computation. In this paper we present a probabilistic version of Mobile Ambients by augmenting the syntax of the original Ambient Calculus with a (guarded) probabilistic choice operator. To allow for the representation of both the probabilistic behaviour introduced through the new probabilistic choice operator and the nondeterminism present in the original Ambient Calculus we use probabilistic automata as the underpinning semantic model. The Ambient logic is a logic for Mobile Ambients that contains a novel treatment of both locations and hidden names. For specifying properties of Probabilistic Mobile Ambients, we extend this logic to specify probabilistic behaviour. In addition, to show the utility of our approach we present an example of a virus infecting a network.     

Flow-sensitive Leakage Analysis in Mobile Ambients

In this paper, we present a refinement of a Control Flow Analysis aimed at studying information flow security in the the calculus of Mobile Ambients. The improvements are achieved by making the analysis be flow-sensitive: the analysis is able to keep track of temporal dependencies of capabilities application when computing a safe approximation of the run-time topology of Mobile Ambient processes.     

safeDpi: a language for controlling mobile code

safeDpi is a distributed version of the Picalculus, in which processes are located at dynamically created sites. Parametrised code may be sent between sites using so-called ports, which are essentially higher-order versions of Picalculus communication channels. A host location may protect itself by only accepting code which conforms to a given type associated to the incoming port. We define a sophisticated static type system for these ports, which restrict the capabilities and access rights of any processes launched by incoming code. Dependent and existential types are used to add flexibility, allowing the behaviour of these launched processes, encoded as process types, to depend on the host's instantiation of the incoming code. We also show that a natural contextually defined behavioural equivalence can be characterised coinductively, using bisimulations based on typed actions. The characterisation is based on the idea of knowledge acquisition by a testing environment and makes explicit some of the subtleties of determining equivalence in this language of highly constrained distributed code.     

Statistical inference for equivalence trials with ordinal responses: A latent normal distribution approach

Testing of equivalence/non-inferiority has become an essential component in modern drug and treatment assessment. Before a newly developed treatment is introduced and applied to its target population, it is necessary to compare it to an existing (reference/standard) treatment. Unlike the traditional trial of testing the equality between two treatments, an equivalence trial, for instance, attempts to demonstrate that the responses to two treatments differ by an amount which is clinically insignificant. In many applications, the outcome measures of interest are usually recorded in ordinal scale (e.g., very good; good; moderate; poor). This paper presents a simple approach to the problem of equivalence testing in the presence of ordered categorical data. The proposed methodology operates on the assumption that the observed ordinal variable is governed by an underlying normally distributed trait. The new approach can be readily adopted for (i) commonly used equivalence limits such as difference and the ratio of treatment means and (ii) both one-sided non-inferiority and two-sided equivalence trials. We illustrate our methodology with two medical examples and demonstrate how test results and confidence interval estimates can be obtained from a freely available computer program.     

面向RISC-V的汇编程序语义等价性自动化测试系统

本文设计并实现了一套面向RISC-V的汇编程序语义等价性自动化测试系统.在面向RISC-V开发软件时,尤其是基于扩展指令(例如向量指令)编写高效的程序时,很难避免以手写汇编的方式编写代码.例如,为标准的C函数库编写相应的向量版函数.与编译器自动生成的代码不同,手写的汇编代码虽然可以最大限度地提高程序的效率,但因绕过了编译时对程序的约束(如类型检查、寄存器分配等)而对开发者提出了更高的要求.能否对新版本与标准版本的汇编程序进行快速地、自动化的语义等价性测试,将大大影响代码的正确性和软件开发和调试的效率.已有面向RISC-V的测试框架缺乏对语义等价性测试的支持,也未考虑程序执行带来的副作用.本研究基于模拟器的动态测试环境,设计并实现了一套面向RISC-V的汇编程序语义等价性自动化测试系统.系统通过跟踪机器状态,捕获程序执行的副作用,并结合用户定义的测试目标生成测试报告.实验表明,本系统相比已有的测试系统,能够有效地对RISC-V汇编程序的语义等价性进行测试.     

Testing Equivalence for Mobile Processes

The impact of applying the testing approach to a calculus of processes with dynamic communication topology is investigated. A proof system is introduced that consists of two groups of laws: those for strong observational equivalence and those needed to deal with invisible actions. Soundness and completeness of this proof system w.r.t. a testing preorder are shown. A fully abstract denotational model for the language is presented that takes advantage of reductions of processes to normal forms.     

Adding Action Refinement to a Finite Process Algebra

In this paper we present a Process Algebra for the specification of concurrent, communicating processes which incorporates operators for the refinement of actions by processes, in addition to the usual operators for communication, nondeterminism, internal actions, and restrictions, and study a suitable notion of semantic equivalence for it. We argue that action refinements should not, in some formal sense, interfere with the internal evolution of processes and their application to processes should consider the restriction operator as a "binder." We show that, under the above assumptions, the weak version of the refine equivalence introduced by Aceto and Hennessy ((1993) Inform. and Comput.103, 204-269) is preserved by action refinements and, moreover, is the largest such equivalence relation contained in weak bismulation equivalence. We also discuss an example showing that, contrary to what happens in Aceto and Hennessy ((1993) Inform. and Comput.103, 204-269), refine equivalence and timed equivalence are different notions of equivalence over the language considered in this paper.