This post aims to further explore how to enable function privacy (FP) property in RMs and how to connect the RM design needs with the proving system affordances.
Ideal properties
Ideally, we are looking for a way to make function privacy a feature that is:
- modular. It can be turned on and off by choosing the correct primitives for the correct functions but the application logic doesn’t have to be aware of the way FP is realised, only about the guarantees it gives (in order to be able to built on these guarantees).[1]
- efficient. Having function privacy requires more computations, but these computations should be minimal (optimising for overhead reduction).
- free of side-effects. The adjustments required to enable FP shouldn’t make the data-privacy-only case significantly more expensive. The ideal model is that enabling function privacy adds some computations that are directly related to FP, but when FP is not used, it is equivalent to never having FP.
General intended approach
The general idea is to use recursion for FP.
Verifying proofs generally requires something called a verifying key, which is a succinct representation of the circuit being evaluated. Simply put, to verify a proof attesting to the correct evaluation of the circuit, we need to know the circuit.
In the data-privacy-only case, we can ensure that the logic is satisfied by proving the corresponding circuit (we are assuming a 1-1 correspondence between logics and circuits. Often we use the terms interchangeably.). Since we need a circuit to verify such a proof, it means the verifier knows the circuit = knows the logic = knows the application - no FP.
To allow FP, the general idea is to use recursion, meaning that:
- the prover proves two statements for each logic:
- the logic circuit proof, like in the data-privacy-only case
- the outer circuit proof. This circuit runs a verifier code, attesting to the correctness of the first proof
- the verifier only verifies the outer circuit proof (and the first proof is verified inside the outer proof)
Since the outer circuit performs the same functionality - given a proof and its public inputs, verifies the proof, the verifier doesn’t get access to the logic circuit, and therefore doesn’t know what application is being used = function privacy.
Other approaches to achieve FP (e.g., for zkVMs) are pretty much isomorphic to this one, with other elements taking the role of the outer circuit, inner circuit, and inputs, and so I’m not gonna mention this difference in this post.
Implementing FP, high level
Implementing FP requires a few steps:
- adjusting RM interfaces to be FP-friendly, which includes:
- including the required checks in the compliance circuit
- adjusting the relevant field types to be able to accommodate both FP and DP-only cases
- implement the outer circuit that runs the verifier
- this part is quite efficiency-sensitive (more so than other types of statements) since within the context of a single proving system, there is a trade-off between prover efficiency, verifier efficiency, and proof size, which is highly relevant for recursion.
Current state
We do not have FP right now, but we want to have it in the future. And while the second step of implementing FP is rather practical, the first step is a point of research we can deal with now, and this is also the step where we ensure modularity and having no side-effects for the DP-only case.
Current implementation vs intended design
In this PR, we discovered another conflict between how things are done now and how we imagined things to work in the future.
- Verifying keys for circuits are large and we don’t want to process them in circuits, so we hash them and verify that the hash is computed correctly from the verifying key out of circuit. This approach only works in the DP-only case.
- The current RM spec approach for FP implies that we perform this check in the compliance circuit (for both FP and non-FP cases), that contains all the mandatory checks for RM, which conflicts with how things are done now, since the check from 1. is done out of circuit.
- One way to tackle this would be to perform this check in the outer FP circuit, which is only relevant in the FP case. Therefore if the outer circuit is checked (FP), the hash is verified in circuit, and if the outer circuit is not checked (DP-only), the outer hash has to be verified out of circuit.
This would require the following:
- the hash of the verified circuit must be checked out of circuit at all times. In FP case, this will be the outer circuit hash check.
- standardize the outer circuit constraints, including the relevant hash check, and enforce this specific circuit to be used for the FP case.
The second part can be a bit difficult to do since we can’t “enforce” it. The user is incentivised to use the proposed circuit, but what to do with malicious third parties that use the “wrong” FP circuit instead? Since RM shouldn’t really differentiate between FP and DP-only cases, it is hard to check. One way I see to resolve this is to include a VK check somewhere, so that when the user is “offered” or chooses FP option, the VK of the outer circuit is checked against the VK of the circuit offered by the RM implementation.
What could be this “somewhere”?
- It could be a logic of some FP-associated utility application. The good thing about logics is that they have to verify upon execution. The challenge is how to bind the input VK we would verify to the VK of the FP circuit since logics don’t naturally take such inputs. Can we even enforce this?
- It could be a part of the executor, which would imply that we assume that a fully shielded RM comes with a prescribed FP circuit. In that case, the executor would have to find the “official” vk and verify it against the given vk. The executor would also have to be aware of when FP is used and when it isn’t.
knowing what primitives to use != knowing how FP is realised. The application doesn’t have to understand why something works. ↩︎