Parallelism and Security
| INRIA Sophia-Antipolis, coordinator. | (contact: Gérard Boudol) |
| PPS - Université Paris 7 | (contact: Roberto Amadio) |
| INRIA Rocquencourt | (contact: Francesco Zappa Nardelli) |
| INRIA Rennes | (contact: Thomas Jensen) |
The ParSec project is funded by SetIn 2006, a program of the Agence Nationale de la Recherche.
The ParSec project intends to study concurrent programming techniques for new computing architectures like multicore processors or multiprocessor machines, 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. We will have to understand what is 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.
The Technical Annex to the contract contains a detailed description of the objectives of the ParSec project.