Jasmin Compiler Preserves Cryptographic Security, Verified for 25 of 30 Front-End Passes

Cryptographic systems rely on complex code, and ensuring their security demands rigorous verification, a challenge that Santiago Arranz-Olmos, Gilles Barthe, and Lionel Blatter, from the Max Planck Institute for Software Systems, Germany, along with colleagues, now address with a significant advance in compiler technology. The team demonstrates that the Jasmin compiler, a framework for developing formally verified cryptographic implementations, preserves cryptographic security throughout its compilation process. This achievement extends beyond simple functional correctness, encompassing essential features like probabilistic computations, and establishes a new level of assurance for cryptographic code. By developing a tailored logic and a novel semantics for Jasmin programs, the researchers prove that the compiler maintains security properties, specifically indistinguishability under chosen ciphertext attack (IND-CCA), throughout its 25 compilation passes, representing a major step towards building truly trustworthy cryptographic systems.

Interaction Trees and Compiler Verification

Scientists are developing formal methods to verify compilers for probabilistic programming languages, establishing strong guarantees about program behavior even with randomness. Researchers leverage Interaction Trees (ITrees) as a semantic foundation and employ equivalence up-to-tau as a measure of compiler correctness, allowing for a modular verification process that separates proving compiler correctness from defining probabilistic semantics. Interaction Trees represent program behavior, particularly with side effects or non-deterministic elements, providing a structured way to analyze execution. Equivalence up-to-tau allows for abstraction, streamlining verification by considering programs equivalent if they behave similarly at a certain level of detail.

A Simulation Relation assesses whether a target system can mimic a source system, and Probabilistic Lifting extends this relation to work with distributions of states, crucial for probabilistic programs. The core argument centers on carefully selecting the semantic model and equivalence notion to achieve a strong compiler correctness guarantee for probabilistic programs. Theorems establish that the compiled program is equivalent to the original, independent of probabilistic semantics, and that if two ITrees are in simulation, the probability of observing certain states remains consistent after compilation. Researchers refined these theorems to address limitations in real-world compilers, considering the probability of sets of states rather than individual states to ensure accuracy. This approach provides rigorous verification for probabilistic programs, ensuring compiled programs behave as expected even with randomness. The modular verification process simplifies the task, and the refined theorem is practical and applicable to real-world compilers, offering strong guarantees about program behavior.

Jasmin Compiler Verification Using Relational Hoare Logics

Scientists developed a rigorous methodology to formally verify the security of cryptographic implementations, focusing on the Jasmin compiler, a framework for high-assurance, high-speed cryptography. This study pioneers a new approach to compiler verification by extending traditional techniques to accommodate probabilistic and potentially non-terminating computations, essential features in modern cryptography. Researchers constructed two Relational Hoare Logics (RHLs) specifically tailored for proving the correctness of the Jasmin compiler, building upon existing work while introducing specialized rules for common compiler patterns. These logics were rigorously proven sound with respect to a denotational semantics based on interaction trees, a framework for modeling program execution.

The team leveraged interaction trees to define a novel semantics for Jasmin programs, explicitly accounting for both infinite and probabilistic executions, critical for verifying post-quantum cryptographic schemes. This new semantics enabled scientists to lift the existing correctness theorem for the Jasmin compiler to encompass these complex behaviors, without modifying the compiler itself. The approach successfully verified the entire compiler front-end, spanning four intermediate languages, using a single, generic RHL implementation. Notably, the proofs required no explicit probabilistic reasoning due to the properties of interaction trees.

Scientists meticulously verified 25 out of 30 compiler passes, demonstrating the scalability and practicality of the methodology. The study establishes a formal link between the source code of cryptographic implementations and their assembly-level counterparts, addressing a critical gap in current security assurance practices. This work provides a robust foundation for deploying high-assurance cryptographic code in mainstream applications, mitigating the risk of attacks exploiting discrepancies between security proofs and actual implementations. The formalized proofs and the mechanized verification within the Rocq prover are provided as a complete artifact, ensuring reproducibility and facilitating further research in computer-aided cryptography.

Jasmin Compiler Passes Preserve Cryptographic Security

The Jasmin framework and compiler represent a significant advancement in the development of formally verified cryptographic implementations. Researchers have successfully enhanced the guarantees of the Jasmin compiler by demonstrating, within the Rocq prover, that 25 out of 30 of its front-end passes preserve cryptographic security. This achievement builds upon the compiler’s existing functional correctness, extending it to encompass nonterminating and probabilistic computations, which are essential for modern cryptography. The work centers on a novel Relational Hoare Logic tailored for compiler correctness proofs, and its soundness has been rigorously established with respect to a new denotational semantics of Jasmin programs based on interaction trees.

These interaction trees provide a modular and coinductive reasoning style, simplifying the process of verifying complex computations. The team formalized cryptographic security, specifically focusing on Indistinguishability under Chosen-Ciphertext Attack (IND-CCA), using interaction trees and proved that the Jasmin compiler preserves this crucial security property. The researchers developed a semantic framework based on interaction trees, a coinductive type parameterized by event families and result types. The core semantics of Jasmin commands are defined through a series of translation rules, demonstrating how each command maps to an interaction tree.

For example, the semantics of a variable assignment translates to evaluating an expression and then assigning the resulting value to a location. The team also introduced a generalization of heterogeneous equivalence to support error handling through a “cutoff” event, allowing the relation to hold trivially from that point onward. This allows for relating ITrees that depend on distinct return types and event families. These advancements collectively deliver a robust and formally verified foundation for building secure cryptographic systems.

Compiler Front-End Preserves Cryptographic Security

The Jasmin framework and its compiler represent a significant advance in the development of formally verified cryptographic implementations. Researchers have extended the guarantees of the Jasmin compiler by demonstrating, using the Rocq prover, that the front-end of the compiler preserves cryptographic security. This achievement builds upon existing work establishing the compiler’s functional correctness and addresses a key limitation by extending these guarantees to computations involving interactive and probabilistic elements, essential for modern cryptography. The team accomplished this by first developing a new relational Hoare logic specifically tailored for proving compiler correctness, and then using this logic to formally verify that the compiler’s front-end maintains cryptographic security, specifically indistinguishability under chosen ciphertext attack (IND-CCA).

This verification relies on a novel use of interaction trees, a framework for reasoning about interactive computations, which allows for a modular and compositional approach to proving security properties. The researchers have made a modified version of the Jasmin compiler, incorporating these new proofs, publicly available. The authors acknowledge that their formalization currently covers only the front-end of the Jasmin compiler, leaving the back-end for future work.