Android Protected Confirmation (APC) is an authentication protocol designed by Google. It leverages the extra security of the Trusted Execution Environment (TEE) to secure transactions even in the presence of a compromised OS. The intended security guarantee for APC is that if a transaction has been signed under APC, then the user must have previously given its explicit consent, even if an attacker has gained root access to the victim’s Android OS. In this paper, we present a security analysis of APC in the Universal Composability (UC) framework. We uncover two attacks on the design of the protocol which allow a root adversary to issue transactions without the user consenting to them. We provide an attack implementation on a Google Pixel phone, and propose light-weight fixes. Finally, we specify the ideal UC functionality capturing the intended security guarantees for APC, and prove that the fixed protocol UC-realizes it.

We present a method for constructing robustly parameterised families of higher-order probabilistic models. Parameter spaces and models are represented by certain classes of functors in the category of Polish spaces. Maps from parameter spaces to models (parameterisations) are continuous and natural transformations between such functors. Naturality ensures that parameterised models are invariant by change of granularity -- ie that parameterisations are intrinsic. Continuity ensures that models are robust with respect to their parameterisation. Our method allows one to build models from a set of basic functors among which the Giry probabilistic functor, spaces of cadlag trajectories (in continuous and discrete time), multisets and compact powersets. These functors can be combined by guarded composition, product and coproduct. Parameter spaces range over the polynomial closure of Giry-like functors. Thus we obtain a class of robust parameterised models which includes the Dirichlet process, various point processes (random sequences with values in Polish spaces) and other classical objects of probability theory. By extending techniques developed in prior work, we show how to reduce the questions of existence, uniqueness, naturality, and continuity of a parameterised model to combinatorial questions only involving finite spaces.

The process of inverting Markov kernels relates to the important subject of Bayesian modelling and learning. In fact, Bayesian update is exactly kernel inversion. In this paper, we investigate how and when Markov kernels (aka stochastic relations, or probabilistic mappings, or simply kernels) can be inverted. We address the question both directly on the category of measurable spaces, and indirectly by interpreting kernels as Markov operators: - For the direct option, we introduce a typed version of the category of Markov kernels and use the so-called "disintegration of measures". Here, one has to specialise to measurable spaces borne from a simple class of topological spaces -e.g. Polish spaces (other choices are possible). Our method and result greatly simplify a recent development in Ref. [4]. - For the operator option, we use a cone version of the category of Markov operators (kernels seen as predicate transformers). That is to say, our linear operators are not just continuous, but are required to satisfy the stronger condition of being $\om$-chain-continuous. Prior work shows that one obtains an adjunction in the form of a pair of contravariant and inverse functors between the categories of $L_1$- and $L_\infty$-cones [3]. Inversion, seen through the operator prism, is just adjunction. No topological assumption is needed. - We show that both categories (Markov kernels and $\om$-chain-continuous Markov operators) are related by a family of contravariant functors $T_p$ for $1\leq p\leq\infty$. The $T_p$'s are Kleisli extensions of (duals of) conditional expectation functors introduced in Ref. [3]. - With this bridge in place, we can prove that both notions of inversion agree when both defined: if $f$ is a kernel, and $f\dg$ its direct inverse, then $T_\infty(f)\dg=T_1(f\dg)$.

We propose an algebraic approach to stochastic graph-rewriting which extends the classical construction of the Heisenberg-Weyl algebra and its canonical representation on the Fock space. Rules are seen as particular elements of an algebra of "diagrams": the diagram algebra D. Diagrams can be thought of as formal computational traces represented in partial time. They can be evaluated to normal diagrams (each corresponding to a rule) and generate an associative unital non-commutative algebra of rules: the rule algebra R. Evaluation becomes a morphism of unital associative algebras which maps general diagrams in D to normal ones in R. In this algebraic reformulation, usual distinctions between graph observables (real-valued maps on the set of graphs defined by counting subgraphs) and rules disappear. Instead, natural algebraic substructures of R arise: formal observables are seen as rules with equal left and right hand sides and form a commutative subalgebra, the ones counting subgraphs forming a sub-subalgebra of identity rules. Actual graph-rewriting is recovered as a canonical representation of the rule algebra as linear operators over the vector space generated by (isomorphism classes of) finite graphs. The construction of the representation is in close analogy with and subsumes the classical (multi-type bosonic) Fock space representation of the Heisenberg-Weyl algebra.

