A property-based testing framework for encryption programs

Abstract

In recent years, a variety of encryption algorithms were proposed to enhance the security of software and systems. Validating whether encryption algorithms are correctly implemented is a challenging issue. Software testing delivers an effective and practical solution, but it also faces the oracle problem (that is, under many practical situations, it is impossible or too computationally expensive to know whether the output for any given input is correct). In this paper, we propose a property-based approach to testing encryption programs in the absence of oracles. Our approach makes use of the so-called metamorphic properties of encryption algorithms to generate test cases and verify test results. Two case studies were conducted to illustrate the proposed approach and validate its effectiveness. Experimental results show that even without oracles, the proposed approach can detect nearly 50% inserted faults with at most three metamorphic relations (MRs) and fifty test cases.

Keywords

software testing / encryption programs / test oracles / metamorphic testing (MT)

References

[1] MenezesA J, OorschotP C, VanstoneS A. Handbook of Applied Cryptography. Boca Raton: Chemical Rubber Company Press Inc., 1996

[2] CremersC J. The scyther tool: verification, falsification, and analysis of security protocols. In: Proceedings of the 20th International Conference on Computer Aided Verification. 2008, 414-418

[3] O’SheaN. Using Elyjah to analyse java implementations of cryptographic protocols. In: Proceedings of the 2008 Joint Workshop on Foundations of Computer Security, Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security. 2008, 156-163

[4] UdreaO, LumezanuC, FosterJ S. Rule-based static analysis of network protocol implementations. Information and Computation, 2008, 206(2-4): 130-157

[5] AvalleM, PirontiA, SistoR. Formal verification of security protocol implementations: a survey. Formal Aspects of Computing, 2012, 24(12): 1-25

[6] BlanchetB. Security protocol verification: symbolic and computational models. In: Proceedings of the 1st International Conference on Principles of Security and Trust. 2012, 3-29

[7] BlanchetB. An efflcient cryptographic protocol verifier based on prolog rules. In: Proceedings of the 14th IEEE Workshop on Computer Security Foundations. 2001, 82-96

[8] DenkerG, MeseguerJ, TalcottC. Protocol specification and analysis in maude. In: Proceedings of the 1998 Workshop on Formal Methods and Security Protocols. 1998, 1-19

[9] ArmandoA, CompagnaL, GantyP. Sat-based model-checking of security protocols using planning graph analysis. In: Proceedings of 2003 International Symposium on Formal Methods Europe. 2003, 875-893

[10] HadjicostisC N. Stochastic testing of finite state machines. In: Proceedings of the 2001 American Control Conference. 2001, 6: 4568-4573

[11] SotoJ. Randomness testing of the AES candidate algorithms. Internal Report 6390 of National Institute of Standards and Technology. 1999, 1-9

[12] WeyukerE J. On testing non-testable programs. The Computer Journal. 1982, 25(4): 465-470

[13] ChenT Y, CheungS, YiuS. Metamorphic testing: a new approach for generating next test cases. HKUST-CS98-01 Technical Report, Hong Kong University of Science and Technology. 2008

[14] HillL. Cryptography in an algebraic alphabet. Mathematical Association of America, 1929, 306-312

[15] RivestR L, ShamirA, AdlemanL. A method for obtaining digital signatures and public-key cryptosystems. Communications of the ACM, 1978, 21(2): 120-126

[16] ZhouZ Q, HuangD, TseT H, YangZ, HuangH, ChenT Y. Metamorphic testing and its applications. In: Proceedings of the 8th International Symposium on Future Software Technology. 2004, 1-6

[17] SunC A, WangG, MuB, LiuH, WangZ, ChenT Y. A metamorphic relation-based approach to testing web services without oracles. International Journal of Web Services Research, 2012, 9(1): 51-73

[18] ChenT Y, HoJ W, LiuH, XieX. An innovative approach for testing bioinformatics programs using metamorphic testing. BMC Bioinformatics, 2009, 10: 24

[19] MurphyC, KaiserG E, HuL, WuL. Properties of machine learning applications for use in metamorphic testing. In: Proceedings of the 20th International Conference on Software Engineering and Knowledge Engineering. 2008, 867-872

[20] ZhouZ Q, ZhangS, HagenbuchnerM, TseT H, KuoF C, ChenT Y. Automated functional testing of online search services. Journal of Software Testing, Verification and Reliability, 2012, 22(4): 221-243

[21] ChenT Y. Metamorphic testing: a simple approach to alleviate the oracle problem. In: Proceedings of the 5th IEEE International Symposium on Service Oriented System Engineering. 2010, 1-2

[22] DeMilloR, LiptonR J, SaywardF G. Hints on test data selection: help for the practicing programmer. IEEE Computer, 1978, 11(4): 34-41

[23] SunC A, WangG, CaiK Y, ChenT Y. Distribution-aware mutation analysis. In: Proceedings of the 9th International Workshop on Software Cybernetics, in conjunction with the 36th IEEE International Computer Software and Application Conference. 2012, 170-175

[24] ChenT Y, HuangD, TseT, ZhouZ Q. Case studies on the selection of useful relations in metamorphic testing. In: Proceedings of the 4th Ibero-American Symposium on Software Engineering and Knowledge Engineering. 2004, 569-583

[25] WangR, BenK. Classification of metamorphic relations and its application. American Journal of Engineering and Technology Research, 2011, 11(12): 1664-1668

