The PSI-Robuste Project is a cristallisation effort at LSV/CNRS UMR 8643 & ENS Cachan. PSI means "Protection des Systèmes d'Information". Its purpose is to explore ways of securing information systems based on cryptographic means and intrusion detection. Stress is put on static analysis of programs to detect vulnerabilities.
Duration is 2 years (not 3 as I previously wrote). This started in Fall 2002. Here is the short description of the project, in RTF format.
The main effort, initially, in the PSIrobuste project,
was to develop the CSur
static C code analyzer. This was eventually published as
•
J. Goubault-Larrecq and F. Parrennes. Cryptographic Protocol Analysis on Real C Code. In Proceedings of the 6th International Conference on
Verification, Model Checking and Abstract Interpretation
(VMCAI'05), Paris, France, January 2005, LNCS 3385, pages 363-379. Springer. ( PDF | BibTeX + Abstract )
The paper offers essentially a simplified view of what the CSur tool really
does. A more complete version will be submitted to TCS in April 2005.
Another gentle introduction to what CSur is really doing is given
in the slides presented at VMCAI'05.
Another major effort was to develop the ORCHIDS intrusion detection system. While this really started as part of the RNTL project DICO, from ideas presented in
•
M. Roger and J. Goubault-Larrecq. Log Auditing through Model Checking. In Proceedings of the 14th IEEE Computer Security Foundations
Workshop (CSFW'01), Cape Breton, Nova Scotia, Canada, June 2001, pages 220-236. IEEE Computer Society Press. ( PS | BibTeX )
the algorithm was then refined in a technical report:
•
J. Goubault-Larrecq. Un algorithme pour l'analyse de logs. Research Report LSV-02-18, Laboratoire Spécification et Vérification, ENS Cachan,
France, November 2002. 33 pages. ( PS | BibTeX )
In the course of implementing ORCHIDS, new techniques and models came up: interval logics, cuts (generalizing the so-called shortest runs of the above algorithm), entropy estimators (see Net-Entropy), in particular.
These results should be submitted during the year 2005.
ORCHIDS is now able to detect very subtle attacks: see the ORCHIDS Web page, and the tool demonstration paper, recently submitted to a conference.