Proof-Carrying Code for Verifying Smart Contracts
How are smart contracts being verified nowadays?
Generally, smart contracts are stored on the blockchain and the executing party must inspect their source code before executing them. If there are N parties that want to execute the source code, all of them should verify it with the consequent replication of effort: in other words, the burden of proof is being displaced from the smart contract developer to the executing parties.
To prevent that all the N executers must verify the source code by themselves, there are two approaches:
- Usually, an independent expert is hired to read the source code with great attention to detail and check it against a list of common anti-patterns and errors.
- Rarely, formal verification tools are used to prove the correctness of the smart contract.
In both cases, the party executing the smart contract must trust that the verification step was done correctly: except that in a malicious setting, there could be bugs intentionally concealed to steal from an unsuspecting executing party, or the auditory process could have been negligent. Thus, wary executers still need to check the correctness of the smart code for themselves.
How could Proof-Carrying Code improve the current state of affairs?
Proof-Carrying Code (PCC) is really advantageous in this setting: using specialized PCC tools for formal verification, the generated proofs are attached to the smart contract and the executing party automatically checks them before running the smart contract.
Additionally, third parties could supplement formal specifications and smart contracts must comply with them to be formally certified: for example, a regulator could formally express that transactions greater than a given amount must be notified to a trusted service, and smart contracts could be proven correct against said formal regulation.
Let’s review an easy illustrative case of the formal verification of a smart contract using Proof-Carrying Code:
- Annotate the code with verification statements:
public class HardCapICO {
/*@ public invariant sumProceeds>=0 @*/
private int sumProceeds;
private int[] contributionByParty = new int[5000];
//@requires 0 <= maxParties && maxParties < 5000 && sumProceeds < 777777
//@ensures sumProceeds <=((n*(n+1))/2) + \old(sumProceeds)
public int getCumulativeContributions (int maxParties) {
int i = 0;
/*@ loop_invariant 0 < i && i <= (maxParties + 1) &&
@ 0 <= n && n < 5000 && \old(maxParties) == maxParties &&
@ 0 <= \old(sumProceeds) && \old(sumProceeds) <= 777777 &&
@ 0 <= sumProceeds && sumProceeds <= \old(sumProceeds) + (((i-1)*i)/2)
@*/
for (i = 1; i <= maxParties; i++)
sumProceeds += contributionByParty[i];
return sumProceeds;
}
public void setContribution (int party, int contribution)
{
contributionByParty[party] = contribution;
}
}
Note the pre-conditions and post-conditions of the method getCumulativeContributions and the loop invariant where all the variables are bounded.
- Compile the code to obtain its bytecode, while keeping and translating the verification statements:
/*@
@ requires 0 <= maxParties && maxParties < 5000 && sumProceeds < 777777
@ modifies \everything
@ ensures sumProceeds <=((n*(n+1))/2) + \old(sumProceeds)
@*/
public int getCumulativeContributions(int);
0: iconst_0
1: istore_2
2: iconst_1
3: istore_2
/*@
@ loop_specification
@ loop_inv 0 < i && i <= (maxParties + 1) && 0 <= n && n < 5000 && \old(maxParties) == maxParties &&
@ 0 <= \old(sumProceeds) && \old(sumProceeds) <= 777777 && 0 <= sumProceeds &&
@ sumProceeds <= \old(sumProceeds) + (((i-1)*i)/2)
@ decreases 1
@*/
4: iload_2
5: iload_1
6: if_icmpgt #30
9: aload_0
10: dup
11: getfield // HardCapICO.sumProceeds I (3)
14: aload_0
15: getfield // HardCapICO.contributionByParty:[I] (2)
18: iload_2
19: iaload
20: iadd
21: putfield // HardCapICO.sumProceeds I (3)
24: iinc %2 1
27: goto #4
30: aload_0
31: getfield // HardCapICO.sumProceeds I (3)
34: ireturn
Note that the pre-conditions, post-conditions, and loop invariants have been maintained.
- Generate Verification Conditions from the bytecode and the verification statements:
Definition mk_assert0:=
fun (_pre_heap: Heap.t)
(_pre_lv1n: Int.t) (heapref: Heap.t) (thisVal: value) (lv1n: Int.t) (lv_2i: Int.t) =>
((IsTrue (leBool
lv_2i
(Int.add
lv1n
(Int.const (1))))) /\
(IsTrue (leBool
(Int.const (0))
(value2int (do_hget _pre_heap
(Heap.Dynamic_Field thisVal HardCapICOSignature.sumProceedsFieldSignature))))) /\
(IsTrue (leBool
(value2int (do_hget
_pre_heap
(Heap.Dynamic_Field thisVal HardCapICOSignature.sumProceedsFieldSignature)))
(Int.const (5000)))) /\
(IsTrue (leBool
(Int.const (0))
(value2int (do_hget
heapref
(Heap.Dynamic_Field thisVal HardCapICOSignature.sumProceedsFieldSignature))))) /\
(IsTrue (leBool
(value2int (do_hget
heapref
(Heap.Dynamic_Field thisVal HardCapICOSignature.sumProceedsFieldSignature)))
(Int.add
(value2int (do_hget
_pre_heap
(Heap.Dynamic_Field this HardCapICOSignature.sumProceedsFieldSignature)))
(Int.div (Int.mul (Int.sub lv_2i (Int.const (1))) lv_2i) (Int.const (2)))))) /\
(IsTrue (leBool (Int.const (0)) lv1n)) /\
(IsTrue (ltBool lv1n (Int.const (5000)))) /\
(IsTrue (ltBool (Int.const (0)) lv_2i)) /\
(IsTrue (eq_bool _pre_lv1n lv1n))).
This is one of the Coq assertions in the annotations file which contains the pre-conditions, post-conditions and all asserts inside of the class methods.
- Complete the formal proofs of the generated verification conditions
Lemma equation : forall i, (i+1-1)*(i+1)/2 = (i-1)*i/2 + i.
intros.
transitivity (((i-1)*i+i*2)/2).
f_equal.
ring.
apply Z_div_plus.
trivial with zarith.
Qed.
Lemma fullProof :
(HardCapICOSignature.getCumulativeContributionsT_int HardCapICO.getCumulativeContributionsT_int
HardCapICOAnnotations.getCumulativeContributionsT_int.spec).
Proof.
prettyfy.
Set Printing Coercions.
zedifyh n_lt_small; try zedifyg; try omega.
zedifyh zero_le_sum; try zedifyg; try omega.
zedifyh zero_le_n; try zedifyg; try omega.
zedifyh zero_lt_i; try zedifyg; try omega.
zedifyh i_le_n_plus_1; try zedifyg; try omega.
zedifyh zero_le_oldsum; try zedifyg; try omega.
zedifyh oldsum_le_small; try zedifyg; try omega.
...
apply H0 in H.
clear H0 H1.
rename H into zero_le_sum.
zedifyh zero_le_sum.
repeat split; repeat zedifyg; try omega.
change ((1 - 1) * 1 / 2) with 0.
omega.
change ((1 - 1) * 1 / 2) with 0.
omega.
discriminate.
discriminate.
discriminate.
discriminate.
Qed.
These two lemmas are part of the complete proof, the second one containing the main body of the proof. This is a complex step that can’t be fully automatised and requires knowledge of formal verification techniques in Coq.
- Finally, include all the generated proofs into a certificate within the Java classes and send them to the verifier/executer.
At the verifying/executing end:
- Recompile to obtain new verification conditions from the bytecode and its annotations (without using the received certificate).
- Check the smart contract using the attached proofs against the newly generated verification conditions: if the compilation is successful, the smart contract is considered safe and can be executed.
Private Smart Contracts using Obliv-Java can also be easily annotated for Proof-Carrying Code: the source code for the full solution will be included in the open-sourcing of the Initial Distribution.