Stages M2 langages de programmation

Mise-à-jour:

Merci pour toutes les (très bonnes) candidatures aux stages que nous avons proposé. Tous les stages ont été pris.

À bientôt pour la prochaine version d’OPA.

We call it OPA

Web applications are nice. They’re useful, they’re cross-platform, users need no installation, no upgrades, no maintenance, not even the computing or storage power to which they are used. As weird as it may sound, I’ve even seen announcements for web applications supposed to run your games on distant high-end computers so that you can actually play on low-end computers. Go web application!

Of course, there are a few downsides to web applications. Firstly, they require a web connexion. Secondly, they are largely composed of plumbing. Finally, ensuring their security is a constant fight.

Firefox, les extensions et la sécurité

Il y a environ un an, un de mes collègues travaillait sur un dispositif de communication pour les services d’urgence. Ce dispositif, prévu pour être utilisé lors de catastrophes naturelles ou d’attentats terroristes majeurs, devait permettre une meilleure synchronisation entre la police, les pompiers et les équipes de secouristes. Ah, et au cas où il se serait effectivement agi d’un attentat, le dispositif se devait d’être sûr. Conclusion du collègue en question : “comme Firefox est sûr, je vais faire cela sous la forme d’une extension Firefox, et ça sera sûr.”

À ce stade, j’espère que vous êtes déjà en train de vous moquer intérieurement de mon collègue. Cela dit, savez-vous effectivement quel risque vous courez en écrivant une extension ? Savez-vous quel risque vous faites courir à l’utilisateur ? Et savez-vous à quel point vous pouvez compter sur la plateforme Mozilla pour vous aider à écrire des extensions ou des applications sûres ?

À l’occasion, je tâcherai d’écrire un article détaillé sur le sujet. En attendant, pour ceux qui se posent des questions, voici les transparents (en français) de l’exposé que j’ai donné samedi dernier au Mozilla Add-Ons Workshop de Paris.

Ah, un indice : ayez peur.

Stage M2 Système et Langages de Programmation

Note De nouveaux stages sont proposés pour l’année 2009-2010.

L’entreprise MLState et l’équipe SDS (Sécurité et Distribution des Systèmes, équipe du Laboratoire d’Informatique Fondamentale d’Orléans) proposent un stage de Master 2 dans le domaine de l’analyse statique de sécurité, sous la supervision de David Teller (SDS) et Henri Binsztok (MLState).

Post-doctorate position in Programming Language Design

Start-up MLState and team SDS (Security of Distributed Systems, part of Laboratoire d’Informatique Fondamentale d’Orléans) offer a post-doctorate position in the domain of Programming Language Design, under the supervision of David Teller (SDS) and Henri Binsztok (MLState).

Post-doctorat en langages de programmation

L’entreprise MLState et l’équipe SDS (Sécurité et Distribution des Systèmes, équipe du Laboratoire d’Informatique Fondamentale d’Orléans) proposent un poste de post-doctorat dans le domaine de la conception de langages de programmation, sous la supervision de David Teller (SDS) et Henri Binsztok (MLState).

Bourse de doctorat dans l’équipe SDS avec le CEA

Le CEA (Commissariat à l’Énergie Atomique) et l’équipe SDS (Sécurité et Distribution des Systèmes, équipe du Laboratoire d’Informatique Fondamentale d’Orléans) proposent une bourse de doctorat dans le domaine de la Sécurité Appliquée ou des Fondements Théoriques de la Sécurité, sous la supervision administrative de Mathieu Blanc (CEA) et Christian Toinard (SDS).

La bourse dure trois ans (renouvelables) et couvre un salaire brut de  1990,25€ par mois (première et deuxième année)  à  2049,75€/mois (troisième année).Le poste est disponible à partir du premier octobre 2008.

Compétences et parcours

Idéalement, le candidat doit avoir un excellent Master 2 d’informatique et un intérêt en Sécurité des Systèmes ou en Méthodes Formelles. De plus, le candidat doit avoir des connaissances dans au moins un des domaines suivants :

• sécurité des systèmes
• systèmes d’exploitation
• systèmes distribués
• programmation système
• clusters
• analyse statique
• théorie des graphes
• théorie du parallélisme
• logique formelle
• sémantique dénotationnelle
• sémantique opérationnelle
• aspects théoriques de la sécurité et de la confiance.

