¡Bienvenido! ¿Eres nuevo en Zcash?
The Zcash network is young, but evolving quickly! Sign up and we'll be in touch with monthly highlights on ecosystem growth, network development and how to get started with Zcash!

Idioma

Bellman: zk-SNARKs en Rust

Sean Bowe | Apr 04, 2017

Bellman es una librería en lenguaje Rust para construir zk-SNARKs ─ pruebas de conocimiento-cero de computaciones arbitrarias pequeñas, con verificaciones que no demandan muchos recursos. El objetivo de Bellman es facilitar al público en general el uso y la experimentación con zk-SNARKs, y es también un paso adelante para mejorar la seguridad y el rendimiento de la próxima versión mayor de Zcash, Sapling.

Bellman contiene una implementación de la construcción de curva elíptica BLS12-381 que hemos descrito hace un par de semanas, la cual aparecerá en un próximo libro blanco de nuestros científicos. Esta construcción fue diseñada específicamente para la construcción eficiente de zk-SNARKs, manteniendo a la vez un alto margen de seguridad.

Esta semana, he añadido una implementación primitiva de un nuevo sistema de prueba de zk-SNARKs diseñado por Jens Groth. Seguro en el modelo de grupo genérico, el nuevo diseño produce pruebas más pequeñas que pueden ser construidas más rápidamente y con menos uso de memoria.

Descripción general de zk-SNARKs

Si estás interesado en el funcionamiento interno de las zk-SNARKs, Ariel Gabizon ha estado escribiendo una serie de artículos de blog sobre las matemáticas subyacentes a los que deberías echar un vistazo! Por el momento, podemos verlos a nivel superficial.

Las zk-SNARKs son pruebas potentes que, a diferencia de otros esquemas de pruebas de conocimiento-cero, son muy pequeñas (unos cientos de bytes) y son baratas de verificar (algunos milisegundos), incluso si el enunciado a demostrar es grande y complicado. Su propiedad de conocimiento-cero permite al probador ocultar detalles del cálculo a la vista del verificador durante el proceso, por lo que son útiles tanto para la privacidad como para el rendimiento.

Los únicos esquemas de este tipo que han probado ser eficientes son preprocesados. En cierto sentido, esto significa que debe construirse una especie de "entorno" que permite al probador evaluar la afirmación y producir una prueba. No existe una manera conocida de construir tal entorno sin estar necesariamente de manera temporal en posesión de información que permitiría construir pruebas falsas.

Zcash, que utiliza zk-SNARKs para sus transacciones blindadas, utiliza parámetros que fueron construidos en una sofisticada ceremonia de computaciones multipares sobre la que puedes leer más aquí. Las zk-SNARKs también son útiles en el modelo de verificador designado, donde el propio verificador construye los parámetros necesarios, por lo que ni el probador ni el verificador deben preocuparse de su integridad.

En muchos esquemas de zk-SNARK, el enunciado que se demuestra se reduce a lo que se llama un sistema de restricción cuadrática de rango-1, o R1CS. En este sistema, se da al probador un sistema de restricciones aritméticas sobre un conjunto de variables (elementos en un campo primo grande \(\mathbb{F}_r\)), y se le pide que produzca una asignación a las variables que satisfaga las restricciones.

Descripción general de Bellman

Bellman está actualmente en su infancia, pero ya podemos usarlo para construir este tipo de pruebas. Actualmente, sólo está disponible una API de muy bajo nivel, sobre la cual podemos construir DSLs y varias abstracciones para sintetizar circuitos. Si quieres experimentar con ella, puedes hacerlo con la caja bellman de crates.io.

Todas nuestras abstracciones de circuitos están escritas genéricamente sobre un trait del Motor que maneja la curva elíptica y la aritmética de campos finitos. Para la síntesis del circuito es central el trait ConstraintSystem:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
pub trait ConstraintSystem<E: Engine> {
    /// Asignar una variable privada en el sistema de restricciones, estableciéndolo en
    /// el valor proporcionado.
    fn alloc(&mut self, value: E::Fr) -> Variable;

    /// Hacer cumplir que `A` * `B` = `C`.
    fn enforce(
        &mut self,
        a: LinearCombination<E>,
        b: LinearCombination<E>,
        c: LinearCombination<E>
    );
}

Aquí hay dos decisiones de diseño importantes:

  1. Toda distribución y asignación de variables, y toda imposición de restricciones se realiza sobre el mismo pasaje de código. Esto difiere del diseño de gadgetlib en libsnark, para el cual era demasiado fácil olvidar potencialmente una restricción o notificar errores en las abstracciones existentes debido a la separación. Este enfoque facilita la escritura de abstracciones y la revisión de código.
  2. Todas las distribuciones y asignaciones de variables se realizan simultáneamente y las asignaciones existentes no pueden ser consultadas o modificadas. Esto fomenta un mejor diseño de gadgets e impide que los gadgets utilicen accidentalmente las asignaciones para "comunicarse" entre sí. Esto también tiene un beneficio de rendimiento: dado que todas las variables están ya asignadas, la imposición de restricciones durante la prueba se sintetiza directamente en los testigos subyacentes, para evitar absolutamente tener que mantener un sistema de restricciones en la memoria.

