SpringerLink
Log in

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

  • Regular Paper
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Germany)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13

Similar content being viewed by others

Notes

  1. http://www.smartesting.com/en/certifyit.

  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).

References

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Google Scholar 

  11. Utting, M., Legeard, B.: Practical Model-Based Testing—a Tools Approach, p. 550. Elsevier Science, Amsterdam (2006)

    Google Scholar 

  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)

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  51. Vegas, S., Basili, V.: A characterisation schema for software testing techniques. Empir. Softw. Eng. 10(4), 437–466 (2005)

    Article  Google Scholar 

  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)

    Article  Google Scholar 

  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  Google Scholar 

  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)

    Google Scholar 

  58. Global Platform Device Commitee. Global platform tee protection profile version 1.0, August (2013)

Download references

Author information

Authors and Affiliations

  1. Smartesting Solutions and Services, 18 rue Alain Savary, 25000, Besançon, France

    Julien Botella, Elizabeta Fourneret & Bruno Legeard

  2. DGA Information Superiority, Bruz, France

    Jean-François Capuron & Florence Schadle

  3. FEMTO-ST Institute (UMR CNRS 6174) - University of Bourgogne Franche-Comté, Besançon, France

    Frédéric Dadeau & Bruno Legeard

Authors
  1. Julien Botella
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jean-François Capuron
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Frédéric Dadeau
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Elizabeta Fourneret
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Bruno Legeard
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Florence Schadle
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Frédéric Dadeau.

Additional information

This research was supported by the French ANR ASTRID Maturation MBT_Sec project (ANR-13-ASMA-0003).

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Botella, J., Capuron, JF., Dadeau, F. et al. Complementary test selection criteria for model-based testing of security components. Int J Softw Tools Technol Transfer 21, 425–448 (2019). https://doi.org/10.1007/s10009-018-0489-2

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-018-0489-2

Keywords

Search

Navigation