Código Acompañado de Demostraciones formales para la verificación de Contratos Inteligentes
¿Cómo se verifican actualmente los contratos inteligentes?
Por regla general, los contratos inteligentes se almacenan en un blockchain y los interesados en ejecutarlos deben inspeccionar primero su código fuente. Si hay N interesados en ejecutar el código fuente, todos deben verificarlo con la consecuente replicación de esfuerzo: en otras palabras, la carga de la prueba se desplaza del desarrollador de contratos de inteligentes a los interesados en ejecutarlos.
Para evitar que los N ejecutores deban verificar el código fuente por sí mismos, hay dos alternativas:
- Normalmente, un experto independiente es contratado para que lea el código fuente prestando gran atención al detalle y comprobándolo contra una lista de anti-patrones y errores comunes.
- De forma excepcional, se emplean herramientas de verificación formal para demostrar la corrección del contrato inteligente.
En ambos casos, el interesado en ejecutar el contrato inteligente debe confiar en que la verificación fue realizada correctamente: a no ser que se trate de un contexto malicioso, en el que se habrían dejado intencionalmente errores escondidos para robar a participantes desprecavidos, o que el proceso de auditoría hubiese sido negligente. En consecuencia, los participantes más prudentes seguirán teniendo que comprobar la corrección del contrato inteligente por sí mismos.
¿Cómo podría el Código Acompañado de Demostraciones formales mejorar la situación?
El Código Acompañado de Demostraciones formales (traducción del anglicismo Proof-Carrying Code -PCC-) resulta de gran ayuda en esta situación: utilizando herramientas PCC para la verificación formal, las demostraciones generadas son incluidas en el contrato inteligente y el interesado las debe comprobar antes de ejecutarlo.
Además, terceras partes podían proponer especificaciones formales y los contratos inteligentes cumplir con ellas para poder ser certificados formalmente: por ejemplo, un regulador podría expresar formalmente que las transacciones superiores a una cantidad dada deben ser notificadas a un servicio de confianza, y los contratos inteligentes deberían demostrar su corrección según dicha regulación formal.
Revisemos a modo ilustrativo un fácil ejemplo de la demostración formal de un contrato inteligente utilizando Código Acompañado de Demostraciones formales:
- Anotar el código con declaraciones de verificación formal:
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;
}
}
Compruébese que las pre-condiciones y post-condiciones del método getCumulativeContributions y el invariante del bucle donde todas las variables están acotadas.
- Compilar el código para obtener su bytecode, al mismo tiempo que se mantiene y traducen las declaraciones de verificación formal:
/*@
@ 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
Compruébese cómo se han mantenido las pre-condiciones, post-condiciones e invariantes del bucle.
- Generar Condiciones de Verificación formal a partir del bytecode y las declaraciones de verificación formal:
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))).
Esta es una de aserciones en Coq del archivo de anotaciones que contiene las pre-condiciones, post-condiciones y todas las aserciones de uno de los métodos de clase.
- Completa las demostraciones formales de las Condiciones de Verificación:
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.
Los dos lemas anteriores forman parte de la demostración formal, el segundo conteniendo la demostración completa. Es la parte compleja de todo el proceso que no puede ser automatizado completamente y requiere el conocimiento de técnicas de verificación formal en Coq.
- Por último, incluir las demostraciones generadas en un certificado dentro de las clases Java y envíalo todo al verificador/ejecutor.
En el lado que realiza la verificación/ejecución:
- Recompila para obtener nuevas Condiciones de Verificación a partir del bytecode y sus anotaciones (sin utilizar el certificado recibido).
- Comprueba el contrato inteligente utilizando las demostraciones adjuntas junto con las Condiciones de Verificación generadas: si la compilación tiene éxito, el contrato inteligente puede ser considerado seguro y entonces ser ejecutado.
Los Contratos Privados que utilizan Obliv-Java pueden ser anotados fácilmente con Código Acompañado de Demostraciones formales: el código fuente de la solución completa será incluido en la liberación de código fuente durante la Distribución Inicial.