Relaxed memory models must simultaneously achieve efficient implementability and thread-compositional reasoning. Is that why they have become so complicated? We argue that the answer is no: It is possible to achieve these goals by combining an idea from the 60s (preconditions) with an idea from the 80s (pomsets), at least for X64 and ARMv8. We show that the resulting model (1) supports compositional reasoning for temporal safety properties, (2) supports all expected sequential compiler optimizations, (3) satisfies the DRF-SC criterion, and (4) compiles to X64 and ARMv8 microprocessors without requiring extra fences on relaxed accesses.

We define local transactional race freedom (LTRF), which provides a programmer model for software transactional memory. LTRF programs satisfy the SC-LTRF property, thus allowing the programmer to focus on sequential executions in which transactions execute atomically. Unlike previous results, SC-LTRF does not require global race freedom. We also provide a lower-level implementation model to reason about quiescence fences and validate numerous compiler optimizations.

This paper studies information flow caused by speculation mechanisms in hardware and software. The Spectre attack shows that there are practical information flow attacks which use an interaction of dynamic security checks, speculative evaluation and cache timing. Previous formal models of program execution are designed to capture computer architecture, rather than micro-architecture, and so do not capture attacks such as Spectre. In this paper, we propose a model based on pomsets which is designed to model speculative evaluation. The model is abstract with respect to specific micro-architectural features, such as caches and pipelines, yet is powerful enough to express known attacks such as Spectre and Prime+Abort, and verify their countermeasures. The model also allows for the prediction of new information flow attacks. We derive two such attacks, which exploit compiler optimizations, and validate these experimentally against gcc and clang.

We address the problem of validity in eventually consistent (EC) systems: In what sense does an EC data structure satisfy the sequential specification of that data structure? Because EC is a very weak criterion, our definition does not describe every EC system; however it is expressive enough to describe any Convergent or Commutative Replicated Data Type (CRDT).

The integration of transactions into hardware relaxed memory architectures is a topic of current research both in industry and academia. In this paper, we provide a general architectural framework for the introduction of transactions into models of relaxed memory in hardware, including the SC, TSO, ARMv8 and PPC models. Our framework incorporates flexible and expressive forms of transaction aborts and execution that have hitherto been in the realm of software transactional memory. In contrast to software transactional memory, we account for the characteristics of relaxed memory as a restricted form of distributed system, without a notion of global time. We prove abstraction theorems to demonstrate that the programmer API matches the intuitions and expectations about transactions.

Session types describe and constrain the input/output behaviour of systems. Existing session typing systems have limited support for polymorphism. For example, existing systems cannot provide the most general type for a generic proxy process that forwards messages between two channels. We provide a polymorphic session typing system for the π calculus, and demonstrate the utility of session-type-level functions in combination with polymorphic session typing. The type system guarantees subject reduction and safety properties, but not deadlock freedom. We describe a formalization of the type system in Coq. The proofs of subject reduction and safety properties, as well as typing of example processes, have been mechanically verified.

Digital forensics reports typically document the search process that has led to a conclusion, the primary means to verify the report is to repeat the search process. We believe that, as a result, the Trusted Computing Base for digital forensics is unnecessarily large and opaque. We advocate the use of forensic certificates as intermediate artifacts between search and verification. Because a forensic certificate has a precise semantics, it can be verified without knowledge of the search process and forensic tools used to create it. In addition, this precision opens up avenues for the analysis of forensic specifications. We present a case study using the specification of a deleted file. We propose a verification architecture that addresses the enormous size of digital forensics data sets. As a proof of concept, we consider a computer intrusion case study, drawn from the Honey net project. Our Coq formalization yields a verifiable certificate of the correctness of the underlying forensic analysis.

