Retour au site du LAAS-CNRS

Abstract

In this paper, we define a type of mobility model that we coin as temporal Mobility Markov Chain (tMMC), which can represent in a compact yet precise way the mobility behaviour of an individual. In short, a tMMC is a timed and probabilistic automaton in which states represent points of interest (POIs) of an individual and transitions between states corresponds to a movement from one POI to another one. The automaton is probabilistic in the sense that a transition between POIs is non deterministic but rather that there is a probability distribution over the transitions that corresponds to the probability of moving from one POI to another (edges are directed).

Abstract

This paper presents a new algorithm aimed at the vulnerability assessment of web applications following a blackbox approach. The objective is to improve the detection efficiency of existing vulnerability scanners and to move a step forward toward the automation of this process. Our approach covers various types of vulnerabilities but this paper mainly focuses on SQL injections. The proposed algorithm is based on the automatic classification of the responses returned by the web servers using data clustering techniques and provides especially crafted inputs that lead to successful attacks when vulnerabilities are present. Experimental results on several vulnerable applications and comparative analysis with some existing tools confirm the effectiveness of our approach.

Résumé

Les travaux résumés dans ce mémoire ont pour cadre la sûreté de fonctionnement des systèmes informatiques. Ils portent sur l'élimination des fautes, en s'intéressant plus particulièrement au test du logiciel. Les contributions sont regroupées en quatre chapitres. Le premier chapitre rassemble des travaux pour adapter la conception du test aux technologies de développement logicielles. Deux technologies sont considérées : la technologie orientée-­‐objet et la méthode formelle B. Le deuxième chapitre porte sur des associations test et vérification formelle. Il s'agit selon les cas de consolider la vérification d'algorithmes partiellement prouvés, ou de faciliter l'analyse de contrexemples retournés par un model checker. Le troisième chapitre traite de la génération de test par des procédés métaheuristiques, en prenant l'exemple du recuit simulé. L'accent est mis sur l'utilisation de mesures pour guider le paramétrage de la métaheuristique. Enfin, le quatrième chapitre aborde le test de systèmes mobiles. Lestraces d'exécutions sont vérifiées par rapport à un ensemble de propriétés décrites par des scénarios graphiques, en combinant des algorithmes d'appariement de graphes et de calcul d'ordres partiels d'événements.

Abstract

The research summarized in this report focuses on the dependability of computer systems. It adresses fault removal by means of software testing. The contributions are grouped into four chapters. Chapter I presents work seeking to adapt the test design to software development technologies. It considers both object-­‐oriented development and the formal B method. Chapter II investigates ways of coupling testing and formal verification. The aim may be to consolidate the verification of partially proved algorithms, or to aid in the analysis of counterexamples obtained from a model checker. Chapter III concerns search-­‐based test generation, taking the example of simulated annealing search. It focuses on a measurement approach to tune the parameters of the metaheuristics. Finally, Chapter IV tackles testing of mobile computing systems. Test traces are checked with respect to properties described in graphical scenarios. The checking involves both graph matching and event order analysis.

Mots-Clés / Keywords

Test de logiciel; Vérification formelle; Procédés métaheuristiques; Systèmes mobiles; Fault removal; Software testing; Formal verification; search-based testing; Mobile computing systems; Elimination des fautes;

Abstract

Modern embedded systems for safety critical applications, found in planes or cars, are based on real-time distributed networks and require high level of robustness, reliability and adaptability. In order to complement static off-line validation of such systems, this paper introduces a novel approach for on-line verification of behavioral properties expressed as a sub-family of timed Petri nets. We show that, for the subclass of acyclic safe nets, whose expressivity matches real-time systems constraints, it is possible to define a commutative and associative operation on states that enables out-of-order evaluation of the state of the Petri net, and thus a fully distributed evaluation of the behavior of the system under supervision. Additionally, when provided with a mapping between events and nodes of the distributed system, we show how to efficiently distribute the monitoring system on top of the applicative system, and provide algorithms for local evaluation and merging of information in order to detect as soon as possible when the system deviates from its specification.