Génération de code sécurisé avec des protections formellement prouvées – PROSECCO

Les composants sécurisés sont des éléments clef dans les systèmes de paiement, de protection des contenus, de transports, de téléphonie mobile et de par les secrets qu'ils contiennent, doivent être protégés contre des manipulations frauduleuses appelées « attaques physiques ». Actuellement les protections logicielles sont en grande partie ajoutées manuellement, nécessitant expertise et temps. L'industrie est en demande de solutions de protection automatisées afin de réduire les coûts de développement et de maintenance, ainsi que le temps de mise sur le marché. Le consortium de PROSECCO propose de créer une rupture technologique: protéger l'application par l'insertion automatique de protections dans le flot de compilation, et prouver leur bonne intégration par vérification formelle (i.e. vérification de l'équivalence fonctionnelle de l'application par rapport à une version non sécurisée et vérification de propriétés sécuritaires).