Randomization is used in computer security as a tool to introduce unpredictability into the software infrastructure. In this paper, we study the use of randomization to achieve the secrecy and integrity guarantees for local memory. We follow the approach set out by Abadi and Plot kin. We consider the execution of an idealized language in two environments. In the strict environment, opponents cannot access local variables of the user program. In the lax environment, opponents may attempt to guess allocated memory locations and thus, with small probability, gain access the local memory of the user program. We model these environments using two novel calculi: lambda-mu-hashref and lambda-mu-proberef. Our contribution to the Abadi-Plot kin program is to enrich the programming language with dynamic memory allocation, first class and higher order references and call/cc-style control. On the one hand, these enhancements allow us to directly model a larger class of system hardening principles. On the other hand, the class of opponents is also enhanced since our enriched language permits natural and direct encoding of attacks that alter the control flow of programs. Our main technical result is a fully abstract translation (up to probability) of lambda-mu-hashref into lambda-mu-proberef. Thus, in the presence of randomized layouts, the opponent gains no new power from being able to guess local references of the user program. Our numerical bounds are similar to those of Abadi and Plot kin, thus, the extra programming language features do not cause a concomitant increase in the resources required for protection via randomization.

We study mechanisms that permit program components to express role constraints on clients, focusing on programmatic security mechanisms, which permit access controls to be expressed, in situ, as part of the code realizing basic functionality. In this setting, two questions immediately arise: (1) The user of a component faces the issue of safety: is a particular role sufficient to use the component? (2) The component designer faces the dual issue of protection: is a particular role demanded in all execution paths of the component? We provide a formal calculus and static analysis to answer both questions.

We address the programmatic realization of the access control model of security in distributed systems. Our aim is to bridge the gap between abstract/declarative policies and their concrete/operational implementations. We present a programming formalism (which extends the asynchronous pi-calculus with explicit principals) and a specification logic (which extends Datalog with primitives from authorization logic). We provide two kinds of static analysis methods to tie implementation to specification. Type checking determines that a program is a sound implementation of policy; i.e., that all granted accesses are safe in the face of arbitrary opponents. Model checking determines a degree of completeness; i.e., that accesses permitted by the policy are actually granted in the implementation.

A memory model for a concurrent imperative programming language specifies which writes to shared variables may be seen by reads performed by other threads. We present a simple mathematical framework for relaxed memory models for programming languages. To instantiate this framework for a specific language, the designer must choose the notion of atomic steps supported by the language (e.g. 32-bit reads and writes) and specify how a composite step may be broken into a sequence of atomic steps (the decomposition rule). This rule determines which sequence of intermediate writes (if any) are visible to concurrent reads by other threads. Different choices of the rule lead to models which permit a read to return any value if there is a concurrent write (race), or models which satisfy a "No Thin Air Read"property. The former is suitable for languages such as C++(programs with races have undefined behavior), and the latter for Java. Other intermediate models are possible, useful and interesting.

Multiple firewalls typically cooperate to provide security properties for a network, despite the fact that these firewalls are often spatially distributed and configured in isolation. Without a global view of the network configuration, such a system is ripe for misconfiguration, causing conflicts and major security vulnerabilities.

We argue that games are expressive enough to encompass (history-based) access control, (resource) usage control (e.g., dynamic adaptive access control of reputation systems), accountability based controls (e.g., insurance), controls derived from rationality assumptions on participants (e.g., network mechanisms), and their composition. Building on the extensive research into games, we demonstrate that this expressive power coexists with a formal analysis framework comparable to that available for access control

We develop a pseudo-metric analogue of bisimulation for generalized semi-Markov processes. The kernel of this pseudo-metric corresponds to bisimulation; thus we have extended bisimulation for continuous-time probabilistic processes to a much broader class of distributions than exponential distributions. This pseudo-metric gives a useful handle on approximate reasoning in the presence of numerical information -- such as probabilities and time -- in the model. We give a fixed point characterization of the pseudo-metric. This makes available coinductive reasoning principles for reasoning about distances. We demonstrate that our approach is insensitive to potentially ad hoc articulations of distance by showing that it is intrinsic to an underlying uniformity. We provide a logical characterization of this uniformity using a real-valued modal logic. We show that several quantitative properties of interest are continuous with respect to the pseudo-metric. Thus, if two processes are metrically close, then observable quantitative properties of interest are indeed close.

This paper focuses on policy languages for (role-based) access control [14, 32], especially in their modern incarnations in the form of trust-management systems [9] and usage control [30, 31]. Any (declarative) approach to access control and trust management has to address the following issues:

