Méthodes de Test pour la Vérification  et la Validation (Test Methods for Verification and Validation)

The MTV2 group brings together all the French academic teams working on the general theme of validation and verification of software and systems, under the supervision of the GDR GPL funded by the CNRS.

The GDR GPL (Groupement de Recherche Génie de la Programming et du Logiciel) is a unit of the INS2I of the CNRS which brings together the French scientific community interested in Software Engineering and Programming.

The next meeting of the MTV2 workshop will take place on 17 October 2019 at Télécom ParisTech and will be a joint event with the IFIP-ICTSS conference.

Program

The duration of the keynote is 60-65 min + questions. The duration of a regular talk is 25 min + questions. All sessions this year will be in English.

Thursday, October 17 (ICTSS/MTV2 Joint Day)

9:00 Registration, Welcome Coffee

9:30 Session 9. Keynote

  • Mauro Pezzè. Testing Human-Centric Cyber-Physical Systems

10:45 Coffee Break

11:00 Session 10. Industrial presentations

  • Frédéric Rivière (MicroEJ). JUnit for Testing Constrained Embedded Systems
  • Fabrice Trollet (All4Tec). Platform for automated testing of distributed systems applied to case studies (Airbus, Thales and IoT)
  • Yves Génevaux (Argosim). Automating Functional Validation of Embedded Systems

12:30 Lunch

14:00 Session MTV2

  • Laurent Mounier (Verimag). Checking the robustness of a software against fault-injection
  • Michaël Marcozzi (Imperial College London). Compiler Fuzzing: How Much Does It Matter?
  • Frédéric Voisin and Marie-Claude Gaudel (LRI). Drawing uniformly at random in dynamic sets of paths.

15:30 Coffee Break

16:00 Session MTV2

  • Frédéric Recoules (CEA List). Get rid of inline assembly through verification-oriented lifting.
  • José Reyes (Telecom SudParis). Data-path Discovery Toolkit and its Usage for Testing and Verification of SDN Frameworks.

17:00-17:10 Closing remarks. End of the event.

Abstracts

The abstract of the keynote, shared with IFIP-ICTSS 2019, is available here.

Frédéric Voisin and Marie-Claude Gaudel (LRI). Drawing uniformly at random in dynamic sets of paths.

Random generation of combinatorial structures can be used for model-based automatic generation of tests or traces : previous works have reported on their successful application to randomised structural program testing or probabilistic exploration of very large models. In the case of structural program testing, random generation is used to first draw a set of paths in the control flow graph of the program. Then, some solver is used for trying to derive input values to traverse these paths during runs of the program: this process is incremental, collecting the conditions encountered when traversing the path and trying to solve their conjunction. A well-known problem is that not all paths of the control flow graph correspond to feasible runs. When such an unfeasible path is drawn, it is simply discarded and another path is drawn. This is a severe limitation in the case of programs with a high ratio of infeasible paths.

We show how to improve the method by using for the drawing the information about infeasible paths already drawn, more precisely the infeasible prefixes already detected. In addition to the counting table used by the recursive method for uniformly generating combinatorial structures, we introduce a trie structure that allows to exclude all paths with an already detected infeasible prefix. Our derived drawing algorithm is uniform among all paths that do not have a known infeasible prefix. Due to the fact that the number of extensions of infeasible prefixes may be (and is often) large, their elimination from the subsequent drawings is a substantial improvement w.r.t. the classical rejection method. Preliminary experiments are reported and commented.

Yves Génevaux (Argosim). Automating Functional Validation of Embedded Systems

Nowadays complex embedded systems require a level of testing higher than ever. However, when test cases are derived from functional requirements written in natural language, each and every functional test case must be created manually. Furthermore, the test objectives themselves, the requirements, could be erroneous as they have never been properly validated. We will present a very innovative approach yet supported by an industry-proven tool, STIMULUS, enabling to, first, capture and simulate the textual requirements, second,  generate numerous test vectors to stimulate the system under test and finally, allow the requirements to be used as Observers to detect any violation of the specification by the developed system.

Michaël Marcozzi (Imperial College London). Compiler Fuzzing: How Much Does It Matter?

