Fast and effective verification techniques are crucial to ensuring the cybersecurity of embedded and ground software used for critical operations in the aeronautics industry. Dassault Aviation recently used several tools in List's Frama-C suite to develop a new method for analyzing the source code of its software.

The new method automatically combines the static EVA and dynamic E-ASCL analyses in the Frama-C suite to detect common weaknesses and, if necessary, trigger countermeasures during software execution. List made improvements to the E-ASCL component, which can now detect more vulnerabilities than competing solutions at similar execution speeds while using less memory.

Once validation testing had been completed, the combined method was tested on two widely-used information system security components—Apache and Open SSL—used in this case by Dassault Aviation in proof-of-concept testing of an experimental ground support application for the company's Falcon jets. The tests confirmed that the improved Frama-C features enable the identification of families of cybersecurity weaknesses and make the applications being analyzed more robust while delivering the performance required for industrial scale-up.