We present a framework for abstracting two-player turn-based games that preserves any formula of the alternating /spl mu/-calculus (AMC). Unlike traditional conservative abstractions which can only prove the existence of winning strategies for only one of the players, our framework is based on 3-valued games, and it can be used to prove and disprove formulas of AMC including arbitrarily nested strategy quantifiers. Our main contributions are as follows. We define abstract 3-valued games and an alternating refinement relation on these that preserves winning strategies for both players. We provide a logical characterization of the alternating refinement relation. We show that our abstractions are as precise as can be via completeness results. We present AMC formulas that solve 3-valued games with /spl omega/-regular objectives, and we show that such games are determined in a 3-valued sense. We also discuss the complexity of model checking arbitrary AMC formulas on 3-valued games and of checking alternating refinement.

A reactive system can be specified by a labelled transition system, which indicates static structure, along with temporal-logic formulas, which assert dynamic behaviour. But refining the former while preserving the latter can be difficult, because: (i) Labelled transition systems are ‘total’ – characterised up to bisimulation – meaning that no new transition structure can appear in a refinement. (ii) Alternatively, a refinement criterion not based on bisimulation might generate a refined transition system that violates the temporal properties. In response, Larsen and Thomson proposed modal transition systems, which are ‘partial’, and defined a refinement criterion that preserved formulas in Hennessy–Milner logic. We show that modal transition systems are, up to a saturation condition, exactly the mixed transition systems of Dams that meet a mix condition, and we extend such systems to non-flat state sets. We then solve a domain equation over the mixed powerdomain whose solution is a bifinite domain that is universal for all saturated modal transition systems and is itself fully abstract when considered as a modal transition system. We demonstrate that many frameworks of partial systems can be translated into the domain: partial Kripke structures, partial bisimulation structures, Kripke modal transition systems, and pointer-shape-analysis graphs.

No abstract available.

We observe that equivalence is not a robust concept in the presence of numerical information - such as probabilities-in the model. We develop a metric analogue of weak bisimulation in the spirit of our earlier work on metric analogues for strong bisimulation. We give a fixed point characterization of the metric. This makes available conductive reasoning principles and allows us to prove metric analogues of the usual algebraic laws for process combinators. We also show that quantitative properties of interest are continuous with respect to the metric, which says that if two processes are close in the metric then observable quantitative properties of interest are indeed close. As an important example of this we show that nearby processes have nearby channel capacities - a quantitative measure of their propensity to leak information.

We study approximate reasoning about continuous-state labeled Markov processes. We show how to approximate a labeled Markov process by a family of finite-state labeled Markov chains. We show that the collection of labeled Markov processes carries a Polish space structure with a countable basis given by finite state Markov chains with rational probabilities. The primary technical tools that we develop to reach these results are: a finite-model theorem for the modal logic used to characterize bisimulation; and a categorical equivalence between the category of Markov processes (with simulation morphisms) with the /spl omega/-continuous dcpo Proc, defined as the solution of the recursive domain equation Proc=/spl Pi//sub Labels/ P/sub Prob/(Proc). The correspondence between labeled Markov processes and Proc yields a logic complete for reasoning about simulation for continuous-state processes.

Constraint-based languages can express in a concise way the complex logic of a new generation of interactive services for applications such as banking or stock trading, that must support multiple types of interfaces for accessing the same data. These include automatic speech-recognition interfaces where inputs may be provided in any order by users of the service. We study in this paper how to systematically test event-driven applications developed using such languages. We show how such applications can be tested automatically, without the need for any manually-written test cases, and efficiently, by taking advantage of their capability of taking unordered sets of events as inputs.

) Vineet Gupta Radha Jagadeesan Prakash Panangaden y [email protected] [email protected] [email protected] Caelum Research Corporation Dept. of Math. and Computer Sciences School of Computer Science NASA Ames Research Center Loyola University--Lake Shore Campus McGill University Moffett Field CA 94035, USA Chicago IL 60626, USA Montreal, Quebec, Canada Abstract This paper describes a stochastic concurrent constraint language for the description and programming of concurrent probabilistic systems. The language can be viewed both as a calculus for describing and reasoning about stochastic processes and as an executable language for simulating stochastic processes. In this language programs encode probability distributions over (potentially infinite) sets of objects. We illustrate the subtleties that arise from the interaction of constraints, random choice and recursion. We describe operational semantics of these programs (programs are run by sampling random choices), deno...

