Verifiable computing in julia

An upcoming field is verifiable computing. The typical topic is that you provide a proof that you have run a program with an input which resulted in a particular output. Even without revealing the input. E.g.

f(x::BigInt, y::BigInt) = x * y

Given an output n, some big integer, you can evaluate f and supply a proof that your output is n, without revealing the two factors x and y. The techniques are known as zkSNARK or STARK and other fancy words.

Software like Risc Zero (https://risczero.com/) and Nexus (https://nexus.xyz/) can achieve this. The typical method is to emulate a simple cpu (a RISCV or something else fairly simple). The program is compiled to this architecture, and run in an emulator to obtain an execution trace. Then one uses some cryptology magic and deliver a proof which can be checked by anyone.

The typical software is written in rust, or in C.

It occured to me that julia might be suitable for such stuff since parts of the compiler is written in julia, and one may meddle with the compiler with packages like Cassette.jl. So one might construct an execution trace with the necessary constraints without going all the way down to assembly level.

Are anybody aware of efforts to do such things in julia? E.g. by supporting constraints for a subset of intrinsics, or possibly at a higher level?

2 Likes

Iā€™m not really sure this is the same thing as Iā€™m not very familiar with the domain, but is this similar to GitHub - hpsc-lab/SecureArithmetic.jl: Secure arithmetic operations using fully homomorphic encryption, which was presented at JuliaCon24 by @sloede? But this is using an external C++ library, not using compiler hacking techniques youā€™re suggesting.

4 Likes

Thanks for pinging me. The topic of our talk was fully homomorphic encryption (FHE), which allows one to do computations on encrypted data without knowing the data itself. It seems to me that FHE may be a component of verifiable computing, covering the ā€œprocess data without knowing the data itselfā€ part. There is still something missing for the verification part, though.

If thereā€™s anything we can contribute from the FHE side (with our limited knowledge, since weā€™re not really cryptographers), please let us know - it might be fun!

3 Likes

Yes. One method is to reduce the problem to proving that one has a polynomial with certain zeros, and homomorphic encryption is an ingredient. Hereā€™s a somewhat old layman intro. [1906.07221] Why and How zk-SNARK Works

Hereā€™s another approach. Anatomy of a STARK, Part 0: Introduction | Anatomy of a STARK

1 Like

This all look intriguing, e.g. that thereā€™s a virtual machine for this (see Risc Zero link), zkVM, just unclear how slow this is, for arbitrary Rust code, unclear to me itā€™s based on RISC-V, but suppose youā€™re right the VM emulated it).

I knew of zero-knowledge proofs, but not zk-SNARK, or STARK (seemingly what to concentrate on), apparently building of them, and both seemingly related to ā€œverifiable computingā€ you pointed to, though not exactly the same.

Itā€™s 65 pages, but donā€™t worry, seems readable, and intriguing (e.g. what I put in bold):

While initially planned as short, the work now spans several dozens of pages, nevertheless it requires very little pre-requisite knowledge, and one can freely skip familiar parts.
[ā€¦]
Zero-knowledge succinct non-interactive arguments of knowledge (zk-SNARK) is the truly ingenious method of proving that something is true without revealing any other information, however, why it is useful in the ļ¬rst place?

Zero-knowledge proofs are advantageous in a myriad of application, including:
ā€¢ Proving statement on private data:
ā€“ Person A has more than X in his bank account
ā€“ In the last year, a bank did not transact with an entity Y
ā€“ Matching DNA without revealing full DNA
ā€“ One has a credit score higher than Z
ā€¢ Anonymous authorization:
ā€“ Proving that requester R has right to access web-siteā€™s restricted area without revealing its identity (e.g., login, password)
ā€“ Prove that one is from the list of allowed countries/states without revealing from which one exactly
ā€“ Prove that one owns a monthly pass to a subway/metro without revealing cardā€™s id
ā€¢ Anonymous payments:
ā€“ Payment with full detachment from any kind of identity
ā€“ Paying taxes without revealing oneā€™s earnings [ā€¦]

And:

Zk-SNARKs have existed for a while, but the STARK proof system is a relatively new thing. It stands out for several reasons:

  • While traditional zk-SNARKs rely on cutting-edge cryptographic hard problems and assumptions, the only cryptographic ingredient in a STARK proof system is a collision-resistant hash function. As a result, the proof system is provably post-quantum under an idealized model of the hash function 1.

image

In part 6: Speeding things up:

The Number Theoretic Transform and its Applications

The Fast Fourier Transform

The Number Theoretic Transform (NTT) is a powerful mathematical tool that has become increasingly important in developing Post Quantum Cryptography (PQC) and Homomorphic Encryption (HE). Its ability to efficiently calculate polynomial multiplication using the convolution theorem with a quasi-linear complexity O(N log n) instead of O(n^2) when implemented with Fast Fourier Transform-style algorithms has made it a key component in modern cryptography. FFT-style NTT algorithm or fast-NTT is particularly useful in lattice-based cryptography. In this short note, we briefly introduce the basic concepts of linear, cyclic, and negacyclic convolutions via traditional schoolbook algorithms, traditional NTT, its inverse (INTT), and FFT-like versions of NTT/INTT. We then provide consistent toy examples through different concepts and algorithms to understand the basics of NTT concepts.

While ā€œBeginners Guideā€, not surprisingly a bit math-heavy, assuming some number-theoretic backgroundā€¦:

Example 3.1. In a ring Z7681 and n = 4, the 4-th root of unity which satisfy the condition Ļ‰4 ā‰” 1 mod 7681 are {3383, 4298, 7680}.

They donā€™t do float, for instance. And even if the emulator might be reasonably fast, the proof generation isnā€™t particularly fast, as this comment reveals:

In the simplest approach, the guest program would simply hash the whole Whereā€™s Waldo image in memory, then perform the crop and mask operations to cut out Waldo on that image. It would commit the image hash and the cut out image to the journal. Unfortunately, hashing the whole image, which we expect to be rather large, is cost prohibitive in the guest.
risc0/examples/waldo at main Ā· risc0/risc0 Ā· GitHub

Of course, if hashing an image is prohibitively costly, itā€™s a bit limited what you can do.