MOTIVATION: Biological systems are complex and challenging to model and therefore model reuse is highly desirable. To promote model reuse, models should include both information about the specifics of simulations and the underlying biology in the form of metadata. The availability of computationally tractable metadata is especially important for the effective automated interpretation and processing of models. Metadata are typically represented as machine-readable annotations which enhance programmatic access to information about models. Rule-based languages have emerged as a modelling framework to represent the complexity of biological systems. Annotation approaches have been widely used for reaction-based formalisms such as SBML. However, rule-based languages still lack a rich annotation framework to add semantic information, such as machine-readable descriptions, to the components of a model. RESULTS: We present an annotation framework and guidelines for annotating rule-based models, encoded in the commonly used Kappa and BioNetGen languages. We adapt widely adopted annotation approaches to rule-based models. We initially propose a syntax to store machine-readable annotations and describe a mapping between rule-based modelling entities, such as agents and rules, and their annotations. We then describe an ontology to both annotate these models and capture the information contained therein, and demonstrate annotating these models using examples. Finally, we present a proof of concept tool for extracting annotations from a model that can be queried and analyzed in a uniform way. The uniform representation of the annotations can be used to facilitate the creation, analysis, reuse and visualization of rule-based models. Although examples are given, using specific implementations the proposed techniques can be applied to rule-based models in general. AVAILABILITY AND IMPLEMENTATION: The annotation ontology for rule-based models can be found at http://purl.org/rbm/rbmo The krdf tool and associated executable examples are available at http://purl.org/rbm/rbmo/krdf CONTACT: [email protected] or [email protected].

Normally, one thinks of probabilistic transition systems as taking an initial probability distribution over the state space into a new probability distribution representing the system after a transition. We, however, take a dual view of Markov processes as transformers of bounded measurable functions. This is very much in the same spirit as a “predicate-transformer” view, which is dual to the state-transformer view of transition systems. We redevelop the theory of labelled Markov processes from this viewpoint; in particular, we explore approximation theory. We obtain three main results. (i) It is possible to define bisimulation on general measure spaces and show that it is an equivalence relation. The logical characterization of bisimulation can be done straightforwardly and generally. (ii) A new and flexible approach to approximation based on averaging can be given. This vastly generalizes and streamlines the idea of using conditional expectations to compute approximations. (iii) We show that there is a minimal process bisimulation-equivalent to a given process, and this minimal process is obtained as the limit of the finite approximants.

Abstract Summary: Spatial Kappa is a simulator of models written in a variant of the rule-based stochastic modelling language Kappa, with spatial extensions. Availability: The spatial kappa simulator is an open-source project licensed under the LGPLv3, with Java source, binaries and manual available at http://github.com/lptolik/SpatialKappa. Contact: [email protected] Supplementary information: Supplementary data are available at Bioinformatics online.

A generalised framework of site graphs is introduced in order to provide the first fully semantic definition of the side-effect-free core of the rule-based language Kappa. This formalisation allows the use of types either to confirm that a rule respects a certain invariant or to guide a restricted refinement process that allows us to constrain its run-time applicability.

This paper is concerned with the asymptotic properties of a restricted class of Petri nets equipped with stochastic mass-action semantics. We establish a simple algebraic criterion for the existence of an equilibrium, that is to say, an invariant probability that satisfies the detailed balance condition familiar from the thermodynamics of reaction networks. We also find that when such a probability exists, it can be described by a free energy function that combines an internal energy term and an entropy term. Under strong additional conditions, we show how the entropy term can be deconstructed using the finer-grained individual-token semantics of Petri nets.

In this paper, we introduce a novel way of constructing concise causal histories (pathways) to represent how specified structures are formed during simulation of systems represented by rule-based models. This is founded on a new, clean, graph-based semantics introduced in the first part of this paper for Kappa, a rule-based modelling language that has emerged as a natural description of protein-protein interactions in molecular biology [Bachman 2011]. The semantics is capable of capturing the whole of Kappa, including subtle side-effects on deletion of structure, and its structured presentation provides the basis for the translation of techniques to other models. In particular, we give a notion of trajectory compression, which restricts a trace culminating in the production of a given structure to the actions necessary for the structure to occur. This is central to the reconstruction of biochemical pathways due to the failure of traditional techniques to provide adequately concise causal histories, and we expect it to be applicable in a range of other modelling situations.