We extend cc to allow the specification of a discrete probability distribution for random variables. We demonstrate the expressiveness of pcc by synthesizing combinators for default reasoning. We extend pcc uniformly over time, to get a synchronous reactive probabilistic programming language, Timed pcc. We describe operational and denotational models for pcc (and Timed pcc). The key feature of the denotational model(s) is that parallel composition is essentially set intersection. We show that the denotational model ofpcc (resp. Timed pcc) is conservative over cc (resp. tcc). We also show that the denotational models are fully abstract for an operational semantics that records probability information.

We extend the model of [SJG94b] to express strong time-outs (and pre-emption): if an event A does not happen through time t, cause event B to happen at time t. Such constructs arise naturally in practice (e.g. in modeling transistors) and are supported in languages such as ESTEREL (through instantaneous watchdogs) and LUSTRE (through the “current” operator).

We develop a model for timed, reactive computation by extending the asynchronous, untimed concurrent constraint programming model in a simple and uniform way. In the spirit of process algebras, we develop some combinators expressible in this model, and reconcile their operational, logical and denotational character. We show how programs may be compiled into finite-state machines with loop-free computations at each state, thus guaranteeing bounded response time.>

Abstract We present a game semantics for Linear Logic, in which formulas denote games and proofs denote winning strategies. We show that our semantics yields a categorical model of Linear Logic and prove full completeness for Multiplicative Linear Logic with the MIX rule: every winning strategy is the denotation of a unique cut-free proof net. A key role is played by the notion of history-free strategy; strong connections are made between history-free strategies and the Geometry of Interaction. Our semantics incorporates a natural notion of polarity, leading to a refined treatment of the additives. We make comparisons with related work by Joyal, Blass, et al.

A new formal embodiment of J.-Y. Girard's (1989) geometry of interaction program is given. The geometry of interaction interpretation considered is defined, and the computational interpretation is sketched in terms of dataflow nets. Some examples that illustrate the key ideas underlying the interpretation are given. The results, which include the semantic analogue of cut-elimination, stated in terms of a finite convergence property, are outlined.>

Althoughthere is considerable experience in using languages that combine the functional and logic program-

There is much interest in combining the functional and logic programming paradigms � in particular, there have been several proposals for adding logic variables to functional languages, since that permits incremental construction of data structures through constraint intersection. While it is straight-forward to give an abstract semantics for functional languages and for logic languages, it has proven surprisingly di cult to give a proper semantic account of functional languages with logic variables. In this paper, we present a rst-order functional language with logic variables and give its meaning using a structural operational semantics. We also give it a denotational semantics, using a novel technique involving closure operators on a Scott domain. Finally, we show that these two semantics correspond in the strongest possible way|weshow that the denotational semantics is fully abstract with respect to the operational semantics. The techniques developed in this paper are quite general, and can be used to give semantics to any constraint-based logic programming languages. Our results can also be interpreted as a generalization of Kahn semantics for data ow networks in which processes not only exchange messages, but have access to a shared global address space in which variables are bound through constraint intersection. Categories and Subject Descriptors: D.1.1 [Programming Techniques]: Functional Programming � D.3.1 [Programming Languages]: Formal De nitions and Theory- semantics � D.3.2 [Programming Languages]: Data ow Languages � F.3.2 [Theory of Computation]: Semantics of Programming Languages- denotational semantics � F.4.1 [Theory of Computation]: Mathematical Logic- logic programming

There is much interest in the declarative languages community in integrating logic variables into functional languages. The authors give a full semantic account of such a language. They present a Plotkin-style operational semantics for the language and an abstract semantics that expresses meanings as closure operators on a Scott domain. They also show that the denotational semantics is fully abstract with respect to the operational semantics.>