Despite much recent interest in randomised testing (fuzzing) of compilers, the practical impact of fuzzer-found compiler bugs on real-world applications has barely been assessed. We present the first quantitative and qualitative study of the tangible impact of miscompilation bugs in a mature compiler. We follow a rigorous methodology where the bug impact over the compiled application is evaluated based on (1) whether the bug appears to trigger during compilation; (2) the extent to which generated assembly code changes syntactically due to triggering of the bug; and (3) whether such changes cause regression test suite failures, or whether we can manually find application inputs that trigger execution divergence due to such changes. The study is conducted with respect to the compilation of more than 10 million lines of C/C++ code from 309 Debian packages, using 12% of the historical and now fixed miscompilation bugs found by four state-of-the-art fuzzers in the Clang/LLVM compiler, as well as 18 bugs found by human users compiling real code or as a by-product of formal verification efforts. The results show that almost half of the fuzzer-found bugs propagate to the generated binaries for at least one package, in which case only a very small part of the binary is typically affected, yet causing two failures when running the test suites of all the impacted packages. User-reported and formal verification bugs do not exhibit a higher impact, with a lower rate of triggered bugs and one test failure. The manual analysis of a selection of the syntactic changes caused by some of our bugs (fuzzer-found and non fuzzer-found) in package assembly code, shows that either these changes have no semantic impact or that they would require very specific runtime circumstances to trigger execution divergence.

Laurent Mounier (Verimag). Checking the robustness of a software against fault-injection?

Fault injection is a powerful attack technique which consists in modifying at runtime the memory content (either the code or the data) of an execution platform. The attacker goal is usually to change a program behavior in order to break some security properties. Such attack are usually performed by physical means (e.g. laser rays, electro-magnetic fields) and typical targets are embedded systems like smart cards, or IoT devices. Protection mechanisms are based on hardware and/or software counter-measures. This talk presents a test-based approach those purpose is to check the robustness of a software against such fault injection attacks. It will describe a prototype tool, called Lazart and based on the symbolic execution engine Klee, which is able to produce multi-fault attacks according to several high-level fault models. This tool can be used by developers and code auditors to identify software weaknesses and to analyze the effectiveness of counter-measures.

Frédéric Recoules (CEA List). Get rid of inline assembly through verification-oriented lifting.

Formal methods for software development have made great strides in the last two decades, to the point that their application in safety-critical embedded software is an undeniable success. Their extension to non-critical software is one of the notable forthcoming challenges. For example, C programmers regularly use inline assembly for low-level optimizations and system primitives. This usually results in driving state-of-the-art formal analyzers developed for C ineffective. We thus propose TInA, an automated, generic, trustworthy and verification-oriented lifting technique turning inline assembly into semantically equivalent C code, in order to take advantage of existing C analyzers. Extensive experiments on real-world C code with inline assembly (including GMP and ffmpeg) show the feasibility and benefits of TInA.

José Reyes (Telecom SudParis). Data-path Discovery Toolkit and its Usage for Testing and Verification of SDN Frameworks.

In Software Defined Networking (SDN), different applications may configure different coexisting forwarding rules, the resulting (running) data-paths a specific network flow traverses may not be the intended ones. Furthermore, the SDN components may be defective or compromised. To provide reliable communication within the SDN driven data-planes, assuring that the running data-paths are the requested (and expected) ones is necessary. However, in order to test or verify such SDN frameworks, the running data-paths must be known. In this talk, a toolkit for discovering the running data-paths in an SDN framework will be presented. The toolkit relies on formal methods, and it can guarantee the discovery of data-paths of interest, differently from previously existing approaches. Furthermore, some directions on how using the data-path discovery (DPD)  toolkit can be used to test and verify that SDN frameworks will be also discussed.

Frédéric Rivière (MicroEJ). JUnit for Testing Constrained Embedded Systems

For those who are familiar to Java, JUnit is the most widely used framework since almost 2 decades. Although it has been originally designed for Java library unit testing on a PC, it can also be a good choice for more advanced testing on embedded systems especially because of its massive API adoption. In this session, we will show how JUnit has been integrated into MicroEJ, not only for the purpose of « unit » testing, but also for more complex integration testing, giving to the « Test Developer » a unique base framework whatever the kind of tests he is writing (unit tests, integration tests, field tests, production tests). The session will end up with a live demo of automatic testing on virtual devices and various embedded boards.

Fabrice Trollet (All4Tech). Platform for automated testing of distributed systems applied to case studies (Airbus, Thales and IoT)

Feedback on test techniques and methods from the DisTA (DIStributed Test Automation) platform deployed at Airbus, Thales and IoT system customers to validate end-to-end distributed communicating systems. This presentation will explain the complexity of automating distributed system tests, such as unsecured communications between systems, the difficulty of calculating a distributed test verdict, or the problem of synchronizing and orchestrating parallel tests on several systems, each with its own automation technology: heavy client HMI, Web, console, webservice, BDD, Embedded, MQTT…. The method for automating distributed systems will be explained, such as a model where the behaviour of systems with respect to their environment and other systems is drawn, or the generation of tests that adapt to the state of the systems, and automate stimuli and verifications as they occur and in real time, and finally the specific algorithms for oracle and verdicts calculations.