wolf-crypto 0.1.0-alpha.7

Safe and thin API for wolfSSL's wolfcrypt
Documentation

Table of Contents

  1. wolf-crypto
  2. Testing
    1. Current Test Suite
      1. Unit Tests
      2. Property Tests
      3. NIST CSRC CAVP Tests
      4. Official KATs (Known Answer Tests)
    2. Goals and Approach
    3. Comparison with wolfcrypt
    4. Formal Verification Considerations
      1. Current Tools and Limitations
      2. Future Prospects
      3. Important Note on Limitations
    5. Future Enhancements
      1. Constant-time Behavior Testing
      2. Expanded Test Coverage
  3. Current Priorities
  4. License
  5. Notes
  6. Roadmap [1/5]

WARNING - THIS LIBRARY IS IN ITS EARLY STAGES, IT IS NOT READY FOR PRODUCTION USE, USE AT YOUR OWN RISK.

wolf-crypto

This library seeks to provide a safe, zero-cost, API for wolfcrypt by wolfSSL. It is in its very early stages, some feature flags are misleading, for instance allow-non-fips implies that when disabled only FIPS 140-3 certified cryptography is used. This is not currently the case due to the associated wolf-crypto-sys not currently leveraging the FIPS-MODE feature. This feature will eventually be enabled, as it was my original reason for beginning to work on this, though the library as previously mentioned is incredibly immature.

Currently, the hash module is the most tested segment of this codebase, outside of this module and the aes module I personally would not be comfortable using anything in a general purpose application (not any of my professional work in security).

Testing

Despite not implementing cryptography by hand, this library deals with cryptography and FFI (involving unsafe code). Consequently, comprehensive testing is crucial. Although still in alpha, we maintain an extensive test suite:

Current Test Suite

Unit Tests

  • Check edge cases
  • Ensure behavior equivalent to robust implementations (e.g., rust-crypto) under these edge cases.

Property Tests

  • Verify expected properties (e.g., encryption bijectivity).
  • Confirm documented properties.
  • Compare against robust implementations for equivalence.

NIST CSRC CAVP Tests

  • Implemented for hashing functions (current or previously NIST-recommended).
  • Includes:
    • Monte-Carlo tests.
    • Known Answer tests (short and long datasets).

Official KATs (Known Answer Tests)

  • Used for algorithms not covered by NIST CAVP.
  • Example: BLAKE2 algorithm.

Goals and Approach

  • Aim for production-ready robustness by first minor release.
  • Design as a thin, type-safe, and memory-safe wrapper around FIPS 140-3 certified wolfcrypt.
  • Careful to avoid introducing security risks.
  • Enforce secure programming practices (e.g., prompt zeroing of secrets from memory).

Comparison with wolfcrypt

  • wolfcrypt has undergone necessary testing and validation for FIPS 140-3 certification.
  • We apply rigorous testing to our abstraction layer.
  • Ensure we don't inadvertently violate underlying certified properties.
  • Build confidence through equivalence testing with other Rust cryptography projects.

Formal Verification Considerations

  • Not formally verified due to impracticality with current Rust tools and FFI.
  • Formal verification is rare but highly valuable for ensuring correctness.
  • Attempting to formally verify our API would have minimal benefits due to necessary assumptions about wolfcrypt.

Current Tools and Limitations

  1. Prusti

    • Handling of lifetimes is practically non-existent.
    • Viper framework struggles with prophecies.
    • Workaround: Creating assumed-correct functions that snap underlying data, stripping lifetimes.

  2. Creusot

    • Built on Why3 with comma lang.
    • Excellent handling of lifetimes using prophecies (based on Martín Abadi and Leslie Lamport's work).
    • Challenges:
      • Installation can be difficult (script issues, manual installation sometimes necessary).
      • Requires nightly Rust, even when not verifying specifications.
      • Necessitates conditional compilation for everything.

  3. Kani

    • Less rigorous than Prusti or Creusot, but useful for libraries lacking formal verification.
    • Currently lacks proper FFI support, limiting its applicability to this crate.
    • This crate implements Kani's Arbitrary trait for certain types.
    • Some proofs using Kani are included, anticipating future improvements in FFI support.

Future Prospects

  • Formal verification tools in Rust are promising but still in early stages.
  • As tools improve, particularly in handling FFI, more comprehensive verification may become feasible.
  • Continuous monitoring of advancements in formal verification for Rust.

Important Note on Limitations

Even with potential future formal verification of our API, it would not constitute complete formal verification as wolfcrypt, the underlying cryptographic module, is not formally verified. True formal guarantees would require formal verification of both our API and the underlying wolfcrypt implementation.

Future Enhancements

Constant-time Behavior Testing

  • Challenge: High-level abstraction introduces noise in black-box testing.
  • Considerations:
    • wolfcrypt's cryptography implementation is constant-time.
    • Public API includes non-constant-time checks.
  • Potential approaches:
    • Manual review of assembly.
    • High-level taint analysis (challenging across FFI).
  • Importance: Preventing information leakage.

Expanded Test Coverage

  • Focus on security properties beyond traditional code coverage.
  • Implement more sophisticated constant-time behavior tests when feasible.

Current Priorities

  • Focus on implementing and stabilizing the core FIPS 140-3 compatible algorithms.
  • Improve test coverage in hashing, symmetric encryption, and AEAD modules.
  • Incrementally implement and test asymmetric cryptographic functions (RSA, ECDSA, ECDH).
  • Enable FIPS-MODE support in wolf-crypto-sys to align with the FIPS compliance goals.

License

This library is under GPLv2 licensing unless you purchased a commercial license from wolfSSL.

Notes

  • Affiliation: I am not affiliated with wolfSSL, I just enjoy security and have appreciation for their work.
  • Why is this named wolf-crypto and not wolfcrypt: I did not want to take the official name by wolfSSL.

Roadmap [1/5]

  • Hashing [6/6]

    • SHA2 [6/6]
      • SHA-224
      • SHA-256
      • SHA-384
      • SHA-512
      • SHA-512/224
      • SHA-512/256
    • SHA3 [5/5]
      • SHA3-224
      • SHA3-256
      • SHA3-384
      • SHA3-512
      • SHAKE [2/2]
        • SHAKE128
        • SHAKE256
    • SHA [1/1]
    • RIPEMD-160 [1/1]
    • MD [2/2]
      • MD5
      • MD4
    • BLAKE2 [2/2]
      • BLAKE2b
      • BLAKE2s

  • AEAD [1/5]

    • AES-GCM [3/3]
      • 256
      • 192
      • 128
    • ChaCha20-Poly1305 [0/2]
      • 256
      • 128
    • AES-CCM [0/3]
      • 256
      • 192
      • 128
    • AES-EAX [0/3]
      • 256
      • 192
      • 128
    • AES-SIV [0/3]
      • 256
      • 192
      • 128

  • Symmetric Encryption [0/3]

    • AES [1/4]
      • CTR [3/3]
        • 256
        • 192
        • 128
      • CBC [0/3]
        • 256
        • 192
        • 128
      • XTS [0/2]
        • 256
        • 128
      • CFB [0/3]
        • 256
        • 192
        • 128
    • ChaCha20 [0/2]
      • 256
      • 128
    • 3DES [0/1]
      • 168

  • MAC [0/2]

    • HMAC [0/9]
      • SHA-256
      • SHA-384
      • SHA-512
      • SHA3-224
      • SHA3-256
      • SHA3-384
      • SHA3-512
      • SHA
      • MD5
    • Poly1305 [0/1]
      • Poly1305

  • Writing the Remaining Sections (asymmetric, password, padding, etc)