Les candidats doivent avoir le droit de travailler en France et seront affectés sur le campus de l’ENSIB (École Nationale Supérieure d’Ingénieurs de Bourges). Leur tâche première concernera la théorie ou/et l’implantation de mécanismes efficaces de garantie de politiques de sécurité pour des systèmes distribués tels que les grilles et les clusters. L’objectif principal de ce doctorat est d’étendre les approches actuelles de garantie locale de politiques de sécurité pour en construire des techniques applicables à de vastes systèmes distribués, tels que ceux utilisés pour l’analyse de données ou l’analyse numérique.

Pour candidater

Pour candidater, nous vous invitons à envoyer un CV et une lettre de motivation, par courrier physique ou électronique, à Christian Toinard et Mathieu Blanc. Si possible, joignez un échantillon de vos travaux scientifiques. La candidature implique une vérification de sécurité par le Ministère de la Défense.

PhD position in either Applied Security or Foundations of Security

A PhD position in Security is to be filled in CEA (Commissariat à l’Énergie Atomique) and team SDS (Security of Distributed Systems, part of Laboratoire d’Informatique Fondamentale d’Orléans), in France, on the topic of Mandatory Access Control for Distributed Systems, under the administrative supervision of Mathieu Blanc (CEA) and Christian Toinard (SDS).

Studentship is for three years (renewable) and includes a salary rising from €1990.25/month (during years 1 and 2)  to €2049.75/month (during year 3). The earliest start date is October 1st 2008.

Profile and skills

The ideal candidate should have an excellent undergraduate degree/Master 2 in Computer Science and an interest in either System Security or Formal Methods. Candidates should have a background in one or more of the following areas:

• system security
• operating systems
• distributed systems
• system programming
• clusters
• static analysis
• graph theory
• theory of concurrency
• logics
• denotational semantics
• operational semantics
• foundations of trust.

Candidates should be eligible to work in France and should expect to work on-campus in ENSIB (École Nationale Supérieure d’Ingénieurs de Bourges). They will work on the theory and/or implementation of effective and manageable enforcement mechanisms for security policies in distributed systems such as clusters and grids.  The main objective of this PhD is to build upon existing local enforcement mechanisms for security policies to design (and, if possible, implement) techniques which may be applied for large distributed systems, as used for data analysis or numeric analysis.

Application procedure

To apply, please send your resume and a motivation letter, either by e-mail or by paper-mail, to both Christian Toinard and Mathieu Blanc. If possible, join a sample of your academic work. The application process entails a background check by the French Department of Defense.

Extrapol update

A quick work regarding the current status of Extrapol and its release.

Development of Extrapol progresses. With our current set of sample, Extrapol works flawlessly. We’re now adding features, improving error reporting and de-hard-wiring the model of the C standard library from the tool and moving it towards an external configuration file as well as progressively moving towards larger and more realistic samples. Development will come to an abrupt (and temporary) halt at the end of this week, though, due to personal matters (i.e. I’m getting married).

The release planned for next week, on the other hand, is canceled. As the research field of applied security is very competitive, and after careful discussion with the rest of my research team, we have decided to only release a version of Extrapol after the scientific content has been accepted for publication in a conference or journal. At the request of one of the institutes which founds this research, I will also refrain from posting detailed information on the theory and algorithms behind Extrapol, until these are cleared by the institute and accepted for publication. Without entering the details, Extrapol is expected to serve in critical infrastructures, which explains the need for clearance.

However, rest assured that there will be a release and it will be open-source (presumably licenced under a combination of MIT and LGPL). The only question is when — and this probably won’t happen before November.

Extrapol and Korset

A colleague recently pointed me towards Korset, a program developed by Ohad Ben-Cohen and Avishai Wool promising features comparable to Extrapol. While I must admit I’m slightly skeptical about the promise of “provable zero false alarm” — since the problem is undecidable, usually people tend to develop “provably complete” rather than “provably sound” analysis — it sounds like an interesting development.

Now, from what I understand, Korset will be presented to Blackhat in a few months, and the rules of the conference forbid the developers from giving away any detail. Until then, we have no way of comparing the unreleased Extrapol and the equally unreleased Korset.

Note: the tarball for the first prototype of Extrapol is waiting on my hard-drive for release clearance. I hope I’ll be able to release it next Tuesday or Wednseday. Stay tuned.