Journal Re-implémentation de TweetNaCl en Spark

Posté par  (site web personnel, Mastodon) . Licence CC By‑SA.
Étiquettes :
28
26
jan.
2022

A l'origine, ce n'était qu'un lien mais finalement, cela méritait un journal sur Spark.

Avant de vous filer le lien sur le portage, on va commencer par un petit exemple rapide de ce que peut faire Spark.

Mais c'est quoi Spark ?

Spark est, aujourd'hui, un sous-ensemble d'Ada restreignant les capacités aux fonctions sécurisées et non-abmigües.

Via un ensemble d'aspects, une sorte d'annotations, le compilateur gnatprove génère des conditions de vérification pour chaque sous-programme.
Ces conditions de vérification (…)

Journal La recherche en langages de programmation au quotidien

Posté par  . Licence CC By‑SA.
Étiquettes :
81
6
fév.
2018

Dans le cadre de mon travail j'ai été amené à écrire un petit texte qui explique mon quotidien fait de "recherche (scientifique) en langages de programmation". Je me permets de le diffuser ici au cas où ça intéresse des gens.

Ma recherche

Je travaille à l'INRIA, un institut public français de recherche en informatique. Je fais de la programmation et de la recherche sur les langages de programmation.

Mon rôle est d’étudier ces langages, de mieux les comprendre (…)

Sortie de Coq 8.5 bêta, un assistant de preuve formelle

Posté par  (site web personnel) . Édité par gasche, BAud, anaseto, ZeroHeure, Snark, Yves Bourguignon, palm123, reno, Nicolas Boulay, Nils Ratusznik et Ontologia. Modéré par Nÿco. Licence CC By‑SA.
Étiquettes :
98
28
jan.
2015
Science

L'assistant de preuve Coq, deux fois primé l'année dernière, vient de sortir en version 8.5 bêta. Attendue depuis plus d'un an déjà, on trouvera au menu de cette version un nombre certain de changements en profondeur.

Coq est un assistant de preuve sous licence LGPL 2.1, développé entre autres à l'INRIA. Issu des travaux sur la correspondance de Curry-Howard, Coq peut être vu aussi bien comme un langage de programmation que comme un système de preuves mathématiques. Il est, de fait, employé par les deux communautés. Parmi les développements en Coq, on peut citer par exemple le compilateur C certifié CompCert sur le versant informatique et la preuve du Théorème de Feit et Thompson sur le versant mathématique. Plus récemment, une des failles d'OpenSSL a été découverte grâce à Coq[0] . Il est aussi de plus en plus utilisé comme système interactif pour l'apprentissage de la logique dans l'enseignement supérieur.

On rappellera dans le reste de la dépêche les grands principes qui sous-tendent Coq, ce qu'il est, ce qu'il n'est pas, puis on détaillera les changements introduits dans cette version.

Journal Analyser la génération de nombre aléatoire du noyau

Posté par  . Licence CC By‑SA.
Étiquettes :
29
26
mar.
2013

Sommaire

Après avoir lu hier un journal décrivant une faille dans le code de génération des nombres aléatoires de NetBSD 6, j'ai décidé de regarder quelques méthodes visant à réduire le risque d'introduire ce genre de bug dans du code "critique".

Disclaimer : je suis novice dans le domaine de la sécurité et de la (…)

Journal Annonce : un blog sur une équipe de recherche en langages de programmation

Posté par  .
Étiquettes :
21
8
nov.
2012

Cette année j'ai lancé un blog (anglophone) en commun avec les autres membres de mon équipe de recherche, Gallium, qui travaille sur les langages de programmation et la preuve de programme. C'est aussi l'équipe qui a conçu et maintient le langage de programmation OCaml, donc une partie des articles concernent ce langage et son développement—au passage, c'est un logiciel libre dans l'écosystème duquel de nombreuses contributions sont possibles.

Voilà, on m'a signalé que ça pourrait intéresser des LinuxFRiens donc (…)