Synthèse des programmes de manipulation de pointeurs sûrs

Cette séance de cours de l'instructeur se concentre sur la synthèse des programmes de manipulation de pointeur de bas niveau sûrs en utilisant la technologie de synthèse de programme. L'exposé présente SuSLik, un synthétiseur de programme qui génère des programmes C sûrs à partir de spécifications logiques, mettant en valeur ses capacités à gérer les structures de données liées. La séance de cours couvre la synthèse déductive des programmes de manipulation de pointeurs, l'utilisation de la logique de séparation et l'application de la logique de séparation synthétique dans l'élaboration de programmes corrects par construction. Des exemples tels que l'échange des valeurs des pointeurs et l'élimination des listes sont démontrés, soulignant l'importance d'une synthèse correcte du programme dans l'élimination des bogues de sécurité de la mémoire.

À 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.

Séances de cours associées (19)

Concepts associés (88)

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

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.

Structure de données

En informatique, une structure de données est une manière d'organiser les données pour les traiter plus facilement. Une structure de données est une mise en œuvre concrète d'un type abstrait. Pour prendre un exemple de la vie quotidienne, on peut présenter des numéros de téléphone par département, par nom, par profession (comme les Pages jaunes), par numéro téléphonique (comme les annuaires destinés au télémarketing), par rue et/ou une combinaison quelconque de ces classements.

Linked data structure

In computer science, a linked data structure is a data structure which consists of a set of data records (nodes) linked together and organized by references (links or pointers). The link between data can also be called a connector. In linked data structures, the links are usually treated as special data types that can only be dereferenced or compared for equality. Linked data structures are thus contrasted with arrays and other data structures that require performing arithmetic operations on pointers.

Structure de données persistante

En informatique, une structure de données persistante est une structure de données qui préserve ses versions antérieures lorsqu'elle est modifiée ; une telle structure est immuable, car ses opérations ne la modifient pas en place (de manière visible) mais renvoient au contraire de nouvelles structures. Une structure est partiellement persistante si seule sa version la plus récente peut être modifiée, les autres n'étant accessibles qu'en lecture. La structure est dite totalement persistante si chacune de ses versions peut être lue ou modifiée.

Gestion de mémoire par régions

En informatique, la gestion de mémoire par région est un type de gestion de mémoire avec lequel chaque objet alloué est assigné à une région. Une région, alias une zone, une arène, ou un contexte mémoire, est une collection d’objets alloués qui peut être efficacement désallouée en bloc. Comme l’allocation par pile, les régions facilitent l’allocation et la désallocation de la mémoire à faible coût ; mais elles sont plus flexibles, permettant aux objets de vivre plus longtemps que la pile d’activation dans laquelle ils ont été alloués.

Analyse des structures de données: mise en œuvre vectorielle CS-119(c): Information, Computation, Communication

Analyse l'implémentation des vecteurs en C++, l'allocation de la mémoire, les recommandations d'utilisation et les techniques d'optimisation.

Structure des données avec les listes liées CS-119(c): Information, Computation, Communication

Comparer les listes liées avec les tableaux/vecteurs en termes de coût d'accès à la mémoire et introduire les listes liées comme une structure de données plus efficace pour certaines opérations.

Introduction à la programmation C ENG-270: Computational methods and tools

Introduit des concepts fondamentaux de programmation C, couvrant les variables, les structures de contrôle, les fonctions et les pointeurs, avec des exemples pratiques et des exercices.

MIPS Assemblage: Fonction Appels & Gestion de la mémoire CS-200: Computer architecture

Explore le langage d'assemblage MIPS, couvrant les appels de fonctions, la gestion de la mémoire et les structures de données, y compris les fonctions récursives, les constructions de programmation, les tableaux et les listes liées.

Laboratoire de génération de code CS-320: Computer language processing

Couvre la génération de code pour un compilateur, traduisant un programme Amy à WebAssembly, y compris la gestion de la mémoire et la compilation de correspondance de motifs.