As I mentioned a few months ago, two master students of mine have been working for the best part of one year on improving the security of extensions in Firefox and Thunderbird. To sum up the current situation in Firefox, extensions have no protection mechanism from each other, nor is the core of Firefox protected in any way from extensions. The objective of this work was to design and implement a mechanism allowing system administrators to define fine-grained policies for accepting or rejecting interactions between extensions or between extensions and the core of Firefox.

Lisez la suite de cette entrée »

As mentioned a few times, I have (had) two students working on a Thunderbird extension to support confidentiality and help avoid involuntary leaks of critical information by e-mail. Yesterday, these students officially turned this project in, which gave me and my colleagues the opportunity of reviewing the code and documentation.

So, what works ?

• The Thunderbird extension can detect that you’re trying to send e-mail to someone with a lower level of accreditation — although, for the moment, it gets confused easily. For this purpose, it may use either SELinux or a text database of recipients.
• The Thunderbird extension can warn you that you need to sanitize and decrease confidentiality of the information and can mark the outgoing e-mail as sanitized for a given level — the UI needs a bit polish, but that works.
• The Sendmail extension can detect that you’re trying to send e-mail to someone with a lower level of accreditation — although, for the moment, it gets confused just as easily and is subject to a number of security holes.
• The Sendmail extension can reject unsanitized e-mail going to unaccredited targets — logging needs a bit of polish, but that works.
• That’s it.

All in all, that’s about 150 lines of code in JavaScript, XUL, C and C++. Not quite ready for prime-time but a good 0.1 release. I expect either the students or I will upload it somewhere for public release in the near future.

Lorsque vous lirez ces lignes, la première Academic Pride aura probablement déjà eu lieu. Une Academic Pride, oui, tout comme la Gay Pride et les autres défilés de minorités obscures, ou exploitées, ou ignorées,ou méprisées, ou ghettoïsées.

Alors pourquoi une Academic Pride ? Parce que l’université française est actuellement l’une des cibles directes du pouvoir en place. Parce que, malgré les habituels discours sur l’importance du Savoir et de la Recherche, malgré les références aux Lumières, l’université est en passe d’être sacrifiée sur l’autel de l’idéologie au pouvoir. “Sacrifiée” — non, l’image est peut-être trop forte. En fait, l’université est en passe d’être jetée d’un geste négligent, avec le collège et le lycée public, le baccalauréat et la politique culturelle, toutes ces vétustés qu’il est à la mode de condamner au nom de critères fantaisistes et de réformer à la va-vite et en dépit du bon sens.

Lisez la suite de cette entrée »

A few weeks ago, I promised I would tell you more about ExtraPol, my current research project. Well, before doing so, here’s a short reminder about the notion of security in computer science — and the manners of enforcing that security.

While most members of the computer science community agree that safety and security are desirable properties, there is little consensus on the methods to be used for ensuring safety or security. Indeed, even the actual meaning of these properties often remains an open question.

One possibility is to define security in terms of authorizations and safety in terms of real-world hazard. In this context, a system or subsystem is therefore secure if there is no way for something forbidden to happen, while it is safe if its use may only cause acceptable risks. Both notions are very broad and their enforcement is far from trivial. Even the reduced problem of ensuring that the installation and execution of a software application will not breach simple cases of security of a desktop station is an open research issue.

In practice, techniques used or investigated in the domain of security tend to fall roughly into three groups:

• static analysis — try and detect security holes before running the program
• dynamic analysis — try and detect security breaches as they happen
• trace analysis — try and detect security breaches after they have happened.

Lisez la suite de cette entrée »

An updated version of the Lazy List module for OCaml has just been uploaded to Batteries Included and submitted to ExtLib. See the release notes for more details.

In addition, I am currently using this module to write a parser combinator library for OCaml. This library has reached early testing stage and will hopefully be added to Batteries Included soon.

A few months ago, I introduced “MLS for Thunderbird“, an on-going effort to add support for confidentiality in Thunderbird. After long months of silence, it seems that this student project, undertaken by Vincent Tarbouriech and Roland Thaisong, two Master Students in ENSI Bourges, is finally getting somewhere.

This extension interfaces with the underlying operating system (SELinux for now) to determine your security level and, if possible, that of your correspondants. If you attempt to send an e-mail to some recipient whose security level is inferior to yours, Thunderbird will warn you that a declassification is going to happen. Lisez la suite de cette entrée »

I have made available the first preview of a second module for OCaml Batteries Included module: Enum. This module builds upon ExtLib’s enumerations (which it means to replace, if it is accepted upstream) and provides support for representation-independent iterators. These iterators are used pervasively in ExtLib and will also be used pervasively in the rest of Batteries Included, as a manner of converting data from/to data structures and as a base for syntax extensions.

With respect to ExtLib’s current implementation, this release adds

• numerous powerful constructors and manipulation functions
• functions inspired from SDFlow and dedicated to cooperative
• better management of infinite iterators
• better management of iterators created using from
• syntactic sugar.

As an example of the last point, let us note that it is now possible, without any Camlp4 extension, to replace for loops with a more (stream-)functional counterpart. That is, instead of

for i = 1 to n do
    (*...*)
done

one may now write

iter (fun i -> (* ... *) )
  (5 -- 10)

for an imperative loop or

map (fun i -> (* ... *) )
  (5 -- 10)

for a lazy transformation, etc. It won’t improve performance and it doesn’t look more readable at first glance, but it allows short expressions such as :

iter printf (5 -- 10) (*to print all numbers between 5 and 10*)
map ( ~ ) (5 --10) (*to obtain enumeration -5, -6, -7, -8, -9, -10 *)
fold ( + ) 0 ( 5 -- 10 )(*to sum all numbers between 5 and 10*)

etc. Everything is computed lazily, without allocating any intermediate data structure.

Code may be found here.

Ces jours-ci, je travaille beaucoup avec et sur OCaml, que ce soit pour le projet ExtraPol (dont je finirai bien par vous glisser quelques mots) ou pour Batteries Included (la rénovation en cours de la bibliothèque standard de OCaml). En particulier, je viens de finaliser un module de gestion des listes paresseuses. Paresseuses ? Oui, paresseuses.

Attardons-nous un moment sur le concept de paresse en programmation.

Lisez la suite de cette entrée »

A quick note to inform that I have made available the first preview of a module for OCaml Batteries Included module: Lazy Lists for OCaml. This module adds the ability to manipulate lists composed of elements which are only computed whenever their value is first needed. In particular, such lists may be used as a more powerful replacement for streams — or to port interesting algorithms from Haskell.

Code may be found here.