A property-based testing framework for encryption programs
Chang-ai SUN1,2,*(),Zuoyi WANG1,Guan WANG1
1. School of Computer and Communication Engineering, University of Science and Technology Beijing, Beijing 100083, China 2. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China
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.
MenezesA J, OorschotP C, VanstoneS A. Handbook of Applied Cryptography. Boca Raton: Chemical Rubber Company Press Inc., 1996 doi: 10.1201/9781439821916
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 doi: 10.1007/978-3-540-70545-1_38
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 doi: 10.1016/j.ic.2007.05.007
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 doi: 10.1007/978-3-642-28641-4_2
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 doi: 10.1093/comjnl/25.4.465
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 doi: 10.1145/359340.359342
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 doi: 10.4018/jwsr.2012010103
18
ChenT Y, HoJ W, LiuH, XieX. An innovative approach for testing bioinformatics programs using metamorphic testing. BMC Bioinformatics, 2009, 10: 24 doi: 10.1186/1471-2105-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 doi: 10.1002/stvr.437
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 doi: 10.1109/C-M.1978.218136
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 doi: 10.1109/ISSPIT.2011.6151539
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 doi: 10.1109/ACT.2009.183
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 doi: 10.1007/978-3-540-30579-8_24
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 doi: 10.1145/1452044.1452049
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 doi: 10.1109/ASE.2006.60
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 doi: 10.1007/s10836-009-5108-4
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