Como ejemplo de un tipo de implementación de gadgets, veamos cómo una variable restringida booleana podría ser implementada, junto con XOR:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
#[derive(Clone)]
pub struct Bit {
    var: Variable,
    value: bool
}

impl Bit {
    pub fn alloc<E, CS>(e: &E,
                        cs: &mut CS,
                        value: bool) -> Bit
        where E: Engine, CS: ConstraintSystem<E> + ?Sized
    {
        // Asignar la variable
        let var = cs.alloc(
            if value { E::Fr::one(e) } else { E::Fr::zero() }
        );

        // Hacer cumplir (1 - var) * var = 0, lo cual requiere que
        // var sea 0 or 1
        cs.enforce(
            LinearCombination::one(e) - var,
            LinearCombination::zero(e) + var,
            LinearCombination::zero(e)
        );

        Bit {
            var: var,
            value: value
        }
    }

    pub fn xor<E, CS>(&self,
                      e: &E,
                      cs: &mut CS,
                      other: &Bit) -> Bit
        where E: Engine, CS: ConstraintSystem<E>
    {
        let new_value = self.value ^ other.value;
        let new_var = cs.alloc(
            if new_value { E::Fr::one(e) } else { E::Fr::zero() }
        );

        // 2a * b = a + b - c
        cs.enforce(
            LinearCombination::zero(e) + self.var + self.var,
            LinearCombination::zero(e) + other.var,
            LinearCombination::zero(e) + self.var + other.var - new_var
        );

        Bit {
            var: new_var,
            value: new_value
        }
    }
}

Construir un circuito es cuestión de implementar los traits Circuit e Input:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
pub trait Circuit<E: Engine> {
    type InputMap: Input<E>;
    fn synthesize<CS: ConstraintSystem<E>>(self,
                                           engine: &E,
                                           cs: &mut CS)
                                           -> Self::InputMap;
}

pub trait Input<E: Engine> {
    fn synthesize<CS: PublicConstraintSystem<E>>(self, engine: &E, cs: &mut CS);
}

Este diseño divide los circuitos en una implementación Circuit, que los probadores instancian para construir pruebas, y una implementación Input, que los probadores y verificadores usan para realizar la distribución de entradas y la síntesis de circuitos relacionados. Esto difiere de libsnark, donde estas rutas de código son redundantes, utilizan diferentes funciones de utilidad y requieren una cuidadosa revisión del código para garantizar la coherencia.

Una vez que tenemos realmente una implementación de Circuit e Input, podemos usar las funciones proporcionadas en el módulo groth16: crear un par de claves (con algunos trapdoors seleccionados al azar), construir una prueba y realizar verificaciones:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
// Crear una clave de prueba y una clave de verificación
let (pk, vk) = {
    let tau = E::Fr::random(e, rng);
    let alpha = E::Fr::random(e, rng);
    let beta = E::Fr::random(e, rng);
    let gamma = E::Fr::random(e, rng);
    let delta = E::Fr::random(e, rng);
    let c = DummyCircuit;

    groth16::keypair(e, c, &tau, &alpha, &beta, &gamma, &delta)
};

// Construir una prueba
let proof = {
    let r = E::Fr::random(e, rng);
    let s = E::Fr::random(e, rng);

    let c = DummyCircuit;

    groth16::prove(e, c, &r, &s, &pk).unwrap()
};

// Preparar la clave de verificación
let pvk = groth16::prepare_verifying_key(e, &vk);

// Verificar la prueba
assert!(groth16::verify(e, |cs| {
    DummyInput
}, &proof, &pvk));

Trabajo futuro

Estos cimientos de bajo nivel son todo lo que está disponible en Bellman ahora mismo. En el futuro estaremos escribiendo herramientas que nos permitan construir cosas tales como funciones hash y cifrados de flujo.

Bellman está todavía en desarrollo y no debe ser utilizado aún en la producción de software. De hecho, de manera deliberada su API no expone nada que permita utilizarlo en la realidad! En la actualidad sirve como una excelente oportunidad de aprendizaje para la construcción de zk-SNARKs de forma segura y eficiente, y las lecciones que aprendemos a partir de su construcción moldearán el futuro de Zcash.

¡También estamos entusiasmados de estar escribiendo Bellman en Rust! Si eres aficionado a Rust y estás interesado en zk-SNARK o Zcash, te invitamos a visitar nuestro proyecto, a unirte a nuestro chat de la comunidad o a mirar algunas de las cosas que hemos escrito en Rust anteriormente, como nuestro código de la ceremonia computacional multipares.

Rust, cryptography, zkSNARKs | Ver todos los tags