Q&A WITH BRUNO STOUFFLET,
CTO of Dassault Aviation, in charge of Innovation; supervising R&T activities
© DASSAULT AVIATION
Mr. Soufflet, could you please remind us what Dassault Aviation is and does ?
“Dassault Aviation is a French aerospace company, with over 10,000 aircraft delivered to 90 countries, several offices and plant in the US, and with dual expertise as a manufacturer of both military aircraft (Rafale, nEUROn demonstrator) and business jets (Falcon family). In France and abroad, the company conducts coordinated scientific, technological and industrial actions with partnerships, where innovation is one of the master-keys for success.”
What are Dassault Aviation Safety and Security needs and duties?
“On the one hand, ensuring aircraft safety is obviously mandatory. This is framed by Airworthiness Authorities’ standards. For the related verification activities, static analysis technologies may mathematically help developers consolidate the code behaviors, looking for runtime errors, and in some cases more functional sought properties.
On the other hand, with emerging services provided through the Internet and their related threats, from aircraft supply chain to maintenance and industrial systems, CyberSecurity must be taken into account in early design steps. Verifying source code by static analysis, in complement to or collaboration with traditional dynamic analyses, is one of the promising means to build even more trustworthy applications. It is expected to increase confidence and resilience, and reduce total development cost by lowering the rework, during further development phases.
Our teams participated in founding research projects, co-funded initiatives in static analysis, in order to address both safety and security verification goals (beyond quality control objectives), which led to the development of Frama-C tool and more recently, to the TrustInSoft tool and service offers.”
 An academic platform for collaborating static analyzers.
What benefits do you get from formal static analysis?
“Formal methods provide developers with sound techniques when verifying code: for every – even potential – faulty statement, an alarm will be duly raised. These methods take into account the whole interval of possible values, exhaustively, for each input parameter, which is a clear cut compared to classic testing activities based on sampling. However, this can also lead to non-conclusive over-approximations and spurious alarms in some cases. Thus, these approaches will be valuable as long as these spurious cases are not too numerous.
To understand the capacities of these methods and guide if needed further developments, we manage to have experts in the company able to discuss with TrustInSoft teams.
In this regard, TrustInSoft tooling approach is deemed of real interest for our verification activities. TiS founders have an expertise in nuclear and aeronautics application formal verification, and now in CyberSecurity. They designed the TrustInSoft Analyzer tool in such a way to ease the preliminary analysis steps, helping developers detect potential safety and security holes on nx10K to nx100K LoC software. Thanks to a user interface focused on most critical locations, rather than on analysis artefacts, formal analysis results interpretation and diagnostic are given more optimal for verifiers. At least, it helps developers sort and carry out further specific investigations, which is highly beneficial.”
What long-term outlooks would be?
“Briefly said, Airworthiness Authorities already acknowledged formal methods in standards. However, obtaining certification credits relies on tool qualification, which requires adapting the process and induces some extra-costs. Regarding CyberSecurity, certification bodies’ agreement on formal tool usage for verification is also mandatory. Benefits expected from formal analysis are clearly identified for this purpose. It remains to point out which security evaluation requirements can be duly fulfilled by formal analysis. A consensus must be found by authorities, tool providers, and industrial users on that point.”
 The ability to replace usual testing and code review, by other (e.g. formal) verification means.