David Teller: Research

Overall subject: semantics of system security (2006-?)

Team

• David Teller
• Jérémy Briffaut

Presentation

A computer system is considered safe if a person, computer or software who is not allowed to read some confidential information, perform some action or alter the behaviour of the system has strictly no manner of doing something forbidden, either directly or indirectly, by tricking some other person, computer or software into helping them.

This notion of authorization (or "security policies") is the main preoccupation of team SDS: how can one determine what the minimal set of authorizations should be granted to a user or an application, so as to let work proceed while limiting risks in case of accident or malicious intents ? How can one determine if these authorizations are sufficient ? How can one ensure that barriers are enforced efficiently ? Indeed, while the latest and upcoming generations of operating systems offer numerous tools for enforcing barriers, in the form of Mandatory Access Control layers such as SELinux, very little exists to be sure that these barriers are well-chosen. This is where our work finds its place: by combining techniques available in the field of system security and techniques found more often in the field of semantics of programming languages, we aim to

• analyze programs and security policies to determine the least security policy required to run a program satisfactorily
• use combinations of dynamically-verified security checks and statically-proved type properties to produce programs that can be guaranteed to comply with complex security policies
• model and analyze security policies to determine if there is a risk that sequence of interactions could provide a mean for a malicious agent to overreach its authorizations by tricking applications into helping him.

Types and Effects for security, in C

Team

• David Teller
• Patrice Clémente
• Bastien Jansen
• Steve-William Kissi

Presentation

While the C language is considered as more dangerous than useful by most members of the field of language semantics, this language is still the most-used for programming of system-level applications, including most of the Linux operating system. Unfortunately, C offers very little in terms of security or verifiable properties. Indeed, one of the main reason why operating system-level security and sanity checks are necessary is that C will let the imperfect programmer write code full of security holes.

Our project aims at helping make C code more trustworthy :

• define an approximate analysis system for C based on the discipline of types and effects, as introduced by Tofte and Talpin, with a small dose of dependent typing, with inference
• model SELinux security policies as a set of program effects, as defined earlier
• implement the analysis
• apply the analysis to the actual source code of C's standard library, possibly correcting it by hand whenever precision turns out insufficient, so as to produce a comprehensive library of SELinux-style effects, which in turn will be usable as a base model for analysis of higher-level programs and libraries.

Note that the analysis is necessarily approximate, as C is an approximately-defined language itself. In additon, there is a trade-off between the complexity of security policies which may be represented and checked and the prcision of the analysis.

This project contrasts with other analysis of C and/or SELinux policies insofar as

• we combine the semantic approach of a type-and-effects type system with inference and a system-based model of SELinux security policies
• our type system attempts to analyze security policies while assuming the absence of programming errors, while most other type systems attempt to detect programming errors while leaving system-level security policies a concern of the type system.

Current status

A prototype type system for a subset of C has been designed and is currently being implemented as a Java application. By design, this type system accepts the whole language, although a number of circumstances not yet handled cause it to decide that some functions are unanalyzable and must be considered dangerous.

Note

This project is part of an ongoing application to an ANR call for projects for year 2008.

Static and dynamic security for JavaScript

Team

• David Teller
• Jérémy Colombet
• Benjamin Meslin

Presentation

JavaScript is an interesting language, with growing popularity. It is used to develop client-side web applications, including GMail, Google Maps, as well as server-side web applications, but also desktop applications such as Firefox, Thunderbird, Nvu/Kompozer, Songbird, and extensions for Firefox, Opera, Safari, MacOS X’ Dashboard, etc.

With JavaScript 2, the language becomes a serious contender in the world of programming languages, somewhere between Java and C# (on the side of rather-strongly-typed languages) and Python and Ruby (on the side of dynamic languages). In particular, JavaScript 2 adds to JavaScript a number of features found most commonly in functional programming languages, such as a degree of pattern-matching and structural typing, both static and dynamic.

The objective of this work is to provide guarantees of safety for programs written in JavaScript, by combining static analysis and dynamic checking. The static analysis takes the form of a types-and-effects type system for a subset of JavaScript, while the dynamic checks are an extension of the Mozilla platform designed to bring SELinux-style security policies to that platform, which in turn will be used as the base for a model of security comparable to that used in our work on analysis of C.

Current status

