For the first time ever in the world of cybersecurity, the operating code of software used to encrypt sensitive data was analyzed using formal verification tools developed at List. The advance addresses a vast potential market: Encrypted communications software is currently used for the majority of digital communications, and vulnerabilities in the software can potentially compromise the security of large amounts of data.

In research conducted under the Thales-List joint R&D lab FormalLab, List applied its code analysis and verification know-how to Thales' encryption software.

The partners began by stating the software's security requirements in everyday language. They then drew up specifications for the features of the target software. The specifications were compared with the existing software code using advanced mathematical reasoning.

List researchers worked closely with developers at Thales on the project, which provided List with an opportunity to implement its Frama-C software on a real-world case. Thales is now rolling out the use of Frama-C on a test basis with the ultimate goal of using it on all of its encryption software code, thus eliminating security vulnerabilities. In other research, FormalLab continues its work to develop future generations of code analysis software.