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.

Short version

Catch me if you can is a small library for OCaml 3.10. The latest release is version 0.2, which you may find here. This library improves management of errors in OCaml. It is released under the LGPL licence. It has been written by David Teller, Arnaud Spiwack, Till Varoquaux and Gabriel Scherer.

Lisez la suite de cette entrée »

A new version of the exception monad for OCaml is now available for download. It’s now richer, comes with extensive syntactic sugar and a brand new system of compile-time optimizations. More on this in the corresponding research paper — and whenever I find the time, on this blog.

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.

A quick note to inform you that the repository for Extrapol is now public. The source code as available on the repository does not have a licence yet and will not compile as such, due to dependencies on libraries available somewhere else. Stay tuned for an actual release.

Update: Sorry, repository cut off by the administrator. I’ll inform you when the sources are back.

Note rapide pour vous informer que le code source d’Extrapol est maintenant disponible au public. Il ne s’agit pas encore d’une version officielle — en particulier, le code n’a pas encore de licence et il manque des bibliothèques (disponibles ailleurs). Plus de détails dès qu’une version officielle est disponible.

Additif: Désolé, je viens d’apprendre que le dépôt de source a été isolé par l’administrateur. Je vous tiendrai au courant dès que le code source est de nouveau public.

Après un billet dans la langue de Turing, voici une présentation d’Extrapol en version française. En quelques mots, le projet Extrapol (pour Extraction de Politiques de Sécurité) vise à combler un vide dans le jeu d’outils dont dispose l’administrateur pour maintenir un système dans un état sûr.

Lisez la suite de cette entrée »

Here comes the long-promised description of Extrapol, my main ongoing research project. In a few words, our objective with Extrapol is to fill a hole in the current suite of tools built to ensure the security of systems. While there’s an ample amount of stuff designed to analyse the behaviour of processes either during their execution (dynamic analysis) or after their completion (trace analysis), there is little work on applying static analysis to actual system security.

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.

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 »