We provide a technical introduction on how to leverage the Z3 Theorem Prover to reason about the correctness of cryptographic software, protocols and otherwise, and to identify potential security vulnerabilities. We cover two distinct use cases: modeling and analysis of an algorithm documented in an old version of the QUIC Transport protocol IETF draft; modeling of specific finite field arithmetic operations for elliptic curve cryptography, with integers represented using a uniform saturated limb schedule, to prove equivalence with arbitrary-precision arithmetic, and for test cases generation.
wolfSSL is a C-language-based SSL/TLS library targeted at IoT, embedded, and RTOS environments. wolfSSL incorrectly implements the TLS 1.3 client state machine. This allows attackers in a privileged network position to completely impersonate any TLS 1.3 servers and read or modify potentially sensitive information between clients using the wolfSSL library and these TLS servers.
Running smart contracts in a Trusted Execution Environment (TEE) such as Intel Software Guard Extensions (SGX) to preserve the confidentiality of blockchain transactions is a novel and not widely understood technique. In this blog post, we point out several bug classes that we observed in confidential smart contract designs and implementations in our recent client … Continue reading Smart Contracts Inside SGX Enclaves: Common Security Bug Patterns