Intégrité du noyau et systèmes en temps réel

Description

Cette séance de cours explore les propriétés critiques de l'intégrité du noyau et la vérification des spécifications du noyau pour assurer la sécurité du système. L'instructeur explique l'importance de prouver l'exactitude fonctionnelle, la sécurité de la mémoire et la terminaison dans la construction de systèmes réels. La séance de cours couvre également les concepts d'intégrité, de disponibilité, de confidentialité et d'actualité dans le contexte d'un système basé sur les capacités. La discussion s'étend à la vérification des pires temps d'exécution pour la construction de systèmes en temps réel, en soulignant le besoin de composants matériels et logiciels fiables. La séance de cours se termine par un aperçu de la synthèse des pilotes de périphériques et des systèmes de fichiers à partir de spécifications de haut niveau pour améliorer la fiabilité du système.

Connectez-vous pour regarder la vidéo

Source officielle

https://mediaspace.epfl.ch/media/0_mn9bbkk8

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (11)

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Terminaison d'un algorithme

La terminaison est une propriété fondamentale des algorithmes. Elle stipule que les calculs décrits par l'algorithme s'arrêteront. En général cet arrêt doit avoir lieu quelles que soient les données initiales que l'on fournit à l'algorithme. Si l'on veut insister sur ce point on parle alors souvent de terminaison uniforme, mais le plus généralement « terminaison » couvre aussi bien l'arrêt sur une donnée que l'arrêt sur toutes les données et c'est le contexte qui décide.

Correction d'un algorithme

Un algorithme est correct s'il fait ce qu'on attend de lui. Plus précisément, rappelons qu'un algorithme est décrit par une spécification des données sur lesquelles l'algorithme va démarrer son calcul et une spécification du résultat produit par l'algorithme. Démontrer la correction de l'algorithme consiste à démontrer que l'algorithme retourne, quand il calcule en partant des données, un objet qui est un des résultats escomptés et qui satisfait la spécification du résultat comme énoncé dans la description de l'algorithme.

Formal specification

In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verifying key properties of interest through rigorous and effective reasoning tools. These specifications are formal in the sense that they have a syntax, their semantics fall within one domain, and they are able to be used to infer useful information.

Memory safety

Memory safety is the state of being protected from various software bugs and security vulnerabilities when dealing with memory access, such as buffer overflows and dangling pointers. For example, Java is said to be memory-safe because its runtime error detection checks array bounds and pointer dereferences. In contrast, C and C++ allow arbitrary pointer arithmetic with pointers implemented as direct memory addresses with no provision for bounds checking, and thus are potentially memory-unsafe.