A blueprint for formal verification of Apple corecrypto
23 points by typesanitizer
23 points by typesanitizer
The library source: https://github.com/apple/corecrypto/tree/main And the verification subdir just because it took me a moment to find it: https://github.com/apple/corecrypto/tree/main/corecrypto_verify
Ok, I've been reading the more detailed document at https://github.com/apple/corecrypto/blob/main/corecrypto_verify/technical_overview/formal-verification-for-apple-corecrypto.md
As far as I can tell they're starting with a formal model of the MachO object format and arm64 instruction encoding, parsing that into a formal model of an ARM64 interpreter, proving equivalence of that to the C implementations, then the equivalence of the C implementation to a formal specification of the implementation, the equivalence of that to a formal model of the actual cryptographic operations, and then the equivalence of that to a formal specification the made of the FIPS specification????