Proof-based general-purpose computing with Magnetar

At a glance A new form of computing . Zero-knowledge proofs let you run a workload and receive, alongside the result, a short proof that the program ran correctly. Anyone can check the proof in milliseconds, without rerunning the program, without trusting whoever ran it, and without needing data on which the program was run. Three grand challenges have stood in the way of broad adoption : making proofs fast enough to produce, making them available to normal programs without cryptographic expertise, and resting them on cryptography that will still be trusted many decades from now. Magnetar makes major progress on all three challenges. It proves programs written in Rust, Go, or C, runs 10 to 39 times faster on average than the prior fastest comparable systems, and rests its security only on standard hash functions. It is the latest result of more than a decade of research at Microsoft Research on making zero-knowledge proofs practical. A new form of computing Every result a computer produces comes with an implicit question: did the program run as claimed and produce correct outputs? Today, answering that question often requires a degree of trust alongside verification. We trust the operator, the vendor, the counterparty, or the agent, and we rely on contracts, audits, and logs to establish that trust. Zero-knowledge proofs offer a fundamentally different approach to establishing trust. A program runs, and along with its output it produces a short proof, a cryptographic certificate that this program, on these inputs, produced this output. The proof is small and fast to check. Whoever receives it can confirm the result in milliseconds without rerunning the program, and can pass the proof on to anyone else who needs the same assurance. With the zero-knowledge property, the proof also reveals nothing about inputs that should stay private. This changes what correctness means in the real world. A result no longer has to be trusted because of who produced it. It can be checked because of what accompanies it. An AI agent acting on someone’s behalf could attach a proof that each action complied with the policy it was given. Regulated financial institutions could prove that transactions were processed correctly without making their transactions public. These become possible once producing a proof is as routine as running the program. Three grand challenges Zero-knowledge proofs were invented in the 1980s, and the ideas behind proving program execution have been around nearly as long. What has kept them from becoming a general tool is three challenges that have resisted being solved at the same time. Efficiency . Producing a proof has historically taken millions of times more computation than running the program itself. Years of research have brought that overhead down, but the fastest systems have achieved their speed by making compromises elsewhere. Generality and usability. Many proof systems require developers to manually rewrite their program as a cryptographic circuit, which is a fixed arithmetic description of that exact computation. This takes months. Every change to the application means a new circuit, and the translation is itself a frequent source of security bugs. A general-purpose alternative is to prove the execution of an ordinary processor, so that any compiled program can be proven as written. Until recently, that generality came at a steep cost in speed or security. Security. A proof is only as strong as the cryptography beneath it. Many proof systems rest on elliptic curves, which can be broken by a sufficiently powerful quantum computer. Microsoft is addressing this problem with its Quantum Safe Program, which will move its products and services to post-quantum cryptography, a goal it recently accelerated to 2029 . Post-quantum proof systems already exist, but some rest on lattice assumptions, and most rest on new cryptographic functions invented to reduce the cost of proving. These new cryptographic functions have not faced the decades of scrutiny given to the cryptography protecting today’s internet, and some rest on mathematical conjectures about error-correcting codes that have not been proven. They have bought their speed with strong assumptions. Foundry Labs Foundry Labs bridges the distance between Microsoft breakthroughs and the builders, scientists, and curious minds who can put them to work. Foundry Labs Opens in a new tab More than a decade of work For more than a decade, Microsoft Research has worked on making zero-knowledge proofs and verifiable computing practical. Early research followed two approaches, both practical only for small programs. The first (opens in new tab) (opens in new tab) lets a verifier check a long computation through a short conversation with the prover using a technique called the sum-check protocol (opens in new tab) , but this applied only to computations with a particular layered structure. The second (opens in new tab) (opens in new tab) used elliptic-curve cryptography to create very small proofs for almost any computation. But this requires a one-time trusted setup involving secret information which, if leaked, could allow anyone to forge proofs. This approach is also vulnerable to quantum computers. In 2019, a new zero-knowledge proof system called Spartan returned to the sum-check approach and made it work for general-purpose programs without a trusted setup. Spartan can also be instantiated with different cryptographic building blocks. That flexibility is what later allowed the proof system to be built on hash functions alone. A sequence of results then filled in the remaining pieces: Phalanx (opens in new tab) , in 2021, showed how to exploit repetition, such as a processor running the same instruction cycle on every step, to prove computations an order of magnitude faster than Spartan. Magnetar’s processor description is built on this idea. Nova (opens in new tab) , HyperNova (opens in new tab) , NeutronNova (opens in new tab) , Neo and SuperNeo (opens in new tab) showed that stopping Spartan’s proving early, and folding the partial results together, makes it practical to prove computations of any size at far lower cost. Brakedown (opens in new tab) , in 2021, introduced a fast hash-based commitment scheme and combined it with Spartan, giving the first Spartan variant whose security rests on standard hash functions. Spice (opens in new tab) , Lasso (opens in new tab) , Nebula (opens in new tab) , and then Twist and Shout (opens in new tab) made the memory operations at the heart of a general-purpose processor inexpensive to prove, and Jolt (opens in new tab) showed that combining them with Spartan can efficiently prove the execution of a complete processor. Earlier this year, Vega (opens in new tab) applied this line of work to digital identity, proving facts from a government credential in under a tenth of a second . More recently, BinarySpartan (opens in new tab) brought Spartan to binary fields, where a processor’s logic and standard hash functions can be efficiently expressed. BinarySpartan also relies on Ligerito (opens in new tab) , a Brakedown-style commitment scheme with much shorter proofs, and on ring switching (opens in new tab) , which makes it efficient to commit to vectors of bits. Each of these solved a piece of the problem. Magnetar is where the pieces come together. Magnetar Magnetar is a zero-knowledge virtual machine, or zkVM, and it makes major progress on all three challenges at once. It is general-purpose. Magnetar proves the execution of RISC-V, an open processor architecture with mature compilers for every mainstream language. A developer writes a program in Rust, Go, or C, compiles it as usual, and Magnetar proves it as written. Consider what this means in practice. A business policy, a data pipeline, or an interpreter for the Ethereum Virtual Machine (EVM) is just a program, and the engineers who already maintain it can prove their executions exactly as written. As a r