Work is proceeding both on the implementation of the Security Extensions for the Mozilla platform and on the implementation of a toolbox designed for testing type systems on actual JavaScript 2 code. Whenever completed, the Security Extensions will provied the base for the model upon which to build the type system.

As a side effect, I have become involved with the team in charge of JavaScript 2, both for the design (remotely) and for the testing (closely) of the JavaScript 2 programming language. I am currently being considered for inclusion in the second stage design team dealing with concurrency.

Dynamic guarantees of semantic properties for native components for distributed systems

Team

• Jérémy Briffaut
• David Teller
• Jean-Bernard Stefani (Inria Grenoble)
• Alan Schmitt (Inria Grenoble)
• Daniel Hirschkoff (ENS Lyon)
• Tom Hirschowitz (ENS Lyon)

Presentation

The calculus of Kells is a formalism designed to specify and model components for distributed, mobile and dynamic programming. For this formalism, a number of theoretical tools have been developed to permit proving or verifying safety or conformance with specifications, including bisimulations, models and type systems. In its current state, it is nearly ready to become the base for a distributed virtual machine, designed for the construction of safe distributed and reconfigurable applications. Unfortunately, the theoretical tools have a limitation: whenever components implemented with the future language of Kells need to interact with native components implemented in C or in any other language, one needs to trust the fact that these components will behave in accordance with their specification.

The objective of our work, here, is to reduce the size of the trusted computing base of the future Kell virtual machine, by generating dynamic specification enforcers for native components. In other words, from a behavioural specification in the Kell language based on bisimulations, create a native wrapper for a native component, which will be able to dynamically monitor the behaviour of the native component and ensure that this component never deviates from the specification.

Current status

We are currently working on isolating a subset of the Kell language with finite control for which generation of the native wrapper will be possible.

Note

This project is part of an ongoing application to an ANR call for projects for year 2008.

---

Past lives: resources for concurrent/distributed systems

Distribution is the name of the field of computer science whose aim is to understand how to effectively use several processing and storage units to achieve a common goal. For instance, in modern PCs, a number of computing tasks are distributed between the Central Processing Unit, a Graphics Processing Unit (typically, 2D/3D accelerated graphics card), a Digital Sound Processor and possibly other peripherals. In next-generation technologies such as Cell-based devices, distribution goes one step further, by forcing to divide nearly all tasks between cells with separate memories and, among each cell, between "Synergistic Processing Elements" with their own unshared memory.

Distribution attempts at solving several problems common in computing:

• lack of processing power on one processing unit, as we seem to approach the boundaries of what non-distributed technologies can offer with regard to speed
• lack of memory on one processing unit, as both short-term storage in RAM and long-term storage on hard-drive are effectively limited on single computers
• lack of information, as each processing unit may have access to different inputs, for instance sensors, which are physically connected only to some nodes
• other factors, such as proximity to the user, a degree of redundancy and fault-tolerance...

One possible point of view on all these requirements is to consider them as resources. A process may need some resources to be executed, may take advantage of some additional resources, may acquire or release resources and may provide resources for other processes.

In turn, a number of issues arise from the distribution of processes and resources:

• potentially unsafe concurrent access to resources
• necessity to ensure that resources are eventually released
• resources limited in their absolute number (i.e. paper for the printer, money, time)
• necessity to ensure that only authorised agents can effectively use a resource
• necessity to ensure that only non-authorised cannot trick authorised agents into using too many resources
• ...

One of the challenges of today's research in programming languages theory and applications is to devise methods to describe resources and resource usage, to ensure that resources are used correctly -- respecting some policies provided by their owner as well as intrinsic limits -- and safely.
This is the overall theme of my work.

Resources, garbage and errors in concurrent processes (2003-?)

Team

• David Teller

with input from

• Martin Berger
• Tom Hirschowitz
• Daniel Hirschkoff
• Julian Rathke
• Davide Sangiorgi
• Vladimiro Sassone

Presentation

The π-calculus is a simple yet powerful formalism for concurrency, mobility and, to a degree, distribution. In addition to the fact that this calculus is interesting for purely intellectual reasons, it closely models concurrent programming and network communications, some of the main concerns of distributed programming. In this calculus, the main entity is the named channel. Channels can be created and used to communicate, either inside a process, or with the outside world. The name of channels itself can be communicated, hence allowing rich protocols.

