Cryptol을 이용한 국내 표준 블록 암호 모듈의 자동 정형 검증
Automated Formal Verification of Korean Standard Block Cipher Using Cryptol
2
조회
0
다운로드
0
인용
0
참고문헌
키워드
초록
암호 알고리즘은 세계적으로 표준화가 진행되고 있으며, 암호 알고리즘의 안전성은 충분히 입증되어 왔다. 하지만, 기존 검증 방법으로는 구현상의 취약점이 존재하여 심각한 피해를 야기할 수 있기 때문에 표준에 따라 올바르게구현되었는지에 대한 개선된 검증 방법이 필요하다. 그러므로 본 논문에서는 국가정보원에서 수행하는 128비트 이상 블록 암호 모듈 중에서 검증 대상인 ARIA와 LEA를 선정하였고, 고신뢰 암호 모듈을 위해 Cryptol을 이용하여 올바르게 구현되었는지 검증하는 방법을 제시하고자 한다.
Abstract
Cryptographic algorithms are being standardized globally, and the security of cryptographic algorithms has been wellproven. However, there is a need for an improved verification method to verify that the existing verification method iscorrectly implemented according to the standard, because there is a weakness in implementation and it can cause seriousdamage. Therefore, in this paper, we selected ARIA and LEA to be verified among 128-bit or more block cipher modulesperformed by the National Intelligence Service, and propose a method to verify whether it is implemented correctly usingCryptol for high-assurance cryptographic module.
참고문헌 (11)
- Zakir Durumeric, "The Matter of Heartbleed", Proceedings of the 2014 ACM Internet Measurement Conference, pp.475~488 (2014)
- 하경주, "암호 알고리즘 구현 적합성 평가 시스템 설계", 한국통신학회논문지B, 39(4), pp.242~250 (2014), 한국통신학회
- P. Caspi, "LUSTRE: A declarative language for programming synchronous systems", Proceedings of the 14th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pp.178~188 (1987)
- Paul Caspi, "From Simulink to SCADE", Lustre to TTA: a Layered Approach for Distributed Embedded Applications, 2003, 153~162
- Jeffrey R. Lewis, "Cryptol: high assurance, retargetable crypto development and validation", IEEE Military Communications Conference, pp.820~825 (2004)
- Levent Erkok, "Pragmatic Equivalence and Safety Checking in Cryptol", Proceedings of the 3rd ACM workshop on Programming languages meets program verification, pp.73~82 (2009)
- Levent Erkok, "Hardware", Software Co-verification of Cryptographic Algorithms using Cryptol, 2009, 188~191
- Levent Erkok, "High assurance programming in Cryptol", Proceedings of the 5th ACM Annual Workshop on Cyber Security and Information Intelligence Research: Cyber Security and Information Intelligence Challenges and Strategies, pp.60~ (2009)
- Lee Pike, "Hints for High-Assurance Cyber-Physical System Design", IEEE Cybersecurity Development (SecDev), pp.25~29 (2016)
- Kyle Carter, "SAW: The Software Analysis Workbench", Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology, pp.15~18 (2013)
- "Github Repository"[URL]