An ACSL-based Formal Verification of Cryptographic Software
Yaohui Hao · Information Security and Communications Privacy · 2011
This article first analyzes the formal verification for universal software,and then proposes an approach for formal verification of cryptographic software security. The approach first adopts ACSL(ANSI/ISO C Specification Language) to formally specify the security of cryptographic software,and then verifies the specifications with the method integrating automatic proof tools and interactive proof assistance. The paper,with the formal verification of RC4 arithmetic in openssl as an example explains this approach. The result shows that this approach could effectively verify properties of cryptographic software in a certain level of automation,and thus reduces the complexity of formal verification in certain degree.