100
Science de la sécurité du système d’information
Deuxième partie
On aura compris que B est un système de développement complet, qui comporte
son propre langage de programmation, ce qui confirme en fait l’idée qu’une méthode de spécification est soit un langage de programmation, soit inutile, et que de
toute façon la création d’un système informatique demande une vraie compétence
en programmation. Il semble clair que les exigences de B en termes de délais et
de qualification technique du personnel sont relativement élevées par rapport à du
développement classique de logiciel non critique. Le tout est de ne pas se tromper
dans la détermination de ce qui est critique et de ce qui ne l’est pas.
Lors du développement des 100 000 lignes de code Ada critique pour le logiciel du
métro METEOR, l’atelier B a produit 30 000 obligations de preuve, dont plus de
90% ont été réalisées automatiquement. Les quelque 2 500 preuves qui ont résisté
aux procédures automatiques ont nécessité plusieurs mois de travail humain, mais
l’industriel a estimé que le bilan était largement positif grâce à l’économie engendrée par la suppression des tests de bas niveau. Après quelques années d’exploitation sans incident notable, la conclusion s’impose que la méthode B est efficace et
sûre pour les développements critiques.
Pour être complet il faut également signaler les limites de la méthode B :
• les capacités de preuve sur des formules comportant des opérations arithmétiques sont limitées ;
• le développement formel de systèmes contenant des calculs numériques
n’est actuellement pas possible avec la méthode B et les outils associés ;
de tels calculs restent sous-spécifiés et les preuves de correction ne peuvent
être données ;
• absence de vérification de propriétés temporelles due à la logique supportée
(par l’atelier B) ;
• on ne peut pas décrire avec B les phénomènes concurrents, les fenêtres de
temps et plus généralement le temps réel (codage des événements par des
variables) ; les logiques temporelles sont plus adaptées pour spécifier le comportement dynamique.
Perl en mode souillé
Le langage Perl [5] propose une méthode de sécurité statique plus prosaïque mais
plus facile à mettre en œuvre : le mode souillé (taint mode), qui déclenche des mesures de sécurité particulières. Le mode souillé est activé automatiquement dans
Science de la sécurité du système d’information
Deuxième partie
On aura compris que B est un système de développement complet, qui comporte
son propre langage de programmation, ce qui confirme en fait l’idée qu’une méthode de spécification est soit un langage de programmation, soit inutile, et que de
toute façon la création d’un système informatique demande une vraie compétence
en programmation. Il semble clair que les exigences de B en termes de délais et
de qualification technique du personnel sont relativement élevées par rapport à du
développement classique de logiciel non critique. Le tout est de ne pas se tromper
dans la détermination de ce qui est critique et de ce qui ne l’est pas.
Lors du développement des 100 000 lignes de code Ada critique pour le logiciel du
métro METEOR, l’atelier B a produit 30 000 obligations de preuve, dont plus de
90% ont été réalisées automatiquement. Les quelque 2 500 preuves qui ont résisté
aux procédures automatiques ont nécessité plusieurs mois de travail humain, mais
l’industriel a estimé que le bilan était largement positif grâce à l’économie engendrée par la suppression des tests de bas niveau. Après quelques années d’exploitation sans incident notable, la conclusion s’impose que la méthode B est efficace et
sûre pour les développements critiques.
Pour être complet il faut également signaler les limites de la méthode B :
• les capacités de preuve sur des formules comportant des opérations arithmétiques sont limitées ;
• le développement formel de systèmes contenant des calculs numériques
n’est actuellement pas possible avec la méthode B et les outils associés ;
de tels calculs restent sous-spécifiés et les preuves de correction ne peuvent
être données ;
• absence de vérification de propriétés temporelles due à la logique supportée
(par l’atelier B) ;
• on ne peut pas décrire avec B les phénomènes concurrents, les fenêtres de
temps et plus généralement le temps réel (codage des événements par des
variables) ; les logiques temporelles sont plus adaptées pour spécifier le comportement dynamique.
Perl en mode souillé
Le langage Perl [5] propose une méthode de sécurité statique plus prosaïque mais
plus facile à mettre en œuvre : le mode souillé (taint mode), qui déclenche des mesures de sécurité particulières. Le mode souillé est activé automatiquement dans