RWC 2026 program

Real World Crypto Symposium

Cryspen | Control flow analysis with hax

High Assurance Software

hax: Verifying Security-Critical Rust Software using Multiple Provers

We present hax, a verification toolchain for Rust targeted at security-critical software such as cryptographic libraries, protocol imple- mentations, authentication and authorization mechanisms, and parsing and sanitization code. The key idea behind hax is the pragmatic observation that different verification tools are better at handling different kinds of verification goals. Consequently, hax supports multiple proof backends, including domain-specific security analysis tools like ProVerif and SSProve, as well as general proof assistants like Coq and F*. In this paper, we present the hax toolchain and show how we use it to translate Rust code to the input languages of different provers. We describe how we systematically test our translated models and our models of the Rust system libraries to gain confidence in their correctness. Finally, we briefly overview various ongoing verification projects that rely on hax.

Ein Meilenstein für IT-Sicherheit in Deutschland - Cyberagentur

Cyberagentur unterzeichnet fünf Verträge für das Forschungsprogramm „Ökosystem vertrauenswürdige IT“ Die Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur) unterzeichnet am 20. Januar 2025 Aufträge mit fünf Unternehmen für das Forschungsprogramm „Ökosystem vertrauenswürdige IT“ (ÖvIT). Ziel ist die formale Verifikation nachweisbarer IT-Sicherheit und die Etablierung eines Netzwerks von Experten und Anwendern. „Die Cyberagentur hat mit […]

TLS Cipher Suite

Berlin Crypto December 2024

Where the Berlin Crypto Community gets together.

Berlin Crypto December 2024

Where the Berlin Crypto Community gets together.

Jobs at Cryspen | JOIN

Jobs at Cryspen. Browse all our open positions and become part of our growing team! We are currently looking for additions to our company. Apply today!

Taking Stock of Validation Checks

When implementing cryptographic protocols, probably the most important thing is to not forget validating all inputs. Failing to do so can lead to inadvertant leakage of private information, state corruption, impersonation attacks… all kinds of vulnerabilities. To give an example, you might remember the “goto fail” vulnerability, a bug in the TLS implementation used in iOS. Here, the verification function of signatures sent along with the ServerKeyExchange message, which ties the server identity to the transcript and ephemeral key material. Due to a hard-to-spot slipup, it returned success early and never really checked the signature, which would allow an attacker to man-in-the-middle the connection. While in this case they didn’t just forget to do the check, it does demonstrate why these checks are important.