Although several technique permit to describe who is allowed to use a channel for reading or writing or what kind of information is acceptable to communicate on a potentially unsafe medium, no work has been done to control the usage of resources by channels themselves. As channels are used to represent most resource-like concepts, from memory cells to files, to sockets, semaphores, printer or other devices, creating a channel allocates resources which may be deallocated, all or in part, when the channel is deallocated, just as using it to communicate may cost resources.

The objectives of this work are to

• define a formal notion of resources for concurrent processes, using the π-calculus
• define semantics for these resources
• devise mechanisms to allow the design of resource-aware protocols, able to adapt to the resources available and to take into account both allocation and deallocation of resources
• devise mechanisms to provide static guarantees of good usage of resources by an agent, with respect to a statically provided policy

Current status

We have isolated a formal notion of abstract resources. We have designed an extended π-calculus, the Controlled π-calculus (or Cπ), with semantics for allocation, deallocation and reuse of resources, taking advantage of a (parametric) mechanism for garbage-collection. This language was completed by a simple type system to guarantee resource bounds (i.e. to check before execution that a process will not use more resources than are available).

A second generation of cπ has been designed, with a notion of run-time resource state, more flexible mechanisms for allocation, deallocation, preallocation, asynchronous garbage-collection and run-time error handling. In particular, cπ provides a framework in which it is possible to model manual deallocation, automatic reference-counting, region-based resource management as well as graph exploration- based garbage-collection. As expected, in the general case, that sound and complete garbage-collection is undecidable.

This new cπ is completed by a more complex type system to guarantee statically some resource protocols (i.e. to check that some operations can only be performed once, that channels are never reused after some point...). In particular, using this cπ, we have been able to study complex systems such as concurrent bounded resource managers (e.g. print spoolers), which need to be able to handle reserves of resources, deal and recover these resources, pass resources from client to client, preempt resources in case of emergency, etc.

As cπ provides a framework for the study of garbage-collection in concurrent systems, one of the next step should be to study the set of decidable garbage-collection mechanisms.

A third generation of cπ, Teπc, has been designed, with the objective of providing a pragmatic framework for the implementation of complex resource-aware protocols. To the features of the previous generations, Teπc adds tools for describing arbitrary kinds of resources, with arbitrary operations, and embedding a low-level formalism/language inside the high-level control permitted by cπ.

We have applied Teπc to the treatment of Erlang. By defining a formal semantics of Erlang and of some of its standard library with Teπc, we provide formal guarantees for the use of resources by network services defined in Erlang.

We are currently studying the properties of Teπc, in particular the notions of resource ownership and resource composition, as well as its applications to distributed systems.

The Kell Calculus (2003-?)

Team

• Philippe Bidinger
• Tom Hirschowitz
• Alan Schmitt
• Jean-Bernard Stefani
• David Teller

Presentation

The Kell calculus is a reconfigurable higher-order process calculus, designed to study and implement component-based systems. The core of the Kell is an extension of the Join Calculus and the Seal Calculus. This formalism provides hierarchical localities, higher-order communications, dynamic binding and process-control operations.

Current status

Several generations of Kell calculus have been designed, improving gradually notions of (bi)simulation, the relations between static and dynamic binding, as well as higher-order communications and the possibility of defining resource-aware protocols. Through this work, we have been able to explore the interests and limitations of the model, isolate a robust set of core primitives, and to imagine the beginning of a programming paradigm for/with the Kell calculus.

A new generation of Kell calculus is currently in the works, redesigned to permit more pragmatic handling of components and component sharing, as well as a notion of module/library.

A prototype implementation of the latest (as of November 2005) stable version of the Kell calculus has been developed : CHALK, the Concurrent Hierarchies Architecture/Language of Kells. This distributed interpreter/virtual machine permits migration of processes and data among instances, (almost) unlimited number of threads, non-blocking system calls, etc. CHALK was written in OCaml 3.08 by Philippe Bidinger and David Teller.

Common Sense (2005-?)

Team

• Dan Chalmers
• Tim Owens
• David Teller
• Ian Wakeman
• Des Watson

Presentation

The Common Sense project applies some of the findings of the TrustUS project to the design and implementation of a resource management infrastructure for shared sensor networks.

Details

