EN

RESEARCH

Research

Research notes and published papers from Ironproof. Every figure traces to a cited source, and each note states what it does not show.

PUBLISHED PAPERS · ARXIV

RESEARCH NOTES

ÉTAT DU MOTEUR

Ce qui fonctionne aujourd’hui. Ce qui est en cours. Ce qui reste ouvert.

Les trois états que nous donnons à chaque résultat, appliqués à nous-mêmes. Chaque ligne dit comment la vérifier.

État au

FONCTIONNE AUJOURD’HUI

  • Traduction de code, vérifiée par preuve

    Un module Python de quatre fonctions avec boucles, traduit en Rust. L’équivalence est prouvée pour toute série d’au plus six valeurs, et les boucles sont prouvées pour n’importe quel calcul à chaque pas. Au-delà de six valeurs, 100 000 essais au hasard n’ont trouvé aucune différence. Les fichiers du test sont disponibles sur demande pour un examen.

  • MISRA C sur du code traduit

    La traduction C d’une fonction de traitement de signal passe le vérificateur libre MISRA C:2012 (cppcheck) sur le programme complet, et son équivalence avec l’original Python est reprouvée. C’est un outil libre qui couvre une partie des règles, pas une certification.

  • Autorisation des actions critiques

    Chaque demande qui passe par Ironproof est vérifiée contre vos règles avant de s’exécuter. Permise, elle s’exécute. Interdite, elle ne s’exécute jamais. Dans les deux cas, la décision est scellée. Ouvrez une décision scellée et vérifiez-la vous-même, dans votre navigateur, sans serveur ni compte.

    VÉRIFIER UNE TRACE SCELLÉE

  • Essayez de passer la barrière

    Quatre attaques contre la politique de paiement scellée de l’exemple, calculées dans votre navigateur. Certaines passent, et la page dit exactement pourquoi.

    OUVRIR LE LABO

EN COURS

  • Modernisation des systèmes hérités

    Les programmes d’assurance GenApp d’IBM, vérifiés sous un modèle CICS que nous écrivons nous-mêmes et confrontés à un vrai CICS. Une exécution sur z/OS et une reprise par un tiers restent à faire. Les réponses « même comportement » de notre vérificateur de traductions sont suspendues : des audits ont reproduit des dizaines de fausses réponses, sur des cas écrits pour attaquer l’outil.

    LIRE LA RECHERCHE

  • Sécurité du logiciel C

    Vérifier qu’un correctif de sécurité ferme vraiment la faille, sur de vrais correctifs de projets open source. Le vérificateur est en reconstruction ; les résultats antérieurs ne sont pas présentés comme des preuves complètes.

    LIRE LA RECHERCHE

  • Correctif de sécurité en Rust

    Une faille publiée d’une librairie Rust (RUSTSEC-2017-0004). Le code d’origine et un faux correctif plausible sont tous deux attrapés. Le vrai correctif est prouvé sur le code réel pour les longueurs de ligne standard, et pour toute longueur sur un modèle écrit à la main, dont le lien avec le code n’est pas encore vérifié par une machine.

PROBLÈMES OUVERTS

  • La fidélité

    Montrer que la logique que nous vérifions dit la même chose que la politique, le code ou le programme d’origine. Une preuve ne vaut pas plus que cette étape.

  • Les correctifs écrits par des modèles de langage

    Prouver qu’un correctif C proposé par un modèle ferme la faille, pas seulement qu’il passe les tests.

  • Le COBOL qui lit de vraies données

    L’équivalence pour toutes les entrées qu’un programme peut recevoir, pas pour une seule exécution.

Vous travaillez sur l’un de ces problèmes ? Nous voulons les attaquer avec des chercheurs universitaires. ÉCRIVEZ-NOUS