Header menu link for other important links
X
An algorithmic approach to formally verify an ECC library
Published in Association for Computing Machinery
2018
Volume: 23
   
Issue: 5
Abstract
The weakest link in cryptosystems is quite often due to the implementation rather than the mathematical underpinnings. A vast majority of attacks in the recent past have targeted programming flaws and bugs to break security systems. Due to the complexity, empirically verifying such systems is practically impossible, while manual verification as well as testing do not provide adequate guarantees. In this article, we leverage model checking techniques to prove the functional correctness of an elliptic curve cryptography (ECC) library with respect to its formal specification. We demonstrate how the huge state space of the C library can be aptly verified using a hierarchical assume-guarantee verification strategy. To test the scalability of this approach, we verify the correctness of five NIST-specified elliptic curve implementations. We also verify the newer curve25519 elliptic curve, which is finding multiple applications, due to its higher security and simpler implementation. The 192-bit NIST elliptic curve took 1 day to verify. This was the smallest curve we verified. The largest curve with a 521-bit prime field took 26 days to verify. Curve25519 took 1.5 days to verify. © 2018 ACM.
About the journal
JournalData powered by TypesetACM Transactions on Design Automation of Electronic Systems
PublisherData powered by TypesetAssociation for Computing Machinery
ISSN10844309
Open AccessNo
Concepts (14)
  •  related image
    Cryptography
  •  related image
    Formal verification
  •  related image
    Geometry
  •  related image
    Program debugging
  •  related image
    PUBLIC KEY CRYPTOGRAPHY
  •  related image
    ALGORITHMIC APPROACH
  •  related image
    BOUNDED MODEL CHECKING
  •  related image
    ELLIPTIC CURVE CRYPTOGRAPHY (ECC)
  •  related image
    FUNCTIONAL CORRECTNESS
  •  related image
    Model-checking techniques
  •  related image
    Multiple applications
  •  related image
    Security
  •  related image
    VERIFICATION STRATEGY
  •  related image
    Model checking