[26] MurphyC. Metamorphic testing techniques to detect defects in applications without test oracles. PhD thesis. Columbia: Columbia University, 2010

[27] AndrewsJ H, BriandL C, LabicheY. Is mutation an appropriate tool for testing experiments? In: Proceedings of the 27th International Conference on Software Engineering. 2005, 402-411

[28] DelamaroM E, MaldonadoJ C, VincenziA M R. Proteum/IM 2.0: an integrated mutation testing environment. In: Proceedings of the 2000 International Symposium on Mutation. 2000, 91-101

[29] MahmoudA Y, ChefranovA G. Hill cipher modification based on eigenvalues HCM-EE. In: Proceedings of the 2nd International Conference on Security of Information and Networks. 2009, 164-167

[30] ZengH. B.. Teaching the RSA algorithm using spreadsheets. Journal of Computing Sciences in Colleges, 2012, 28(1): 18-24

[31] DesokyA, MadhusoodhananA P. Bitwise hill crypto system. In: Proceedings of the 2011 IEEE International Symposium on Signal Processing and Information Technology. 2011, 80-85

[32] AcharyaB, ShuklaS K, PanigrahyS K, PatraS K, PandaG. Cryptosystem and its application to image encryption. In: Proceedings of the 2009 International Conference on Advances in Computing, Control, and Telecommunication Technologies. 2009, 720-724

[33] RonS, ZhengY. An advantage of low-exponent RSA with modulus primes sharing least significant bits. In: Proceedings of the 2001 International Conference on Topics in Cryptology, the Cryptographer’s Track at RSA. 2001, 52-62

[34] BoldyrevaA. Strengthening security of RSA-OAEP. In: Proceedings of the 2009 International Conference on Topics in Cryptology, the Cryptographer’s Track at RSA. 2009, 399-413

[35] SuG, LiuZ C, YaoX C, YinX W. A test method of sequence randomness of information security system. Chinese Journal of Computer Engineering, 2006, 32(8): 153-154

[36] ShiG D, KangF, GuH W. Research and Implementation of Randomness Tests. Chinese Journal of Computer Engineering, 2009, 35(20): 145-150

[37] MohamedE M, El-EtribyS, Abdul-kaderH S. Randomness testing of modern encryption techniques in cloud environment. In: Proceedings of the 8th International Conference on Informatics and Systems. 2012, CC-1-CC-6

[38] RukhinA, SotoJ, NechvatalJ, SminM, BarkerE, LeighS, LevensonM, VangelM, BanksD, HeckertA, DrayJ, VoS. A statistical test suite for random and pseudorandom number generators for cryptographic applications. Technical Report of National Institute of Standards and Technology. 2001

[39] ZhangB, YangY S, GaoJ P. On the randomness test and its incompleteness. Journal of Tsinghua University (Science and Technology), 2011, 51(10): 1269-1273

[40] Goubault-LarrecqJ, ParrennesF. Cryptographic protocol analysis on real c code. In: Proceedings of the 6th International Conference on Verification, Model Checking, and Abstract Interpretation. 2005, 363-379

[41] DupressoirF, GordonA D, JurjensJ, NaumannD A. Guiding a general-purpose C verifier to prove cryptographic protocols. In: Proceedings of the 24th IEEE Computer Security Foundations Symposium. 2011, 3-17

[42] BodeiC, BuchholtzM, Degano, NielsonF, NielsonH R. Automatic validation of protocol narration. In: Proceedings of the 16th IEEE Workshop on Computer Security Foundations. 2003, 126-140

[43] BhargavanK, FournetC, GordonA D, TseS. Verified interoperable implementations of security protocols. ACM Transactions on Programming Languages and Systems, 2008, 31(1): 1-61

[44] AizatulinM, GordonA D, JürjensJ. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: Proceedings of the 18th ACM Conference on Computer and Communications Security. 2011, 331-340

[45] JurjensJ. Security analysis of crypto-based java programs using automated theorem provers. In: Proceedings of the 21st IEEE/ACM International Conference on Automated Software Engineering. 2006, 167-176

[46] BertoniG, BreveglieriL, KorenI, MaistriP, PiuriV. A parity code based fault detection for an implementation of the advanced encryption standard. In: Proceedings of the 17th IEEE International Symposium on Defect and Fault-Tolerance in VLSI Systems. 2002, 51-59

[47] Announcing the Advanced Encryption Standard. Federal Information Processing Standards Publication 197. 2001

[48] Mozaffari-KermaniM, Reyhani-MasolehA. Fault detection structures of the S-boxes and the inverse S-boxes for the advanced encryption standard. Journal of Electronic Testing, 2009, 25(4-5): 225-245

[49] DingJ, WuT, LuJ Q, HuX H. Self-checked metamorphic testing of an image processing program. In: Proceedings of the 4th International Conference on Secure Software Integration and Reliability Improvement. 2010, 190-197

[50] TseT H, YauS S, ChanW K, LuH, ChenT Y. Testing context sensitive middleware-based software applications. In: Proceedings of the 28th Annual International Computer Software and Applications Conference. 2004, 458-466

[51] ChanW K, ChenT Y, LuH. A metamorphic approach to integration testing of context-sensitive middleware-based applications. In: Proceedings of the 5th International Conference on Quality Software. 2005, 241-249

[52] MyersG J, SandlerC, BadgettT. The Art of Software Testing. 3rd Edition. Wiley Publishing, 2011

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg