Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
International Journal on Software Tools for Technology Transfer
Erschienen in: International Journal on Software Tools for Technology Transfer 4/2019

28.02.2018 | Regular Paper

Complementary test selection criteria for model-based testing of security components

verfasst von: Julien Botella, Jean-François Capuron, Frédéric Dadeau, Elizabeta Fourneret, Bruno Legeard, Florence Schadle

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 4/2019

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

This article presents a successful industrial application of a model-based testing approach to the validation of security components. We present a smart combination of three test selection criteria applied to testing security requirements of components such as Hardware Security Modules. This combination relies on the use of static test selection criteria, namely structural model coverage, complemented by dynamic test selection criteria, based on abstract test scenarios or temporal properties, designed to target corner cases of security functional requirements. Our approach is implemented in an industrial and scalable MBT tool. We evaluated and successfully applied it on three real-world security components. The outcome of these experiences showed that the three test selection criteria target distinct kinds of errors in the software and are able to reveal inconsistencies in the specification. Moreover, a 5-year experience of working with both manufacturers and evaluators of security components, along with other industrial collaborations, showed that the approach is easy to adopt in the industry and the time spent to learn the methodology is negligible with respect to its benefits. Finally, the approach can be completely applied in a more general context on systems that underlay thorough validation of compliance to specifications or audits.
Vorheriger Artikel Parallel reachability analysis of hybrid systems in XSpeed
Nächster Artikel Comparing approaches for model-checking strategies under imperfect information and fairness constraints

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Fußnoten
2
TRL levels are commonly used for evaluation of software in many research projects. TRL 6: Representative model or prototype system, which is well beyond that of TRL 5, is tested in a relevant environment. Represents a major step up in software demonstrated readiness. Examples include testing a prototype in a live/virtual experiment or in a simulated operational environment. Algorithms run on processor of the operational environment are integrated with actual external entities.
 
3
A test target is said to be reachable if the test generator is able to compute a sequence of operation calls in the model state space to reach it.
 
4
2009–2012, funded by the French National Research Agency (ANR).
 
Literatur
1.
Common criteria for information technology security evaluation, version 3.1, July (2009)
2.
RSA Laboratories. Pkcs#11 specification (2004)
3.
Global Platform Consortium. Global platform uicc configuration version 1.0, October (2008)
4.
Cortier, V., Delaune, S., Lafourcade, P.: A survey of algebraic properties used in cryptographic protocols. J. Comput. Secur. 14(1), 1–43 (2006)CrossRef
5.
Dadeau, F., Héam, P.-C., Kheddam, R., Maatoug, G., Rusinowitch, M.: Model-based mutation testing from security protocols in HLPSL. Softw. Test. Verif. Reliab. 25, 684–711 (2014)CrossRef
6.
Wimmel, G., Jürjens, J.: Specification-based test generation for security-critical systems using mutations. In: ICFEM ’02: Proceedings of the 4th International Conference on Formal Engineering Methods, pages 471–482, London, UK. Springer (2002)
7.
Lazar, D., Chen, H., Wang, X., Zeldovich, N.: Why does cryptographic software fail?: A case study and open problems. In: Proceedings of 5th Asia-Pacific Workshop on Systems, APSys ’14, New York, NY, USA, pp. 7:1–7:7. ACM (2014)
8.
Hemmati, H.: How effective are code coverage criteria? An empirical analysis of 274 faults. In: Proceedings of the IEEE International Conference on Software Quality Reliability and Security (2015)
9.
Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and fixing pkcs#11 security tokens. In: Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS ’10, pp. 260–269. ACM, New York (2010)
10.
Beizer, B.: Black-Box Testing: Techniques for Functional Testing of Software and Systems. Wiley, New York (1995)
11.
Utting, M., Legeard, B.: Practical Model-Based Testing—a Tools Approach, p. 550. Elsevier Science, Amsterdam (2006)
12.
Bernabeu, G., Jaffuel, E., Legeard, B., Peureux, F.: MBT for global platform compliance testing: experience report and lessons learned. In: 25th IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops, Naples, Italy, 3–6 November 2014, pp. 66–70 (2014)
13.
Masson, P.-A., Potet, M.-L., Julliand, J., Tissot, R., Debois, G., Legeard, B., Chetali, B., Bouquet, F., Jaffuel, E., Van Aertrick, L., Andronick, J., Haddad, A.: An access control model based testing approach for smart card applications: results of the POSÉ project. JIAS J. Inf. Assur. Secur. 5(1), 335–351 (2010)
14.
Botella, J., Bouquet, F., Capuron, J.-F., Lebeau, F., Legeard, B., Schadle, F.: Model-based testing of cryptographic components—lessons learned from experience. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation, Luxembourg, Luxembourg, 18–22 March 2013, pp. 192–201 (2013)
15.
Castillos, K. Cabrera, Dadeau, F., Julliand, J.: Coverage criteria for model-based testing using property patterns. In: Proceedings Ninth Workshop on Model-Based Testing, MBT 2014, Grenoble, France, 6 April 2014, pp. 29–43 (2014)
16.
International Software Testing Qualifications Board. Standard glossary of terms used in software testing, March (2015)
17.
Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. 22(5), 297–312 (2012)CrossRef
18.
Graettinger, C.P., Garcia, S., Siviy, J., Schenk, R.J., VanSyckle, P.J.: Using the technology readiness levels scale to support technology management in the DoDs ATD/STO environments. Technical Report CMU/SEI-2002-SR-027, Carnegie Mellon University and Software Engineering Institute, September (2002)
19.
Bouquet, F., Grandpierre, C., Legeard, B., Peureux, F., Vacelet, N., Utting, M.: A subset of precise UML for model-based testing. In: 3rd International Workshop on Advances in Model Based Testing, pp. 95–104 (2007)
20.
Julliand, J., Masson, P.-A., Tissot, R., Bué, P.-C.: Generating tests from B specifications and dynamic selection criteria. FAC Form. Asp. Comput. 23, 3–19 (2011)CrossRefMATH
21.
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering, ICSE ’99, New York, NY, USA, pp. 411–420. ACM (1999)
22.
Anisetti, M., Ardagna, C.A., Damiani, E., Saonara, F.: A test-based security certification scheme for web services. ACM Trans. Web 7(2), 5:1–5:41 (2013)CrossRef
23.
Bernet, J.: Tasccc project: deliverable 5.5—report on the industrial use of the tasccc process. Technical report, Gemalto (2012)
24.
Rouillard, D.: Tasccc project—deliverable 5.4—report on the integration of the ate requirements. Technical report, Serma Technologies (2012)
25.
Tian-yang, G., Yin-sheng, S., You-yuan, F.: Research on software security testing. World Acad. Sci. Eng. Technol. 70, 647–651 (2010)
26.
Felderer, M., Zech, P., Breu, R., Bchler, M., Pretschner, A.: Model-based security testing: a taxonomy and systematic classification. Softw. Test. Verif. Reliab. 26, 119–148 (2015)CrossRef
27.
Le Traon, Y., Mouelhi, T., Pretschner, A., Baudry, B.: Test-driven assessment of access control in legacy applications. In: 2008 1st International Conference on Software Testing, Verification, and Validation, pp. 238–247 (2008)
28.
Mouelhi, T., Fleurey, F., Baudry, B., Traon, Y.: A model-based framework for security policy specification, deployment and testing. In: Proceedings of the 11th International Conference on Model Driven Engineering Languages and Systems, MoDELS ’08, pp. 537–552. Springer, Berlin (2008)
29.
Pretschner, A., Mouelhi, T., le Traon, Y.: Model-based tests for access control policies. In: 2008 1st International Conference on Software Testing, Verification, and Validation, pp. 338–347 (2008)
30.
Xu, D., Thomas, L., Kent, M., Mouelhi, T., Le Traon, Y.: A model-based approach to automated testing of access control policies. In: Proceedings of the 17th ACM Symposium on Access Control Models and Technologies, SACMAT ’12, New York, NY, USA, pp. 209–218. ACM (2012)
31.
Anisetti, M., Ardagna, C.A., Bezzi, M., Damiani, E., Sabetta, A.: Machine-readable privacy certificates for services. In: Meersman, R., Panetto, H., Dillon, T., Eder, J., Bellahsene, Z., Ritter, N., De Leenheer, P., Dou, D. (eds.) On the Move to Meaningful Internet Systems: OTM 2013 Conferences. Lecture Notes in Computer Science, vol. 8185, pp. 434–450. Springer, Berlin (2013)
32.
Mallouli, W., Lallali, M., Mammar, A., Morales, G., Cavalli, A.: Modeling and testing secureweb applications. In: Web-Based Information Technologies and Distributed Systems, volume 2 of Atlantis Ambient and Pervasive Intelligence, pp. 207–255. Atlantis Press (2010)
33.
Rosenzweig, D., Runje, D., Schulte, W.: Model based testing of cryptographic protocols. In: De Nicola R., Sangiorgi D. (eds.) Trustworthy Global Computing, volume 3705 of Lecture Notes in Computer Science, pp. 33–60. Springer, Berlin (2005)
34.
Schneider, M., Grossmann, J., Schieferdecker, I., Pietschker, A.: Online model-based behavioral fuzzing. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops, pp. 469–475 (2013)
35.
Johansson, W., Svensson, M., Larson, U.E., Almgren, M., Gulisano, V.: T-fuzz: model-based fuzzing for robustness testing of telecommunication protocols. In: 2014 IEEE Seventh International Conference on Software Testing, Verification and Validation, pp. 323–332 (2014)
36.
Jürjens, J., Wimmel, G.: Formally testing fail-safety of electronic purse protocols. In: Proceedings 16th Annual International Conference on Automated Software Engineering (ASE 2001), pp. 408–411 (2001)
37.
Slotosch, O., Molterer, S., Sihling, M., Rausch, A., Schtz, B., Huber, F.: Tool supported specification and simulation of distributed systems. In: International Symposium on Software Engineering for Parallel and Distributed Systems, p. 155 (1998)
38.
Botella, J., Legeard, B., Peureux, F., Vernotte, A.: Risk-based vulnerability testing using security test patterns. In: Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications—6th International Symposium, ISoLA 2014, Imperial, Corfu, Greece, 8–11 October 2014, Proceedings, Part II, pp. 337–352 (2014)
39.
Gargantini, A., Heitmeyer, C.: Using model checking to generate tests from requirements specifications. In: Proceedings of the Joint 7th European Software Engineering Conference and 7th ACM SIGSOFT International Symposium on Foundations of Software Engineering (1999)
40.
Tan, L., Sokolsky, O., Lee, I.: Specification-based testing with linear temporal logic. In: IRI’2004, IEEE International Conference on Information Reuse and Integration, pp. 413–498 (2004)
41.
Amman, P., Ding, W., Xu, D.: Using a model checker to test safety properties. In: 7th International Conference on Engineering of Complex Computer Systems (ICECCS’01), p. 212. IEEE (2001)
42.
Fraser, G., Wotawa, F.: Using model-checkers to generate and analyze property relevant test-cases. Softw. Qual. J. 16, 161–183 (2008)CrossRef
43.
Falcone, Y., Mounier, L., Fernandez, J.-C., Richier, J.-L.: j-POST: a Java Toolchain for property-oriented software testing. Electron. Notes Theor. Comput. Sci. 220(1), 29–41 (2008)CrossRef
44.
Rusu, V., Marchand, H., Jéron, T.: Automatic verification and conformance testing for validating safety properties of reactive systems. In: Fitzgerald J., Tarlecki A., Hayes I. (eds.) Formal Methods 2005 (FM05), LNCS. Springer (2005)
45.
Felderer, M., Agreiter, B., Zech, P., Breu, R.: A classification for model-based security testing. In: Proceedings of the 3rd International Conference on Advances in System Testing and Validation Lifecycle(VALID 2011), pp. 109–114 (2011)
46.
Jard, C., Jéron, T.: Tgv: theory, principles and algorithms: a tool for the automatic synthesis of conformance test cases for non-deterministic reactive systems. Int. J. Softw. Tools Technol. Transf. 7(4), 297–315 (2005)CrossRef
47.
Clarke, D., Jéron, T., Rusu, V., Zinovieva, E.: STG: a tool for generating symbolic test programs and oracles from operational specifications. In: ESEC/FSE-9: Proceedings of the 8th European Software Engineering Conference, pp. 301–302. ACM, New York (2001)
48.
Tretmans, G. J., Brinksma, H.: TorX: automated model-based testing. In: First European Conference on Model-Driven Software Engineering, Nuremberg, Germany, pp. 31–43 (2003)
49.
Bigot, C., Faivre, A., Gallois, J.-P., Lapitre, A., Lugato, D., Pierron, J.-Y., Rapin, N.: Automatic test generation with AGATHA. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003, Tools and Algorithms for the Construction and Analysis of Systems, 9th International Conference. LNCS, vol. 2619, pp. 591–596. Springer (2003)
50.
Basili, V.R., Rombach, H.D.: Support for comprehensive reuse. Softw. Eng. J. 6(5), 303–316 (1991)CrossRef
51.
Vegas, S., Basili, V.: A characterisation schema for software testing techniques. Empir. Softw. Eng. 10(4), 437–466 (2005)CrossRef
52.
Dias-Neto, A.C., Travassos, G.Horta: Supporting the combined selection of model-based testing techniques. IEEE Trans. Softw. Eng. 40(10), 1025–1041 (2014)CrossRef
53.
Wojcicki, M.A., Strooper, P.: An iterative empirical strategy for the systematic selection of a combination of verification and validation technologies. In: Software Quality, 2007. WoSQ’07: ICSE Workshops 2007. Fifth International Workshop on, p. 9 (2007)
54.
Victor, M., Upadhyay, N.: Selection of software testing technique: a multi criteria decision making approach. In Nagamalai D., Renault E., Dhanuskodi M. (eds.) Trends in Computer Science, Engineering and Information Technology: First International Conference on Computer Science, Engineering and Information Technology, CCSEIT 2011, Tirunelveli, Tamil Nadu, India, September 23–25, 2011. Proceedings, pp. 453–462. Springer (2011)
55.
Fourneret, E., Ochoa, M., Bouquet, F., Botella, J., Jürjens, J., Yousefi, P.: Model-based security verification and testing for smart-cards. In: Sixth International Conference on Availability, Reliability and Security, ARES 2011, Vienna, Austria, August 22–26, 2011, pp. 272–279 (2011)
56.
Jürjens, J.: Secure Systems Development with UML. Springer, Berlin (2010)MATH
57.
Baker, P., Dai, Z.R., Grabowski, J., Haugen, O., Schieferdecker, I., Williams, C.: Model-Driven Testing: Using the UML Testing Profile. Springer, New York (2007)
58.
Global Platform Device Commitee. Global platform tee protection profile version 1.0, August (2013)
Metadaten
Titel
Complementary test selection criteria for model-based testing of security components
verfasst von
Julien Botella
Jean-François Capuron
Frédéric Dadeau
Elizabeta Fourneret
Bruno Legeard
Florence Schadle
Publikationsdatum
28.02.2018
Verlag
Springer Berlin Heidelberg
Erschienen in
International Journal on Software Tools for Technology Transfer / Ausgabe 4/2019
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI
https://doi.org/10.1007/s10009-018-0489-2

Weitere Artikel der Ausgabe 4/2019

International Journal on Software Tools for Technology Transfer 4/2019 Zur Ausgabe

Regular Paper

Comparing approaches for model-checking strategies under imperfect information and fairness constraints

Regular Paper

Parallel reachability analysis of hybrid systems in XSpeed

Regular Paper

ASAP: A Source Code Authorship Program

Regular Paper

Fast detection of concurrency errors by state space traversal with randomization and early backtracking