David Teller: Publications

Techniques such as mobility and distribution are often used to overcome limitations of resources such as the amount of memory or the necessity for specialised devices. Indeed, questions related to such limitations are crucial in matters of security, compilation and quality of service. However, few attempts have been made at formalising this notion of resource limitation in presence of mobility, distribution or concurrency.

In this paper, we present a formalisation of resource usage, resource limitations and garbage-collection, using as a support a variant of the pi-calculus, the second generation of the controlled pi-calculus. We use this calculus to study formally the notion of garbage-collection and to produce an effective proof system for respect of resource bounds, aware of resource transfer between processes and resource reuse thanks to finalisation. We also present an example of transformation of a protocol for compliance with such limitations and we confront informally our definitions with commonly-used garbage-collectors such as those of OCaml, Java and C#.

Although limits of resources such as memory or disk usage are one of the key problems of many communicating applications, most process algebras fail to take this aspect of mobile and concurrent systems into account. In order to study this problem, we introduce the Controlled pi-calculus, an extension of the pi-calculus with a notion of recovery of unused resources with an explicit (parametrized) garbage-collection and dead-process elimination. We discuss the definition of garbage-collection and dead-process elimination for concurrent, communicating applications, and provide a type-based technique for statically proving resource bounds. Selected examples are presented and show the potential of the Controlled pi-calculus.

Current software and hardware systems, being parallel and reconfigurable, raise new safety and reliability problems, and the resolution of these problems requires new methods. Numerous proposals attempt at reducing the threat of bugs and preventing several kinds of attacks. In this paper, we develop an extension of the calculus of Mobile Ambients, named Controlled Ambients, that is suited for expressing such issues, specifically Denial of Service attacks. We present a type system for Controlled Ambients, which makes static resource control possible in our setting.

Slowly but surely, the language industry is discovering the need for programming languages, runtime supports and methodologies adapted to distributed computing platforms. However, current distributed platforms, whether industrial or academic, are generally fragile with respect to resource exhaustion, and can provide, at best, ad hoc solutions to counter accidents or Denial of Service attacks. In this paper, we examine the problem of resource management in Erlang. Using Tepic, an applied variant of the pi-calculus, we provide a formal semantics for a subset of Core Erlang and a sample of its library, with a formal notion of resource usage, resource exhaustion and robustness. We then complete these definitions by a type system whose judgements guarantee robustness of a program with respect to Denial of Service attacks.

Failing to control resources in mobile, concurrent and distributed systems may lead to important breakdowns or Denial of Service-like attacks. In order to address this problem, we present enhanced versions of several calculi for mobile and distributed computing, namely NBA, Seals, Nomadic Pi and Kells. In each case, we make the formalism resource-conscious and define a type system in order to guarantee statically compliance with resource control policies. Comparing the solutions we proposed for these calculi, we try and define the necessities of resource-control in mobile and distributed formalisms.

Slowly but surely, the language industry is discovering the need for programming languages, runtime supports and methodologies adapted to distributed computing platforms. However, current distributed platforms, whether industrial or academic, are generally fragile with respect to resource exhaustion, and can provide, at best, ad hoc solutions to counter accidents or Denial of Service attacks. In this paper, we examine the problem of resource management in Erlang. Using Tepic, an applied variant of the pi-calculus, we provide a formal semantics for a subset of Core Erlang and a sample of its library, with a formal notion of resource usage, resource exhaustion and robustness. We then complete these definitions by a type system whose judgements guarantee robustness of a program with respect to Denial of Service attacks.

Edition of books has changed. Ten years ago, there were only two on-line publishers, both of them non-profit organisations. Nowadays, a number of companies provide one-size-fits-all on-line shops for on-line publishers or on-line self-published authors. Outside of Project Gutenberg, however, on-line publications tend to be either web pages, proprietary formats or open formats restricted by patents to proprietary readers.

The OpenBerg project aims at providing free, open-source and open-standard tools for digital publication (a.k.a. e-Publishing), for use by authors, readers and editors. In particular, our main effort is the development of OpenBerg Reader, a cross-platform, multi-format, e-Book reader targetted towards textbooks, exercise books and academic content.

This document describes the key notions of OpenBerg Reader, the choices we made regarding our tools and platforms, as well as the current status of the implementation and our plans for the future. The objective of this document is to serve as a reference for the developers of OpenBerg Reader and the associated tools. As OpenBerg Reader and the open-source world in general, this document is intended as a permanent work-in-progress, to be completed as we add features and specifications.

We introduce Tepic, a family of calculi based on the pi-calculus. By opposition to the pi-calculus, Tepic allows the embedding of a low-level language for resource acquisitions (e.g. a library of primitives) and a low-level language for resource depositaries (e.g. references to the outside world) inside the concurrency framework of the pi-calculus. This design should permit using Tepic as both a setting for reasoning about properties of various protocols (e.g. resource usage, security protocols, code migration) and a base for a programming language for the implementation of these protocols.

We present operational semantics for Tepic, for reasoning both in absence and in presence of resource limitations, notions of resource-aware (bi)simulations, of equivalence of primitives, of garbage-collection of both values internal to the language or references to external entities. We complete this by the definition of several type systems for proving correctness of operations with respect to resource bounds.

We also present examples of programming with Tepic, including a concrete syntax, interesting data structures, an encoding of Tepic into itself, and details of the implementation of cryptographic protocols in Tepic.

This is a work in progress.

Techniques such as mobility and distribution are often used to overcome limitations of resources such as the amount of memory or the necessity for specialized devices. However, few attempts have been made at formalizing the notion limited resources in process algebras for mobility and distribution. One of our previous works introduced a variant of the pi-calculus with explicit allocation, garbage-collection and finalization of resources and a type system to guarantee bounds on resource usage.

In this paper, we revisit this controlled pi-calculus, providing better semantics for allocation and deallocation and a better observation of resource-related behaviours and garbage-collection. We also expand the type system to provide guarantees of respect of more complex protocols on resources. We demonstrate the interest of the controlled π-calculus by building a model of a complex resources manager for concurrent systems, with manual and automatic garbage-collection, error-handling and statically distributed and transmitted authorizations and resources.

Failing to control resources in mobile, concurrent and distributed systems may lead to important breakdowns or Denial of Service-like attacks. In order to address this problem, we present enhanced versions of several calculi for mobile and distributed computing, namely NBA, Seals, Nomadic Pi and Kells. In each case, we make the formalism resource-conscious and define a type system in order to guarantee statically compliance with resource control policies. Comparing the solutions we proposed for these calculi, we try and define the necessities of resource-control in mobile and distributed formalisms.

Proof-carrying code (PCC), as pioneered by Necula and Lee, allows a code producer to provide a compiled program to a host, along with a formal proof of safety. The PCCbased systems often rely on solving integer constraints to prove the soundness of the index types and to control resource consumption. Unfortunately, existing approaches often require the inclusion of an oracle-like constraints solver into the trusted computing base (TCB) or at least lock the safety policy with one particular solver. This paper presents a feasibility study for dissociating the constraints solver from the TCB and the safety policy from the actual solver algorithm. To demonstrate this, we produce a simple framework, we show how to adapt the popular solvers such as the Omega test and the Simplex method into this framework and we study some of its properties.