A sensor network is a system composed of of sensors and services. Sensors are typically devices with only little memory and power, able to provide some information to clients, either by interrupts or by polling. Some sensors are able to provide several kinds of informations in mutual exclusion (e.g. some cameras may provide images at different resolutions by need time to reconfigure themselves from one resolution to another). Some sensors have other resource limitations, such as battery power. Sensors typically do not have any notion of multi-users or concurrency. Services, on the other hand, are implemented on computers, with much less restrictions on their resources, and may often rely on protected concurrent executions.
Each sensor and each service of the network is described by the resources it requires to answer a call and the resources it provides.

Users may send requests to the sensor network. These requests may imply constraints of time, information, cost or other resources. The network itself is "hidden" behind a proxy server, who alone deals with matters of authorisations, billing and compilation.
Requests are combined and compiled into a concurrent execution language, in which matters of resource acquisition, transformation and release are made explicit. This language is based on the notion of channels, so as to allow distributed composition of components. Techniques of program transformation, scheduling and constraint-solving are used to determine whether requests may be fulfilled, and if there is a cost associated to that execution.
This set of operations also implement a step of type-safe compilation from the concurrent execution language into a larger language with explicit distributed scheduling/synchronisation and resource passing.
In turn, the explicit scheduling code is executed as a set of calls to drivers for sensor access or service access, progressively building the answer while minimising the amount of communication on the network and returning the final result directly to the user.

Status

The project is currently on hiatus, after the disbanding of University of Sussex' informatics lab.

TrustUS project (2004-?)

Team

• Tim Owens
• Julian Rathke
• Vladimiro Sassone
• David Teller
• Ian Wakeman

Presentation

The TrustUS project, formerly known as Third-Party Resource Usage for Pervasive Computing, aims at designing and implementing formal tools to

• describe resources and resource policies, allowing a process to find out
  • what service a given resource can provide
  • what it costs to use a given resource
  • what credentials an agent must have to be entitled to use the resource
  • ...
• describe requirements and perform resource negotiations and transactions between agents
  • ensuring that the resource acquired can perform the necessary service
  • exchanging the promised resources between agents
  • proving that an agent is entitled to use a resource
• keep unforgeable tracks of trustworthiness of agents and deduce notions of acceptable risks and acceptable costs

Status

The project is currently on hiatus, after the disbanding of University of Sussex' informatics lab.

By the way

TrustUS stands for Third-Party Resource Usage in Systems and Theory at University of Sussex.

Resource control in process algebras (2000-2004)

Team

• Daniel Hirschkoff
• David Teller
• Pascal Zimmer

with input from

• Davide Sangiorgi

Presentation

Before studying the problem of resources in the π-calculus, we attempted to understand the same problem in process algebras with site mobility, such as the calculus of Mobile Ambients, the calculus of Boxed Ambients, the Kell calculus or the Seals calculus. Although these calculi are more abstract than the π-calculus, insofar as terms written in these formalisms are not as close to actual concurrent programs as terms written in the π-calculus, they constituted an easier first step in our work on resources.

In process algebras with site mobility, mechanisms for allocation and deallocation are more immediate than in process algebras with information mobility, such as the π-calculus: entities (sub-sites) are created in specific places of the system (sites) and some instructions destroy or moved then. In particular, as allocations, deallocations or movements must be explicitly requested, it is not necessary to examine the effects of various automatic garbage-collection methods.

Status

We have defined a notion of abstract resource for calculi with site mobility.

In order to permit controlling the use and reuse of these resources, we have introduced a few primitives for reacting to allocations and deallocations, hence producing a few variants of the canonical process algebras we were working on: the Controlled Ambients, the Controlled Kells, the Controlled Seals, the Controlled Nomadic Pict and the Controlled NBAs.

For each of these modified calculi, we have designed a type system to control bounds on resource allocation, taking advantage of informations of deallocation and reuse of resources.

Our modification to the syntax and semantics of the Kell calculus has been adopted by the authors of this process algebra, with small changes, for the more recent versions of this language.

These results have permitted the ulterior work on resources in the π-calculus.

Perspectives

• studying TEπC and improving the results on resource analysis
• completing the design of an application language based on TEπC and implementing it
• implementing TEπC as a set of libraries for existing languages
• implementing tools for resource analysis of TEπC
• applying the results obtained for cπ/TEπC to existing distributed languages (probably either Acute or the next generation of Kell machine).