{"id":1140982,"date":"2025-06-10T09:00:00","date_gmt":"2025-06-10T16:00:00","guid":{"rendered":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library\/"},"modified":"2025-06-18T03:06:37","modified_gmt":"2025-06-18T10:06:37","slug":"rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library","status":"publish","type":"post","link":"https:\/\/www.microsoft.com\/en-us\/research\/blog\/rewriting-symcrypt-in-rust-to-modernize-microsofts-cryptographic-library\/","title":{"rendered":"Rewriting SymCrypt in Rust to modernize Microsoft\u2019s cryptographic library\u00a0"},"content":{"rendered":"\n
\"Three<\/figure>\n\n\n\n

Outdated coding practices and memory-unsafe languages like C are putting software, including cryptographic libraries, at risk. Fortunately, memory-safe languages like Rust, along with formal verification tools, are now mature enough to be used at scale, helping prevent issues like crashes, data corruption, flawed implementation, and side-channel attacks.<\/p>\n\n\n\n

To address these vulnerabilities and improve memory safety, we\u2019re rewriting SymCrypt (opens in new tab)<\/span><\/a>\u2014Microsoft\u2019s open-source cryptographic library\u2014in Rust. We\u2019re also incorporating formal verification methods. SymCrypt is used in Windows, Azure Linux, Xbox, and other platforms.<\/p>\n\n\n\n

Currently, SymCrypt is primarily written in cross-platform C, with limited use of hardware-specific optimizations through intrinsics (compiler-provided low-level functions) and assembly language (direct processor instructions). It provides a wide range of algorithms, including AES-GCM, SHA, ECDSA, and the more recent post-quantum algorithms ML-KEM and ML-DSA. <\/p>\n\n\n\n

Formal verification will confirm that implementations behave as intended and don\u2019t deviate from algorithm specifications, critical for preventing attacks. We\u2019ll also analyze compiled code to detect side-channel leaks caused by timing or hardware-level behavior.<\/p>\n\n\n\n

Proving Rust program properties with Aeneas<\/h2>\n\n\n\n

Program verification is the process of proving that a piece of code will always satisfy a given property, no matter the input. Rust\u2019s type system profoundly improves the prospects for program verification by providing strong ownership guarantees, by construction, using a discipline known as \u201caliasing xor mutability\u201d.<\/p>\n\n\n\n

For example, reasoning about C code often requires proving that two non-const pointers are live and non-overlapping, a property that can depend on external client code. In contrast, Rust\u2019s type system guarantees this property for any two mutably borrowed references.<\/p>\n\n\n\n

As a result, new tools have emerged specifically for verifying Rust code. We chose Aeneas (opens in new tab)<\/span><\/a> because it helps provide a clean separation between code and proofs.<\/p>\n\n\n\n

Developed by Microsoft Azure Research in partnership with Inria, the French National Institute for Research in Digital Science and Technology, Aeneas connects to proof assistants like Lean (opens in new tab)<\/span><\/a>, allowing us to draw on a large body of mathematical proofs\u2014especially valuable given the mathematical nature of cryptographic algorithms\u2014and benefit from Lean\u2019s active user community.<\/p>\n\n\n\n

Compiling Rust to C supports backward compatibility  <\/h2>\n\n\n\n

We recognize that switching to Rust isn\u2019t feasible for all use cases, so we\u2019ll continue to support, extend, and certify C-based APIs as long as users need them. Users won\u2019t see any changes, as Rust runs underneath the existing C APIs.<\/p>\n\n\n\n

Some users compile our C code directly and may rely on specific toolchains or compiler features that complicate the adoption of Rust code. To address this, we will use Eurydice (opens in new tab)<\/span><\/a>, a Rust-to-C compiler developed by Microsoft Azure Research, to replace handwritten C code with C generated from formally verified Rust. Eurydice (opens in new tab)<\/span><\/a> compiles directly from Rust\u2019s MIR intermediate language, and the resulting C code will be checked into the SymCrypt repository alongside the original Rust source code.<\/p>\n\n\n\n

As more users adopt Rust, we’ll continue supporting this compilation path for those who build SymCrypt from source code but aren\u2019t ready to use the Rust compiler. In the long term, we hope to transition users to either use precompiled SymCrypt binaries (via C or Rust APIs), or compile from source code in Rust, at which point the Rust-to-C compilation path will no longer be needed.<\/p>\n\n\n\n\t

\n\t\t\n\n\t\t

\n\t\tPODCAST SERIES<\/span>\n\t<\/p>\n\t\n\t

\n\t\t\t\t\t\t
\n\t\t\t\t\n\t\t\t\t\t\"Illustrated\n\t\t\t\t<\/a>\n\t\t\t<\/div>\n\t\t\t\n\t\t\t
\n\n\t\t\t\t\t\t\t\t\t

The AI Revolution in Medicine, Revisited<\/h2>\n\t\t\t\t\n\t\t\t\t\t\t\t\t

Join Microsoft\u2019s Peter Lee on a journey to discover how AI is impacting healthcare and what it means for the future of medicine.<\/p>\n\t\t\t\t\n\t\t\t\t\t\t\t\t

\n\t\t\t\t\t
\n\t\t\t\t\t\t\n\t\t\t\t\t\t\tListen now\t\t\t\t\t\t<\/a>\n\t\t\t\t\t<\/div>\n\t\t\t\t<\/div>\n\t\t\t\t\t\t\t<\/div>\n\t<\/div>\n\t<\/div>\n\t\n\n\n

Timing analysis with Revizor <\/h2>\n\n\n\n

Even software that has been verified for functional correctness can remain vulnerable to low-level security threats, such as side channels caused by timing leaks or speculative execution. These threats operate at the hardware level and can leak private information, such as memory load addresses, branch targets, or division operands, even when the source code is provably correct. <\/p>\n\n\n\n

To address this, we\u2019re extending Revizor (opens in new tab)<\/span><\/a>, a tool developed by Microsoft Azure Research, to more effectively analyze SymCrypt binaries. Revizor models microarchitectural leakage and uses fuzzing techniques to systematically uncover instructions that may expose private information through known hardware-level effects.  <\/p>\n\n\n\n

Earlier cryptographic libraries relied on constant-time programming to avoid operations on secret data. However, recent research has shown that this alone is insufficient with today\u2019s CPUs, where every new optimization may open a new side channel.\u00a0<\/p>\n\n\n\n

By analyzing binary code for specific compilers and platforms, our extended Revizor tool enables deeper scrutiny of vulnerabilities that aren\u2019t visible in the source code.<\/p>\n\n\n\n

Verified Rust implementations begin with ML-KEM<\/h2>\n\n\n\n

This long-term effort is in alignment with the Microsoft Secure Future Initiative<\/a> and brings together experts across Microsoft, building on decades of Microsoft Research investment in program verification and security tooling.<\/p>\n\n\n\n

A preliminary version of ML-KEM in Rust is now available on the preview feature\/verifiedcrypto (opens in new tab)<\/span><\/a> branch of the SymCrypt repository. We encourage users to try the Rust build and share feedback (opens in new tab)<\/span><\/a>. Looking ahead, we plan to support direct use of the same cryptographic library in Rust without requiring C bindings. <\/p>\n\n\n\n

Over the coming months, we plan to rewrite, verify, and ship several algorithms in Rust as part of SymCrypt. As our investment in Rust deepens, we expect to gain new insights into how to best leverage the language for high-assurance cryptographic implementations with low-level optimizations. <\/p>\n\n\n\n

As performance is key to scalability and sustainability, we\u2019re holding new implementations to a high bar using our benchmarking tools to match or exceed existing systems.<\/p>\n\n\n\n

Looking forward <\/h2>\n\n\n\n

This is a pivotal moment for high-assurance software. Microsoft\u2019s investment in Rust and formal verification presents a rare opportunity to advance one of our key libraries. We\u2019re excited to scale this work and ultimately deliver an industrial-grade, Rust-based, FIPS-certified cryptographic library.<\/p>\n","protected":false},"excerpt":{"rendered":"

We’re rewriting parts of Microsoft’s SymCrypt cryptographic library in Rust to improve memory safety and defend against side-channel attacks, enabling formal verification while maintaining backward compatibility via a Rust-to-C compiler.<\/p>\n","protected":false},"author":43868,"featured_media":1141377,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"msr-url-field":"","msr-podcast-episode":"","msrModifiedDate":"","msrModifiedDateEnabled":false,"ep_exclude_from_search":false,"_classifai_error":"","msr-author-ordering":[{"type":"user_nicename","value":"Jonathan Protzenko","user_id":"33286"},{"type":"user_nicename","value":"Samuel Lee","user_id":"43893"},{"type":"user_nicename","value":"Samreen Khadeer","user_id":"43894"},{"type":"user_nicename","value":"Son Ho","user_id":"43830"},{"type":"user_nicename","value":"Oleksii Oleksenko","user_id":"43146"},{"type":"user_nicename","value":"Michael Naehrig","user_id":"32976"},{"type":"user_nicename","value":"C\u00e9dric Fournet","user_id":"31819"}],"msr_hide_image_in_river":null,"footnotes":""},"categories":[1],"tags":[],"research-area":[13558],"msr-region":[],"msr-event-type":[],"msr-locale":[268875],"msr-post-option":[269148,243984,269142],"msr-impact-theme":[],"msr-promo-type":[],"msr-podcast-series":[],"class_list":["post-1140982","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-research-blog","msr-research-area-security-privacy-cryptography","msr-locale-en_us","msr-post-option-approved-for-river","msr-post-option-blog-homepage-featured","msr-post-option-include-in-river"],"msr_event_details":{"start":"","end":"","location":""},"podcast_url":"","podcast_episode":"","msr_research_lab":[],"msr_impact_theme":[],"related-publications":[],"related-downloads":[],"related-videos":[],"related-academic-programs":[],"related-groups":[],"related-projects":[],"related-events":[],"related-researchers":[{"type":"user_nicename","value":"Samuel Lee","user_id":43893,"display_name":"Samuel Lee","author_link":"Samuel Lee<\/a>","is_active":false,"last_first":"Lee, Samuel","people_section":0,"alias":"saml"},{"type":"user_nicename","value":"Samreen Khadeer","user_id":43894,"display_name":"Samreen Khadeer","author_link":"Samreen Khadeer<\/a>","is_active":false,"last_first":"Khadeer, Samreen","people_section":0,"alias":"skhadeer"},{"type":"user_nicename","value":"Son Ho","user_id":43830,"display_name":"Son Ho","author_link":"Son Ho<\/a>","is_active":false,"last_first":"Ho, Son","people_section":0,"alias":"t-sonho"},{"type":"user_nicename","value":"Oleksii Oleksenko","user_id":43146,"display_name":"Oleksii Oleksenko","author_link":"Oleksii Oleksenko<\/a>","is_active":false,"last_first":"Oleksenko, Oleksii","people_section":0,"alias":"ololeksenko"},{"type":"user_nicename","value":"Michael Naehrig","user_id":32976,"display_name":"Michael Naehrig","author_link":"Michael Naehrig<\/a>","is_active":false,"last_first":"Naehrig, Michael","people_section":0,"alias":"mnaehrig"},{"type":"user_nicename","value":"C\u00e9dric Fournet","user_id":31819,"display_name":"C\u00e9dric Fournet","author_link":"C\u00e9dric Fournet<\/a>","is_active":false,"last_first":"Fournet, C\u00e9dric","people_section":0,"alias":"fournet"}],"msr_type":"Post","featured_image_thumbnail":"\"Three","byline":"","formattedDate":"June 10, 2025","formattedExcerpt":"We're rewriting parts of Microsoft's SymCrypt cryptographic library in Rust to improve memory safety and defend against side-channel attacks, enabling formal verification while maintaining backward compatibility via a Rust-to-C compiler.","locale":{"slug":"en_us","name":"English","native":"","english":"English"},"_links":{"self":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/1140982","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/users\/43868"}],"replies":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/comments?post=1140982"}],"version-history":[{"count":13,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/1140982\/revisions"}],"predecessor-version":[{"id":1141637,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/posts\/1140982\/revisions\/1141637"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media\/1141377"}],"wp:attachment":[{"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/media?parent=1140982"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/categories?post=1140982"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/tags?post=1140982"},{"taxonomy":"msr-research-area","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/research-area?post=1140982"},{"taxonomy":"msr-region","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-region?post=1140982"},{"taxonomy":"msr-event-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-event-type?post=1140982"},{"taxonomy":"msr-locale","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-locale?post=1140982"},{"taxonomy":"msr-post-option","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-post-option?post=1140982"},{"taxonomy":"msr-impact-theme","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-impact-theme?post=1140982"},{"taxonomy":"msr-promo-type","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-promo-type?post=1140982"},{"taxonomy":"msr-podcast-series","embeddable":true,"href":"https:\/\/www.microsoft.com\/en-us\/research\/wp-json\/wp\/v2\/msr-podcast-series?post=1140982"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}