CEA and Thales announce major breakthrough in cybersecurity protection for cryptographic code
Thales and CEA have unveiled a completely new solution developed by their joint research unit, FormalLab, to guarantee the security of cryptographic code. The innovation lies in the formal verification[1] of secure library components for the encryption of sensitive communications, and represents a real technological breakthrough in the field of cybersecurity.
Cybersecurity, or IT security, is one of the key challenges of the digital society, and calls for an effective combination of design, verification and certification. CEA LIST, one of CEA Tech’s technological research institutes, has been working on the analysis and formal verification of software systems for many years and has considerable expertise in this field. Its innovative technologies have applications in energy and aerospace and, more recently, in the automotive and naval industries.
FormalLab: the power of formal methods
Thales and CEA set up the FormalLab joint research unit in June 2015 with the objective of using formal approaches to address the challenges of digital trust. Using advanced mathematical techniques, formal solutions are considered a promising alternative to conventional test type verification, which, by definition, can contain flaws. While formal solutions require expertise in specification and analysis techniques, they provide solid assurances that the software program will behave as expected. In particular, they can demonstrate that a program is free from certain classes of security vulnerabilities and thus immune to many types of cyberattacks.
Formal code analysis for cybersecurity
Encryption software is a fundamental part of digital communications and data protection today. A flaw in any of these applications can leave the system open to cyberattack, with potentially major repercussions. For example, when the Heartbleed bug was publicly disclosed in 2014, some 17% of the Internet’s secure servers were believed to be vulnerable to attack. The Thales and CEA teams have been working on the issue of cybersecurity for encrypted communication code. Using the Frama-C[2] code analysis platform, they have produced a set of security specifications and formally validated the compliance of communication code with these requirements.
In today’s world of cloud computing and increasingly interconnected information systems, including the most critical systems in the defence sector, perimeter based approaches to cybersecurity are no longer sufficient. Data security is not the same thing as network security. At Thales, we believe that the future lies in natively secure solutions, with cybersecurity built into every level — the overall architecture, the network and, importantly, the software, especially the application modules used for communications and data encryption. In this field, FormalLab is breaking with conventional cybersecurity practices to better defend against constantly changing cyberthreats.
Said Marko Erman, Chief Technical Officer of Thales.
The issue of digital trust, and cybersecurity in particular, is a central focus of our research programmes at LIST. We are developing a new breed of software security tools, drawing on the advanced mathematics expertise of the Paris-Saclay research cluster and a wealth of experience that is recognised around the world. At the FormalLab, we are working closely with Thales engineers to identify exactly what industry needs, determine where the added value lies and pursue the process of innovation, from solving fundamental problems to transferring technologies to operating units. In this way, CEA is helping drive some of the key technological advances in the French cybersecurity ecosystem today.
Said Philippe Watteau, Director of LIST.
[1] Formal verification uses mathematical techniques to demonstrate that a system complies with a predefined set of specifications or properties.
[2] www.frama-c.com
Frama-C: Framework for Modular Analysis of C programs
The French Atomic Energy and Alternative Energies Commission (CEA) is a public-sector research body active in four main fields: defence and security, low-carbon energies (nuclear and renewables), technology research for industry and fundamental research. Drawing on widely recognised expertise, CEA is involved in setting up collaborative projects with many academic and industrial partners. With its 16,000 researchers and other employees, CEA is a major player in the European research community and has a growing involvement at international level. Learn more: www.cea.fr
CEA LIST, one of CEA Tech’s technological research institutes, pursues research into smart digital systems. Major economic and social drivers, its R&D programmes are focused on advanced manufacturing, cyber-physical systems, data intelligence and technologies for the digital patient. By developing cutting-edge technologies, LIST helps its industrial partners enhance their competitiveness through innovation and technology transfer. In recognition of the quality of its partnership-based research, CEA LIST was awarded an Institut Carnot certificate of excellence in 2006. Learn more: www-list.cea.fr
About Thales
Thales is a global technology leader for the Aerospace, Transport, Defence and Security markets. With 64,000 employees in 56 countries, Thales reported sales of €14.9 billion in 2016. With over 25,000 engineers and researchers, Thales has a unique capability to design and deploy equipment, systems and services to meet the most complex security requirements. Its unique international footprint allows it to work closely with its customers all over the world.
Research-driven innovation is an integral part of Thales’s identity. In 2016, Thales devoted €743 million to self-funded R&D. At Thales, innovation translates into a portfolio of 16,500 patents, R&D centres in 19 countries, 20 joint laboratories with partner research institutes around the world and 50 cooperation agreements with universities and public research bodies in Europe, the United States and Asia.