formally PROven protections for SEcured Compiled COde – PROSECCO

Secure elements are essential building blocks in information systems used in payment, content protection, transportation, mobile and identification industries. They have to be strongly protected against a wide class of malicious and very effective manipulations, called “attacks”. Protections are still manually added to applications, requiring expert efforts, time and money. The software industry looks for automated solutions that could reduce development costs, software maintenance, expertise and know-how in security, and time to market. The consortium of PROSECCO plans to create a technological breakthrough by developing tools that will automatically insert protections in the compilation flow and formally prove the functional equivalence and the robustness of the protected software.