A Survey on Tools and Techniques for the Programming and Verification of Secure Cryptographic Software
Resumo
This paper contributes to broaden the discussion on tools and techniques in cryptographic programming and verification. The paper accomplishes three goals: (i) surveys recent advances in supporting tools for cryptographic software programming and verification; (ii) associates these tools to current security practices; and (iii) organizes their use into software programming and verification steps. The paper concludes that there is no single tool for secure development of cryptographic software. Instead, only a well-crafted toolkit can cover the whole landscape of secure cryptographic software coding and verification.
Referências
J. Saltzer and M. Schroeder, “The protection of information in computer systems,” Proc. of the IEEE, vol. 63, no. 9, pp. 1278–1308, 1975.
R. Anderson, “Security engineering,” 2001.
G. McGraw, Software Security: Building Security in. 2006.
B. Schneier, “Cryptographic design vulnerabilities,” Comp., Sep., pp.29–33, 1998.
P. Gutmann, “Lessons Learned in Implementing and Deploying Crypto Software,” Usenix Security Symposium, 2002.
R. Anderson, “Why Cryptosystems Fail,” in Proc. of the 1st ACM Conf. on Computer and Comm. Security, 1993, pp. 215–227.
B. Schneier, “Designing Encryption Algorithms for Real People,” Proc. of the 1994 workshop on New security paradigms., pp. 98–101, 1994.
A. Shamir and N. Van Someren, “Playing ‘hide and seek’with stored keys,” Financial cryptography, pp. 1–9, 1999.
D. Akhawe, B. Amann, M. Vallentin, and R. Sommer, “Here’s My Cert, So Trust Me, Maybe?: Understanding TLS Errors on the Web,” in Proc. of the 22Nd Intn’l Conf. on World Wide Web, 2013, pp. 59–70.
E. S. Alashwali, “Cryptographic vulnerabilities in real-life web servers,” 2013 Third Intn’l Conf. on Comm. and Inform. Technology (ICCIT), pp. 6–11, 2013.
M. Egele, D. Brumley, Y. Fratantonio, and C. Kruegel, “An empirical study of cryptographic misuse in android applications,” Proc. of the 2013 ACM SIGSAC Conf. on Computer & Comm. security CCS ’13, pp. 73–84, 2013.
M. Georgiev, S. Iyengar, and S. Jana, “The most dangerous code in the world: validating SSL certificates in non-browser software,” in Proc. of the 2012 ACM Conf. on Computer and Comm. security CCS ’12 (2012), 2012, pp. 38–49.
S. Fahl, M. Harbach, and T. Muders, “Why Eve and Mallory love Android: An analysis of Android SSL (in) security,” Proc. of the 2012 ACM Conf. on Computer and Comm. security, pp. 50–61, 2012.
S. Shuai, D. Guowei, G. Tao, Y. Tianchang, and S. Chenjie, “Modelling Analysis and Auto-detection of Cryptographic Misuse in Android Applications,” in IEEE 12th Intn’l Conf. on Dependable, Autonomic and Secure Computing (DASC), 2014, pp. 75–80.
D. Lazar, H. Chen, X. Wang, and N. Zeldovich, “Why Does Cryptographic Software Fail?: A Case Study and Open Problems,” in Proc. of 5th Asia-Pacific Workshop on Systems, 2014, pp. 7:1–7:7.
“Real World Cryptography Workshop Series.” [Online]. Available: http://www.realworldcrypto.com.
“The Heartbleed Bug.” [Online]. Available: http://heartbleed.com/.
“Apple’s SSL/TLS ‘Goto fail’ bug.” [Online]. Available: https://www.imperialviolet.org/2014/02/22/applebug.html.
S. Vaudenay, “Security Flaws Induced by CBC Padding—Applications to SSL, IPSEC, WTLS...,” Advances in Cryptology—EUROCRYPT 2002, no. 1, 2002.
J. Rizzo and T. Duong, “Practical padding oracle attacks,” Proc. of the 4th USENIX Conf. on Offensive technologies (2010), pp. 1–9, 2010.
T. Jager and J. Somorovsky, “How to break XML encryption,” Proc. of the 18th ACM Conf. on Computer and Comm. security CCS ’11, p. 413, 2011.
T. Duong and J. Rizzo, “Cryptography in the Web: The Case of Cryptographic Design Flaws in ASP.NET,” IEEE Symp. on Sec. and Priv., pp. 481–489, 2011.
“Java Cryptography Architecture (JCA) Reference Guide.” [Online]. Available: https://docs.oracle.com/javase/8/docs/technotes/guides/security/crypto/CryptoSpec.html.
S. Fahl, M. Harbach, and H. Perl, “Rethinking SSL development in an appified world,” Proc. of the 2013 ACM SIGSAC Conf. on Computer & Comm. security CCS ’13 (2013), pp. 49–60, 2013.
E. Bangerter, S. Krenn, M. Seifriz, and U. Ultes-Nitsche, “cPLC — A cryptographic programming language and compiler,” Information Security for South Africa, pp. 1–8, Aug. 2011.
M. Barbosa, A. Moss, and D. Page, “Constructive and Destructive Use of Compilers in Elliptic Curve Cryptography,” Journal of Cryptology, vol. 22, no. 2, pp. 259–281, 2008.
“Cryptol.” [Online]. Available: http://www.cryptol.net.
A. Bain, J. Mitchell, R. Sharma, and D. Stefan, “A Domain-Specific Language for Computing on Encrypted Data (Invited Talk).,” FSTTCS, 2011.
M. Barbosa, A. Moss, D. Page, N. F. Rodrigues, and P. F. Silva, “Type checking cryptography implementations,” in Fundamentals of Software Engineering, Springer, 2012, pp. 316–334.
M. Barbosa, D. Castro, and P. Silva, “Compiling CAO: From Cryptographic Specifications to C Implementations,” Principles of Security and Trust, 2014.
J. Lewis, “Cryptol: Specification, Implementation and Verification of High-grade Cryptographic Applications,” in Proc. of the 2007 ACM Workshop on Formal Methods in Security Engineering, 2007, p. 41.
J. J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, “Certified computeraided cryptography: efficient provably secure machine code from high-level implementations,” in ACM Conf. on Comp. & Comm. Sec. (SIGSAC), 2013, pp. 1217–1229.
A. Moss, E. Oswald, D. Page, and M. Tunstall, “Automatic Insertion of DPA Countermeasures.,” IACR Cryptology ePrint Archive, vol. 2011, p. 412, 2011.
A. Moss, E. Oswald, D. Page, and M. Tunstall, “Compiler assisted masking,” in Cryptographic Hardware and Embedded Systems (CHES), 2012, pp. 58–75.
G. Agosta, A. Barenghi, M. Maggi, and G. Pelosi, “Compiler-based side channel vulnerability analysis and optimized countermeasures application,” in Design Automation Conf. (DAC), 2013 50th ACM/EDAC/IEEE, 2013, pp. 1–6.
P. Bourque and R. Fairley, Eds., Guide to the Software Engineering Body of Knowledge (SWEBOK), Version 3. IEEE Computer Society, 2014.
A. Braga and E. Nascimento, “Portability evaluation of cryptographic libraries on android smartphones,” Cyberspace Safety and Security, pp. 459–469, 2012.
D. González, O. Esparza, J. Muñoz, J. Alins, and J. Mata, “Evaluation of Cryptographic Capabilities for the Android Platform,” in Future Network Systems and Security SE 2, vol. 523, Springer, 2015, pp. 16–30.
P. Gutmann, “The design of a cryptographic security architecture,” Proc. of the 8th USENIX Security Symposium, 1999.
D. Bernstein, T. Lange, and P. Schwabe, “The security impact of a new cryptographic library,” Progress in Cryptology – LATINCRYPT 2012 (LNCS), vol. 7533, pp. 159–176, 2012.
C. Forler, S. Lucks, and J. Wenzel, “Designing the API for a Cryptographic Library: A Misuse-resistant Application Programming Interface,” in Proc. of the 17th Ada-Europe Intn’l Conf. on Reliable Software Technol., 2012, pp. 75–88.
M. Fayad and D. C. Schmidt, “Object-oriented application frameworks,” Comm. of the ACM, vol. 40, no. 10, pp. 32–38, Oct. 1997.
R. E. Johnson, “Frameworks = (components + patterns),” Comm. of the ACM, vol. 40, no. 10, pp. 39–42, Oct. 1997.
A. D. A. Keromytis, J. L. J. Wright, T. De Raadt, and M. Burnside, “Cryptography As an Operating System Service: A Case Study,” ACM Trans. Comput. Syst., vol. 24, no. 1, pp. 1–38, 2006.
A. D. A. Keromytis, J. L. J. Wright, T. De Raadt, and T. De Raadt, “The Design of the {OpenBSD} Cryptographic Framework.,” in USENIX Annual Technical Conf., General Track, 2003, pp. 181–196.
“Secure Coding Practices,” OWASP. [Online]. Available: [link].
SANS/CWE, “TOP 25 Most Dangerous Software Errors.” [Online]. Available: https://www.sans.org/top25-software-errors.
“Cryptography Coding Standard.” [Online]. Available: https://cryptocoding.net/index.php/Cryptography_Coding_Standard.
A. Lux and A. Starostin, “A tool for static detection of timing channels in Java,” Journal of Cryptographic Engineering, vol. 1, no. 4, pp. 303–313, Oct. 2011.
A. G. Bayrak, F. Regazzoni, D. Novo, and P. Ienne, “Sleuth: Automated verification of software power analysis countermeasures,” in Cryptographic Hardware and Embedded Systems-CHES 2013, 2013, pp. 293–310.
G. Doychev, B. Köpf, L. Mauborgne, and J. Reineke, “CacheAudit: A Tool for the Static Analysis of Cache Side Channels,” ACM Trans. Inf. Syst. Secur., vol. 18, no. 1, pp. 4:1–4:32, 2015.
J. B. Almeida, M. Barbosa, J.-C. Filliâtre, J. S. Pinto, and B. Vieira, “CAOVerif: An open-source deductive verification platform for cryptographic software implementations,” Science of Computer Prog., vol. 91, pp. 216–233, 2014.
NIST, “Cryptographic Algorithm Validation Program (CAVP).” [Online]. Available: https://csrc.nist.gov/groups/STM/cavp/index.html.
A. Braga and D. Schwab, “The Use of Acceptance Test-Driven Development to Improve Reliability in the Construction of Cryptographic Software,” in The Ninth Intn’l Conf. on Emerging Security Information, Systems and Technologies (SECURWARE 2015). Accepted., 2015.
OWASP, “Testing for Padding Oracle.” [Online]. Available: https://www.owasp.org/index.php/Testing_for_Padding_Oracle_(OTG-CRYPST-002).
OWASP, “Top10 2013 (A6 Sensitive Data Exposure).” .
OWASP, “Key Management Cheat Sheet.” [Online]. Available: https://www.owasp.org/index.php/Key_Management_Cheat_Sheet.
NIST, “Cryptographic Module Validation Program (CMVP).” [Online]. Available: http://csrc.nist.gov/groups/STM/cmvp/index.html.
A. Barenghi, L. Breveglieri, I. Koren, D. Naccache, B. A. Barenghi, L. Breveglieri, I. Koren, F. Ieee, D. Naccache, and A. Barenghi, “Fault injection attacks on cryptographic devices: Theory, practice, and countermeasures,” in Proc. of the IEEE, 2012, vol. 100, no. 11, pp. 3056–3076.
R. Anderson, “Security engineering,” 2001.
G. McGraw, Software Security: Building Security in. 2006.
B. Schneier, “Cryptographic design vulnerabilities,” Comp., Sep., pp.29–33, 1998.
P. Gutmann, “Lessons Learned in Implementing and Deploying Crypto Software,” Usenix Security Symposium, 2002.
R. Anderson, “Why Cryptosystems Fail,” in Proc. of the 1st ACM Conf. on Computer and Comm. Security, 1993, pp. 215–227.
B. Schneier, “Designing Encryption Algorithms for Real People,” Proc. of the 1994 workshop on New security paradigms., pp. 98–101, 1994.
A. Shamir and N. Van Someren, “Playing ‘hide and seek’with stored keys,” Financial cryptography, pp. 1–9, 1999.
D. Akhawe, B. Amann, M. Vallentin, and R. Sommer, “Here’s My Cert, So Trust Me, Maybe?: Understanding TLS Errors on the Web,” in Proc. of the 22Nd Intn’l Conf. on World Wide Web, 2013, pp. 59–70.
E. S. Alashwali, “Cryptographic vulnerabilities in real-life web servers,” 2013 Third Intn’l Conf. on Comm. and Inform. Technology (ICCIT), pp. 6–11, 2013.
M. Egele, D. Brumley, Y. Fratantonio, and C. Kruegel, “An empirical study of cryptographic misuse in android applications,” Proc. of the 2013 ACM SIGSAC Conf. on Computer & Comm. security CCS ’13, pp. 73–84, 2013.
M. Georgiev, S. Iyengar, and S. Jana, “The most dangerous code in the world: validating SSL certificates in non-browser software,” in Proc. of the 2012 ACM Conf. on Computer and Comm. security CCS ’12 (2012), 2012, pp. 38–49.
S. Fahl, M. Harbach, and T. Muders, “Why Eve and Mallory love Android: An analysis of Android SSL (in) security,” Proc. of the 2012 ACM Conf. on Computer and Comm. security, pp. 50–61, 2012.
S. Shuai, D. Guowei, G. Tao, Y. Tianchang, and S. Chenjie, “Modelling Analysis and Auto-detection of Cryptographic Misuse in Android Applications,” in IEEE 12th Intn’l Conf. on Dependable, Autonomic and Secure Computing (DASC), 2014, pp. 75–80.
D. Lazar, H. Chen, X. Wang, and N. Zeldovich, “Why Does Cryptographic Software Fail?: A Case Study and Open Problems,” in Proc. of 5th Asia-Pacific Workshop on Systems, 2014, pp. 7:1–7:7.
“Real World Cryptography Workshop Series.” [Online]. Available: http://www.realworldcrypto.com.
“The Heartbleed Bug.” [Online]. Available: http://heartbleed.com/.
“Apple’s SSL/TLS ‘Goto fail’ bug.” [Online]. Available: https://www.imperialviolet.org/2014/02/22/applebug.html.
S. Vaudenay, “Security Flaws Induced by CBC Padding—Applications to SSL, IPSEC, WTLS...,” Advances in Cryptology—EUROCRYPT 2002, no. 1, 2002.
J. Rizzo and T. Duong, “Practical padding oracle attacks,” Proc. of the 4th USENIX Conf. on Offensive technologies (2010), pp. 1–9, 2010.
T. Jager and J. Somorovsky, “How to break XML encryption,” Proc. of the 18th ACM Conf. on Computer and Comm. security CCS ’11, p. 413, 2011.
T. Duong and J. Rizzo, “Cryptography in the Web: The Case of Cryptographic Design Flaws in ASP.NET,” IEEE Symp. on Sec. and Priv., pp. 481–489, 2011.
“Java Cryptography Architecture (JCA) Reference Guide.” [Online]. Available: https://docs.oracle.com/javase/8/docs/technotes/guides/security/crypto/CryptoSpec.html.
S. Fahl, M. Harbach, and H. Perl, “Rethinking SSL development in an appified world,” Proc. of the 2013 ACM SIGSAC Conf. on Computer & Comm. security CCS ’13 (2013), pp. 49–60, 2013.
E. Bangerter, S. Krenn, M. Seifriz, and U. Ultes-Nitsche, “cPLC — A cryptographic programming language and compiler,” Information Security for South Africa, pp. 1–8, Aug. 2011.
M. Barbosa, A. Moss, and D. Page, “Constructive and Destructive Use of Compilers in Elliptic Curve Cryptography,” Journal of Cryptology, vol. 22, no. 2, pp. 259–281, 2008.
“Cryptol.” [Online]. Available: http://www.cryptol.net.
A. Bain, J. Mitchell, R. Sharma, and D. Stefan, “A Domain-Specific Language for Computing on Encrypted Data (Invited Talk).,” FSTTCS, 2011.
M. Barbosa, A. Moss, D. Page, N. F. Rodrigues, and P. F. Silva, “Type checking cryptography implementations,” in Fundamentals of Software Engineering, Springer, 2012, pp. 316–334.
M. Barbosa, D. Castro, and P. Silva, “Compiling CAO: From Cryptographic Specifications to C Implementations,” Principles of Security and Trust, 2014.
J. Lewis, “Cryptol: Specification, Implementation and Verification of High-grade Cryptographic Applications,” in Proc. of the 2007 ACM Workshop on Formal Methods in Security Engineering, 2007, p. 41.
J. J. B. Almeida, M. Barbosa, G. Barthe, and F. Dupressoir, “Certified computeraided cryptography: efficient provably secure machine code from high-level implementations,” in ACM Conf. on Comp. & Comm. Sec. (SIGSAC), 2013, pp. 1217–1229.
A. Moss, E. Oswald, D. Page, and M. Tunstall, “Automatic Insertion of DPA Countermeasures.,” IACR Cryptology ePrint Archive, vol. 2011, p. 412, 2011.
A. Moss, E. Oswald, D. Page, and M. Tunstall, “Compiler assisted masking,” in Cryptographic Hardware and Embedded Systems (CHES), 2012, pp. 58–75.
G. Agosta, A. Barenghi, M. Maggi, and G. Pelosi, “Compiler-based side channel vulnerability analysis and optimized countermeasures application,” in Design Automation Conf. (DAC), 2013 50th ACM/EDAC/IEEE, 2013, pp. 1–6.
P. Bourque and R. Fairley, Eds., Guide to the Software Engineering Body of Knowledge (SWEBOK), Version 3. IEEE Computer Society, 2014.
A. Braga and E. Nascimento, “Portability evaluation of cryptographic libraries on android smartphones,” Cyberspace Safety and Security, pp. 459–469, 2012.
D. González, O. Esparza, J. Muñoz, J. Alins, and J. Mata, “Evaluation of Cryptographic Capabilities for the Android Platform,” in Future Network Systems and Security SE 2, vol. 523, Springer, 2015, pp. 16–30.
P. Gutmann, “The design of a cryptographic security architecture,” Proc. of the 8th USENIX Security Symposium, 1999.
D. Bernstein, T. Lange, and P. Schwabe, “The security impact of a new cryptographic library,” Progress in Cryptology – LATINCRYPT 2012 (LNCS), vol. 7533, pp. 159–176, 2012.
C. Forler, S. Lucks, and J. Wenzel, “Designing the API for a Cryptographic Library: A Misuse-resistant Application Programming Interface,” in Proc. of the 17th Ada-Europe Intn’l Conf. on Reliable Software Technol., 2012, pp. 75–88.
M. Fayad and D. C. Schmidt, “Object-oriented application frameworks,” Comm. of the ACM, vol. 40, no. 10, pp. 32–38, Oct. 1997.
R. E. Johnson, “Frameworks = (components + patterns),” Comm. of the ACM, vol. 40, no. 10, pp. 39–42, Oct. 1997.
A. D. A. Keromytis, J. L. J. Wright, T. De Raadt, and M. Burnside, “Cryptography As an Operating System Service: A Case Study,” ACM Trans. Comput. Syst., vol. 24, no. 1, pp. 1–38, 2006.
A. D. A. Keromytis, J. L. J. Wright, T. De Raadt, and T. De Raadt, “The Design of the {OpenBSD} Cryptographic Framework.,” in USENIX Annual Technical Conf., General Track, 2003, pp. 181–196.
“Secure Coding Practices,” OWASP. [Online]. Available: [link].
SANS/CWE, “TOP 25 Most Dangerous Software Errors.” [Online]. Available: https://www.sans.org/top25-software-errors.
“Cryptography Coding Standard.” [Online]. Available: https://cryptocoding.net/index.php/Cryptography_Coding_Standard.
A. Lux and A. Starostin, “A tool for static detection of timing channels in Java,” Journal of Cryptographic Engineering, vol. 1, no. 4, pp. 303–313, Oct. 2011.
A. G. Bayrak, F. Regazzoni, D. Novo, and P. Ienne, “Sleuth: Automated verification of software power analysis countermeasures,” in Cryptographic Hardware and Embedded Systems-CHES 2013, 2013, pp. 293–310.
G. Doychev, B. Köpf, L. Mauborgne, and J. Reineke, “CacheAudit: A Tool for the Static Analysis of Cache Side Channels,” ACM Trans. Inf. Syst. Secur., vol. 18, no. 1, pp. 4:1–4:32, 2015.
J. B. Almeida, M. Barbosa, J.-C. Filliâtre, J. S. Pinto, and B. Vieira, “CAOVerif: An open-source deductive verification platform for cryptographic software implementations,” Science of Computer Prog., vol. 91, pp. 216–233, 2014.
NIST, “Cryptographic Algorithm Validation Program (CAVP).” [Online]. Available: https://csrc.nist.gov/groups/STM/cavp/index.html.
A. Braga and D. Schwab, “The Use of Acceptance Test-Driven Development to Improve Reliability in the Construction of Cryptographic Software,” in The Ninth Intn’l Conf. on Emerging Security Information, Systems and Technologies (SECURWARE 2015). Accepted., 2015.
OWASP, “Testing for Padding Oracle.” [Online]. Available: https://www.owasp.org/index.php/Testing_for_Padding_Oracle_(OTG-CRYPST-002).
OWASP, “Top10 2013 (A6 Sensitive Data Exposure).” .
OWASP, “Key Management Cheat Sheet.” [Online]. Available: https://www.owasp.org/index.php/Key_Management_Cheat_Sheet.
NIST, “Cryptographic Module Validation Program (CMVP).” [Online]. Available: http://csrc.nist.gov/groups/STM/cmvp/index.html.
A. Barenghi, L. Breveglieri, I. Koren, D. Naccache, B. A. Barenghi, L. Breveglieri, I. Koren, F. Ieee, D. Naccache, and A. Barenghi, “Fault injection attacks on cryptographic devices: Theory, practice, and countermeasures,” in Proc. of the IEEE, 2012, vol. 100, no. 11, pp. 3056–3076.
Publicado
09/11/2015
Como Citar
BRAGA, Alexandre; DAHAB, Ricardo.
A Survey on Tools and Techniques for the Programming and Verification of Secure Cryptographic Software. In: SIMPÓSIO BRASILEIRO DE SEGURANÇA DA INFORMAÇÃO E DE SISTEMAS COMPUTACIONAIS (SBSEG), 15. , 2015, Florianópolis.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2015
.
p. 30-43.
DOI: https://doi.org/10.5753/sbseg.2015.20083.
