security of information systems – PARSEC

Some new applications, like web servers, multi-player games or Internet-scale storage applications are
inherently massively concurrent, and open to untrusted parties. These applications require adequate
programming techniques, and some of them involve security issues. The traditional process model is not
well-suited for these applications, where a fair amount of sharing is required. In the past few years, it has
been recognized that kernel threads are too restrictive and too inefficient to provide a convenient means
for programming these applications, and that a user-level thread facility would provide better support.
Whether this should follow a preemptive discipline, or an event-driven model, or a cooperative style is
still a research matter.
Similarly, the well-established technologies (e.g. sand-boxing) for security are inadequate in the case
where a number of concurrent activities should share an address space. Moreover, access control has
to be complemented, in multi-threaded applications, with new security policies, ensuring for instance
that a thread does not consume common resources in an immoderate way, or corrupt them, or disclose
confidential information to other threads having low access rights.
Our PARSEC (for PARallelism and SECurity, where “parallelism” should here be understood as “concurrency”)
project intends to study concurrent programming techniques for these new applications, focusing
on the security issues that arise in multi-threaded systems. Our main objective is to understand what
could be an efficient and “security-minded” concurrent programming model. Such a model should both
be convenient for programming the kind of applications mentioned above, and support mechanisms to
ensure high-level security policies. To achieve this objective we will have to study well-known models,
like Java multi-threading, Posix threads or shared memory models, as well as less standard ones, like the
cooperative model which is gaining some popularity in user-level thread systems, or the synchronous model.
We will have to understand what are the right safety and security properties to guarantee regarding
multi-threaded systems, like for instance the “non-interference” property, which is not so clear in this
case, or the “availability” property, meaning in particular that a single thread should not monopolize
any shared resource. We will also have to design and study means to ensure these properties, using and
adapting standard tools like type systems, program logics (including Floyd-Hoare logic, temporal logics,
or Reynolds' separation logic) or run-time verification mechanisms.
There are many difficulties in this task. First of all, the semantics of multi-threaded programming is not
at all well understood, for a number of reasons (analyzed in our proposal). Moreover, synchronization
is a delicate matter, even at the language level, and all this makes the classical (i.e. preemptive) multithreaded
programming extremely difficult, and error prone. It is then necessary to design some techniques
to analyse concurrent programs in order to make them “thread safe”. Besides the study of this classical,
preemptive model, one may also explore, as we plan to do, the use of cooperative threads at the language
level. This is by now advocated as a better model for applications like the ones mentioned above, but this
programming style is not free of defects. In particular, cooperative programs have to indeed cooperate,
in order not to make the other threads starving for the processor, and there is by now no well established
technique to guarantee cooperation for programs written in an expressive language. The same problem
arises with the synchronous programming style. A fair amount of basic research has therefore to be done
in order to design a concurrent model in which programming massively concurrent applications would be
reasonably safe.
5
Multi-threaded applications also raise some difficult questions regarding security. As we indicated above,
in such applications access control has to be complemented with information flow control, and resource
usage control. It is well-known that secure information flow is difficult to formalize in a concurrent
setting, due to the various kinds of leaks that can arise, like termination leaks or timing leaks. Moreover,
even for weak notions of secure information flow, most of the well-known techniques (e.g. type systems)
for enforcing such security properties are far too restrictive to be of practical use. We believe that the
cooperative model for concurrency is better suited than the preemptive one for a language-based approach
to information flow security, because in this model the flow of control is determined at the programming
level, but this belief has still to be proved right by some formal results. As a matter of fact, some difficult
questions regarding secure information flow already arise in a purely sequential setting. For instance,
we still lack an adequate treatment of exception mechanisms `a la Java ; also, secure information flow
(non-interference) should be made closer, in one direction or the other, to static analysis techniques (type
systems) that are meant to enforce it. Similarly, although multi-threaded applications provide a strong
motivation for studying resource usage control, there is still no well-established technique that would
provide, in the sequential case, static means to enforce reasonably accurate bounds on resource usage.
Even the standard issue of access control needs further investigation, to formally understand for instance
what exactly is guaranteed by the run-time protection mechanisms in Java.
Our proposal is to make contributions to solving all the above mentioned problems, aiming at providing,
at the end of the project, solid foundations for what could be a safe and secure concurrent programming
model. As regards the methodology, we shall follow in the PARSEC proposal a language-based approach
to address in a formal way security issues such as access control, secure information flow, and resource
usage control, focusing in particular on concurrent programming constructs, and especially on cooperative
concurrency. To this end, we have built a coherent group made of five teams, namely the Concurrency
group (R. Amadio) at the PPS Lab of Paris 7 University and CNRS, the Everest (G. Barthe) and
Mimosa (G. Boudol) teams at INRIA Sophia Antipolis, the Lande (T. Jensen) team at IRISA, and
the Moscova (J.-J. L´evy) team at INRIA Rocquencourt, sharing their expertise in concurrency and/or
security. The scientific results obtained in our project will be communicated at workshops and conferences,
and published in technical journals. We will, as far as possible, experiment our ideas via prototype
software, but we do not expect these to provide pre-competitive technology that could be directly exploited
industrially.