Vérification de Machines Abstraites pour les Systèmes d’Exploitation – VeriAMOS

Les Systèmes d'Exploitation généralistes comme Linux sont de plus en
plus utilisés dasn des systèmes embarqués critiques, dans
l'automobile, le secteur médical et les systèmes cyber-physiques.
Toutefois, il es bien connu que les OS généralistes sont vulnérables
aux bugs. Récemment, de grands progrès ont été effectués dans la
vérification de noyaux d'OS, principalement à l'aide de méthodes
reposant sur des assistants de preuve interactifs. Toutefois, ces
techniques entraînent un coût énorme lié au temps nécessaire pour les
preuves non seulement lors de la conception et de l'implémentation,
mais aussi lors de la maintenance et de l'extension des OS. Par
conséquent, le passage à l'échelle de la vérification d'OS reste un
objectif difficile.

Une autre solution qui n'a pas été déployée sur des OS est l'analyse
statique automatisée de programmes. Un outil d'analyse statique
calcule des invariants de programmes et propriétés sémantiques sans
aide de l'utilisateur. Ces outils sont fondés sur des abstractions
décrivant les propriétés nécessaires pour exprimer des invariants et
de algorithmes permettant de les calculer. Bien que corrects, les
analyseurs statiques sont incomplets: autrement dit, ils peuvent
échouer à prouver un programme valide, et le considérer de manière
conservative "potentiellement incorrect". Les strutures de données
complexes, opérations bas-niveau et aspects concurrents des codes OS
aggravent les difficultés inhérentes à ces méthodes dans le cas des
OS.

Le projet VeriAMOS réunit des experts en analyse statique, systèmes
d'exploitation et langages dédiés, à INRIA, Sorbonne Université et à
l'Université de Grenoble, afin de développer une nouvelle solution à
la vérification de services systèmes, fondée sur l'utilisation de
langages dédiés et d'analyseurs statiques. Un langage dédié est un
langage reposant sur des abstractions spécifiques à une famille de
programme, et permet ainsi aux programmeur d'implanter une classe
spécifique d'algorithmes à un niveau plus abstrait et reposant sur un
compilateur pour générer le code final. En limitant l'expressivité,
ces langages contraignent les développeurs et empêchent la mauvaise
utilisation de fonctions des langages de programmation. L'idée
fondatrice du projet VeriAMOS est qu'en augmentant le niveau
d'abstraction et en limitant la variabilité des programmes, les
langages dédiés peuvent rendre possible la vérification automatique de
propriétés de correction importantes, sur des services systèmes réels.

Pour démontrer la faisabilité de cette solution, le projet VeriAMOS
considérera les séquenceurs d'entrées/sorties (I/O). Ces dernières
années de nouveaux et complexes séquenceurs I/O ont été introduits
pour tirer parti des SSDs, qui offrent des performances bien
meilleures que les disques classiques, et sont plus adaptées aux
systèmes embarqués du fait de leur résistance aux chocs. VeriAMOS a
pour ambition de vérifier des propriétés critiques des séquenceurs
I/O, comme la non corruption des requêtes et l'absence de famine. Les
défis principaux sont la conception, l'automatisation et la mise en
oeuvre des abstractions sous-jacentes à l'analyse statique et à la
définition d'un langage dédié haut niveau et expressif, garantissant
la génération de politiques de séquencement prouvablement correctes.
Pour surmonter ces défis, VeriAMOS développera une synergie entre les
domaines de l'analyse statique, des langages dédiés et des systèmes
d'exploitation.

Bien que le projet VeriAMOS se concentre sur le domaine des
séquenceurs entrées~/~sorties, nous sommes confiants que ce travail
ouvrira la route à de grands progrès dans l'automatisation de la
vérification de service systèmes. À long terme, tous les développeurs
systèmes pourront ainsi réaliser des services critiques entièrement
vérifiés, et non seulement quelques experts en preuve.