Séance de cours

Compilation officiellement sécurisée : assurer la sécurité des composantes

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Description

Cette séance de cours de l'instructeur s'inscrit dans le concept de compilation formellement sécurisée, en mettant l'accent sur les défis d'assurer la sécurité face à un compromis dynamique. La présentation porte sur la recherche sur les fondations de sécurité, les mécanismes d'application de la sécurité et l'importance des preuves mathématiques pour garantir les propriétés de sécurité. La séance de cours explore l'initiative Project Everest, qui vise à améliorer la sécurité HTTPS grâce à des protocoles de communication vérifiés. Il traite également d'EverCrypt, un fournisseur de cryptogramme vérifié, et de l'importance de la compartimentation pour atténuer les risques de sécurité. L'instructeur insiste sur la nécessité d'officialiser les garanties de sécurité et de mettre en place des chaînes de compilation sécurisées pour appliquer efficacement les politiques de sécurité.

Source officielle

Concepts associés (32)

Démonstration (logique et mathématiques)

vignette| : un des plus vieux fragments des Éléments d'Euclide qui montre une démonstration mathématique. En mathématiques et en logique, une démonstration est un ensemble structuré d'étapes correctes de raisonnement. Dans une démonstration, chaque étape est soit un axiome (un fait acquis), soit l'application d'une règle qui permet d'affirmer qu'une proposition, la conclusion, est une conséquence logique d'une ou plusieurs autres propositions, les prémisses de la règle.

Raisonnement par récurrence

vignette|Le raisonnement par récurrence est comme une suite de dominos. Si la propriété est vraie au rang n0 (i. e. le premier domino de numéro 0 tombe) et si sa véracité au rang n implique celle au rang n + 1 (i. e. la chute du domino numéro n fait tomber le domino numéro n + 1) alors la propriété est vraie pour tout entier (i. e. tous les dominos tombent). En mathématiques, le raisonnement par récurrence (ou par induction, ou induction complète) est une forme de raisonnement visant à démontrer une propriété portant sur tous les entiers naturels.

Computer-assisted proof

A computer-assisted proof is a mathematical proof that has been at least partially generated by computer. Most computer-aided proofs to date have been implementations of large proofs-by-exhaustion of a mathematical theorem. The idea is to use a computer program to perform lengthy computations, and to provide a proof that the result of these computations implies the given theorem. In 1976, the four color theorem was the first major theorem to be verified using a computer program.

Proofs and Refutations

Proofs and Refutations: The Logic of Mathematical Discovery is a 1976 book by philosopher Imre Lakatos expounding his view of the progress of mathematics. The book is written as a series of Socratic dialogues involving a group of students who debate the proof of the Euler characteristic defined for the polyhedron. A central theme is that definitions are not carved in stone, but often have to be patched up in the light of later insights, in particular failed proofs. This gives mathematics a somewhat experimental flavour.

Théorie de la démonstration

La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du . Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au congrès international des mathématiciens en 1900 avec pour objectif de démontrer la cohérence des mathématiques.

Afficher plus

Séances de cours associées (64)

Preuves : Logique, Mathématiques et Algorithmes

Explore les concepts, les techniques et les applications de la preuve dans la logique, les mathématiques et les algorithmes.

Existence de mesures Gibbs

Explore la quasi-localité en mécanique statistique et les conditions d'existence des mesures de Gibbs.

Logique formelle: preuves et ensembles

Couvre les bases de la logique formelle, en se concentrant sur les expressions logiques et les preuves mathématiques.

Transport optimal : théorie et applications

Explore la théorie optimale des transports, les cartes de transport, l'entropie et leurs implications pratiques dans l'optimisation mathématique.

Raisonnement automatisé : vérification formelle avec LISA

Examine la vérification formelle à l'aide de l'assistant d'épreuve LISA et du vérificateur d'équivalence OCBSL.

Afficher plus

Concepts associés (32)

Démonstration (logique et mathématiques)

Raisonnement par récurrence

Computer-assisted proof

Proofs and Refutations

Théorie de la démonstration

Afficher plus