Rule-based approaches (as in our own Kappa, or the BNG language, or many other propositions allowing the consideration of "reaction classes'') offer new and more powerful ways to capture the combinatorial interactions that are typical of molecular biological systems. They afford relatively compact and faithful descriptions of cellular interaction networks despite the combination of two broad types of interaction: the formation of complexes (a biological term for the ubiquitous non-covalent binding of bio-molecules), and the chemical modifications of macromolecules (aka post-translational modifications). However, all is not perfect. This same combinatorial explosion that pervades biological systems also seems to prevent the simulation of molecular networks using systems of differential equations. In all but the simplest cases the generation (and even more the integration) of the explicit system of differential equations which is canonically associated to a rule set is unfeasible. So there seems to be a price to pay for this increase in clarity and precision of the description, namely that one can only execute such rule-based systems using their stochastic semantics as continuous time Markov chains, which means a slower if more accurate simulation. In this paper, we take a fresh look at this question, and, using techniques from the abstract interpretation framework, we construct a reduction method which generates (typically) far smaller systems of differential equations than the concrete/canonical one. We show that the abstract/reduced differential system has solutions which are linear combinations of the canonical ones. Importantly, our method: 1) does not require the concrete system to be explicitly computed, so it is intensional, 2) nor does it rely on the choice of a specific set of rate constants for the system to be reduced, so it is symbolic, and 3) achieves good compression when tested on rule-based models of significant size, so it is also realistic.

Measurement-based quantum computation has emerged from the physics community as a new approach to quantum computation where the notion of measurement is the main driving force of computation. This is in contrast with the more traditional circuit model that is based on unitary operations. Among measurement-based quantum computation methods, the recently introduced one-way quantum computer [Raussendorf and Briegel 2001] stands out as fundamental. We develop a rigorous mathematical model underlying the one-way quantum computer and present a concrete syntax and operational semantics for programs, which we call patterns , and an algebra of these patterns derived from a denotational semantics. More importantly, we present a calculus for reasoning locally and compositionally about these patterns. We present a rewrite theory and prove a general standardization theorem which allows all patterns to be put in a semantically equivalent standard form. Standardization has far-reaching consequences: a new physical architecture based on performing all the entanglement in the beginning, parallelization by exposing the dependency structure of measurements and expressiveness theorems. Furthermore we formalize several other measurement-based models, for example, Teleportation, Phase and Pauli models and present compositional embeddings of them into and from the one-way model. This allows us to transfer all the theory we develop for the one-way model to these models. This shows that the framework we have developed has a general impact on measurement-based computation and is not just particular to the one-way quantum computer.

All classical ?-terms typable with disjunctive normal forms are shown to share a common computational behavior: they implement a local exception handling mechanism whose exact workings depend on the tautology. Equivalent and more efficient control combinators are described through a specialized sequent calculus and shown to be correct.

This paper proposes a measure-theoretic reconstruction of the approximation schemes developed for labeled Markov processes: approximants are seen as quotients with respect to sets of temporal properties expressed in a simple logic. This gives the possibility of customizing approximants with respect to properties of interest and is thus an important step towards using automated techniques intended for finite state systems, e.g. model checking, for continuous state systems. The measure-theoretic apparatus meshes well with an enriched logic, extended with a greatest fix-point, and gives means to define approximants which retain cyclic properties of their target.

A category of HO/N-style games and probabilistic strategies is developed where the possible choices of a strategy are quantified so as to give a measure of the likelihood of seeing a given play. A two-sided die is shown to be universal in this category, in the sense that any strategy breaks down into a composition between some deterministic strategy and that die. The interpretative power of the category is then demonstrated by delineating a Cartesian closed subcategory that provides a fully abstract model of a probabilistic extension of Idealized Algol.

A category of HO/N-style games and probabilistic strategies is developed where the possible choices of a strategy are quantified so as to give a measure of the likelihood of seeing a given play. A 2-sided die is shown to be universal in this category, in the sense that any strategy breaks down into a composition between some deterministic strategy and that die. The interpretative power of the category is then demonstrated by delineating a Cartesian closed subcategory which provides a fully abstract model of a probabilistic extension of Idealized Algol.

A general category of games is constructed. A subcategory of saturated strategies, closed under all possible codings in copy games, is shown to model reduction in classical linear logic.

Abstract The main concern of this paper is the design of a noetherian and confluent normalization for LK2 (that is, classical second order predicate logic presented as a sequent calculus). The method we present is powerful: since it allows us to recover as fragments formalisms as seemingly different as Girard's LC and Parigot's λμ, FD ([10, 12, 32, 36]), delineates other viable systems as well, and gives means to extend the Krivine/Leivant paradigm of ‘programming-with-proofs’ ([26, 27]) to classical logic; it is painless: since we reduce strong normalization and confluence to the same properties for linear logic (for non-additive proof nets, to be precise) using appropriate embeddings (so-called decorations); it is unifying: it organizes known solutions in a simple pattern that makes apparent the how and why of their making. A comparison of our method to that of embedding LK into LJ (intuitionistic sequent calculus) brings to the fore the latter's defects for these ‘deconstructive purposes’.

The interaction processes at work by M. Hyland and L. Ong (1994) (HO) and S. Abramsky et al. (1994) (AJM) new game semantics are two preexisting paradigmatic implementations of linear head reduction: respectively Krivine's abstract machine and Girard's interaction abstract machine. There is a simple and natural embedding of AJM-games to HO-games, mapping strategies to strategies and reducing AJM definability (or full abstraction) property to HO's one.

Since the rebirth of /spl lambda/-calculus in the late 1960s, three major theoretical investigations of /spl beta/-reduction have been undertaken: (1) Levy's (1978) analysis of families of redexes (and the associated concept of labeled reductions); (2) Lamping's (1990) graph-reduction algorithm; and (3) Girard's (1988) geometry of interaction. All three studies happened to make crucial (if not always explicit) use of the notion of a path, namely and respectively: legal paths, consistent paths and regular paths. We prove that these are equivalent to each other.>

The authors build a confluent, local, asynchronous reduction on lambda -terms, using infinite objects (partial injections of Girard's (1988) algebra L*), which is simple (only one move), intelligible (semantic setting of the reduction), and general (based on a large-scale decomposition of beta ), and may be mechanized.>