en visioconférence
Durée d'exposé: 20 min + 5 min. questions-réponses + 5 min. transition
Les exposés seront donnés en français (ou, si le conférencier le préfère, en anglais)
13:45 Accueil MTV2 2020 - Nikolai Kosmatov, Natalia Kushik, Pascale Le Gall, Antoine Rollet
14:00 Monitoring at the Bytecode Level with BISM - Chukri Soueidi - Inria
14:30 Attack tolerance techniques for Web-based services - Fatiha Zaïdi - LRI
15:00 Fast, Automatic, and Nearly Complete Structural Unit-Test Generation Combining Genetic Algorithms and Formal Methods - David Mentré - MERCE
15:30-16:00 Pause café et tour de table
16:00 On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators - Erick Petersen - ADS\SAMOVAR
16:30 Revisiting Semantics of Interactions for Trace Validity Analysis - Erwan Mahe - CentraleSupélec
17:00-17h10 Annonces, discussions, fin de journée - Nikolai Kosmatov, Natalia Kushik, Pascale Le Gall, Antoine Rollet
Monitoring at the Bytecode Level with BISM (Chukri Soueidi - Inria)
Instrumentation is essential in software monitoring, allowing the extraction of information from a running system and abstracting it into a trace of events fed into a monitor checking a desired behavior. Depending on the property monitored, the extracted information's granularity level may range from coarse (e.g., a method call) to fine (e.g., an assignment to a local variable, a jump in the control flow). An important aspect of instrumentation is expressiveness, which refers to how much information we can extract from the bytecode and how much we can alter its underlying execution. In addition to enabling the extraction of low-level events at the bytecode level, high expressive instrumentation enables runtime enforcement by responding to unexpected behavior and modifying the system execution.
BISM (Bytecode-level Instrumentation for Software Monitoring) is a lightweight Java bytecode instrumentation tool that features an expressive high-level control-flow-aware instrumentation language. BISM language follows the aspect-oriented programming paradigm by adopting the joinpoint model capturing various levels of execution, advice inlining, and separate instrumentation mechanisms. It provides out-of-the-box control-flow information to developers and access to comprehensive static and dynamic context information. BISM also allows inserting arbitrary byte-code instructions in the program to modify a program behavior.
We demonstrate BISM and show how effective it is in the context of classical runtime verification. We also demonstrate how BISM can be utilized in low-level and security scenarios detecting and enforcing control-flow integrity in programs.
Attack tolerance techniques for Web-based services - (Fatiha Zaïdi - LRI)
Although research on formalization and verification has improved trust in Web services, issues such as high availability and security are not fully addressed since the solutions proposed are sometimes attack-specific. In addition, Web services deployed in cloud infrastructures inherit their vulnerabilities. In this presentation, we propose a new formal monitoring methodology that takes into account the risks that our services may face. To implement this methodology, we propose a method based on software reflection to detect insider attacks. While the program is running, we analyze the methods to detect malicious executions. When these malicious activities are detected, using reflection again, as a countermeasures we change the attacked methods. Finally, we illustrate the application of our methodology to cloud applications deployed as a choreography.
Fast, Automatic, and Nearly Complete Structural Unit Test Generation Combining Genetic Algorithms and Formal Methods (David Mentré - MERCE )
Software testing is a time consuming and error prone activity, mostly manual in most industries. One approach to increase productivity is to automatically generate tests. In this paper, we focus on automatic generation of structural unit tests of safety-critical embedded software. Our purpose is to make a tool that integrates seamlessly with existing test processes in industry. We use genetic algorithms and automatic stub generation to quickly and automatically produce test cases satisfying test objectives of a given coverage criteria, using only the software under test as input. Moreover, we combine those genetic algorithms with formal methods to determine unfeasible test objectives and help on the coverage of difficult test objectives. We implemented our approach in a tool and tested it on a real-world industrial project, demonstrating that our approach can reliably generate test cases when feasible or demonstrate they are unfeasible for 99% of the MC/DC test objectives in about half an hour for 82,000 lines of C code with integer data.
On using SMT-solvers for Modeling and Verifying Dynamic Network Emulators (Erick Petersen - ADS\SAMOVAR)
A novel model-based approach to verify dynamic networks is proposed. The network topology and dynamic link parameters are described as a many sorted first order logic formula, that is verified by an SMT-solver (z3 in our case) with respect to a set of properties. The formula is also used for run-time network verification when a given static network instance is implemented. Preliminary experiments showcase the expressiveness and current limitations of the proposed approach.
Revisiting Semantics of Interactions for Trace Validity Analysis (Erwan Mahe - CentraleSupélec)
Interaction languages such as MSC are often associated with formal semantics by means of translations into distinct behavioral formalisms such as automatas or Petri nets. In contrast to translational approaches we propose an operational approach. Its principle is to identify which elementary communication actions can be immediately executed, and then to compute, for every such action, a new interaction representing the possible continuations to its execution. We also define an algorithm for checking the validity of execution traces (i.e. whether or not they belong to an interaction's semantics). Algorithms for semantic computation and trace validity are analyzed by means of experiments.