Articles


Lundi, 30 Jan 2017

CertiKOS: une évolution énorme vers les systèmes d'exploitation résistant aux pirates



Cyber Security

Une équipe de chercheurs de Yale a dévoilé CertiKOS, le premier système d'exploitation au monde qui fonctionne sur des processeurs multi-cœurs et des boucliers contre les cyber-attaques, une jalon que les scientifiques disent pourrait conduire à une nouvelle génération de logiciels de systèmes fiables et sécurisés.


Dirigés par Zhong Shao, professeur d'informatique à Yale, les chercheurs ont développé un système d'exploitation qui intègre la vérification formelle pour s'assurer qu'un programme fonctionne exactement comme ses concepteurs ont prévu - une prévention qui pourrait empêcher le piratage de n'importe quel équipement, allant de l'Internet des objets (IoT) aux voitures auto-conduites et à la monnaie numérique.


Les informaticiens pensent depuis longtemps que les systèmes d'exploitation des ordinateurs devraient avoir à leur base un petit noyau fiable qui facilite la communication entre les logiciels et le matériel des systèmes. Mais les systèmes d'exploitation sont compliqués, et il suffit d'un simple lien faible dans le code - un lien qui est pratiquement impossible à détecter via les tests traditionnels - pour qu'un système soit vulnérable aux pirates.


L'une des principales évolutions de CertiKOS, par rapport aux autres systèmes d'exploitation, est qu'il prend en charge la simultanéité, ce qui signifie qu'il peut simultanément exécuter plusieurs threads (petites séquences d'instructions programmées) sur plusieurs noyaux d'unité de traitement central (CPU). Cela place CertiKOS dans une catégorie à part par rapport aux autres systèmes précédemment vérifiés et permet à CertiKOS de fonctionner sur des machines multi-cœurs modernes. L'architecture de CertiKOS est également conçue pour être très extensible, c'est-à-dire qu'elle peut supporter de nouvelles fonctionnalités et être utilisée pour différents domaines d'application.


La simultanéité permet l'exécution imbriquée de plusieurs threads de programme, ce qui rend impossible de considérer toutes les circonstances et d'éliminer tous les problèmes dans le système via les tests traditionnels. Beaucoup d'experts ont longtemps cru que la complexité d'un tel système rend la vérification formelle de la correction fonctionnelle problématique ou très coûteuse.


«La construction de logiciels qui fonctionnent correctement a été l'un des grands défis de l'informatique depuis le milieu du XXe siècle», a déclaré Anindya Banerjee, directrice de programmes à la National Science Foundation (NSF), qui finance le projet CertiKOS. "CertiKOS démontre qu'il est possible et pratique de construire un logiciel vérifié qui en plus fournit des preuves - des preuves mathématiques vérifiables par machine - qu'il est fonctionnellement correct."


Dans la construction du système CertiKOS, Shao et son équipe intègrent une logique formelle et de nouvelles techniques de vérification déductive en couches. C'est-à-dire qu'ils décomposent soigneusement les composants interdépendants du noyau, organisent le code en une grande collection de modules hiérarchiques et écrivent une spécification mathématique pour le comportement prévu de chaque module du noyau. L'utilisation de la vérification formelle déductive pour certifier le système diffère de la méthode conventionnelle de vérification de la fiabilité d'un programme, dans laquelle le rédacteur du code teste le programme contre de nombreux scénarios.


"Un programme peut être écrit 99% correctement - c'est pourquoi aujourd'hui vous ne voyez pas les problèmes évidents - mais un pirate peut toujours se faufiler dans une configuration particulière où le programme ne se comportera pas comme prévu", a déclaré Shao. "La personne qui a écrit le logiciel a travaillé avec toutes les bonnes intentions, mais ne pouvait pas considérer tous les cas."


Le kernel du système d'exploitation CertiKOS est un élément clé du programme HACMS (High Assurance cyber Military Systems) de l'Agence de Recherche Avancée de la Défense (DARPA), qui est utilisé pour construire des systèmes cyber-physiques qui sont manifestement exempts de vulnérabilités cybernétiques.


«L'équipe HACMS utilise la capacité de virtualisation fournie par CertiKOS pour séparer les composants fiables des composants non fiables», a déclaré Ray Richards, directeur de programmes à la DARPA. «C'est une capacité importante qui nous permet de construire efficacement des systèmes cyber-résilients. Dans le monde où la cybersécurité est une préoccupation croissante, cette résilience est un attribut puissant que nous espérons qu'il sera largement adopté par les concepteurs de systèmes.


La création d'un système comme CertiKOS serait possible seulement au cours des dernières années, puisque les épreuves pour un noyau certifié sont trop grandes pour n'importe quel humain à vérifier.


«C'est un progrès étonnant», a déclaré Greg Morrisett, un expert en sécurité des logiciels et doyen de l'informatique et des sciences de l'information à l'Université de Cornell. "Il y a dix ans, personne ne pourrait prédire que nous pourrions prouver l'exactitude d'un noyau à coeur unique, et encore moins un noyau à multi-coeurs. Zhong et son équipe ont vraiment ouvert une piste spectaculaire pour le reste d'entre nous. "



Source :
CertiKOS: A breakthrough toward hacker-resistant operating systems