Model-based mutation testing from security protocols in HLPSL - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Article Dans Une Revue Journal of Software Testing, Verification and Reliability Année : 2015

Model-based mutation testing from security protocols in HLPSL

Résumé

In recent years, important efforts have been made for offering a dedicated language for modelling and verifying security protocols. Outcome of the European project AVISPA, the high-level security protocol language (HLPSL) aims at providing a means for verifying usual security properties (such as data secrecy) in message exchanges between agents. However, verifying the security protocol model does not guarantee that the actual implementation of the protocol will fulfil these properties. This article presents a model-based testing approach, relying on the mutation of HLPSL models to generate abstract test cases. The proposed mutations aim at introducing leaks in the security protocols and represent real-world implementation errors. The mutated models are then analysed by the automated validation of Internet security protocols and applications tool set, which produces, when the mutant protocol is declared unsafe, counterexample traces exploiting the security flaws and, thus, providing test cases. A dedicated framework is then used to concretize the abstract attack traces, bridging the gap between the formal model level and the implementation level. This model-based testing technique has been experimented on a wide range of security protocols, in order to evaluate the mutation operators. This process has also been fully tool-supported, from the mutation of the HLPSL model to the concretization of the abstract test cases into test scripts. It has been applied to a realistic case study of the Paypal payment protocol, which made it possible to discover a vulnerability in an implementation of an e-commerce framework.

Dates et versions

hal-01090881 , version 1 (04-12-2014)

Identifiants

Citer

Frédéric Dadeau, Pierre-Cyrille Héam, Rafik Kheddam, Ghazi Maatoug, Michaël Rusinowitch. Model-based mutation testing from security protocols in HLPSL. Journal of Software Testing, Verification and Reliability, 2015, pp.30. ⟨10.1002/stvr.1531⟩. ⟨hal-01090881⟩
278 Consultations
0 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More