/ Verificación formal avanzada de la pila de software completa Web3 /
CertiK publicó recientemente un informe de verificación formal avanzada sobre el módulo Cosmos SDK Bank, que, hasta donde sabemos, es el primer intento exitoso de verificación formal del Cosmos SDK. La verificación formal es una técnica que utiliza lógica matemática para garantizar que un sistema cumpla con las especificaciones para que se comporte como se espera en todas las entradas y condiciones posibles. En este artículo, presentaremos los pasos específicos para verificar formalmente el módulo Cosmos SDK Bank, así como algunos resultados de la verificación.
¿Qué es el SDK de Cosmos?
El kit de desarrollo de software Cosmos (SDK para abreviar) es un marco que permite a los desarrolladores crear aplicaciones blockchain personalizadas. Con el SDK de Cosmos, los desarrolladores pueden lanzar fácilmente su propia cadena de bloques de Capa 1 sin tener que preocuparse por el diseño y la implementación desde la capa de consenso hasta la capa de aplicación. El SDK de Cosmos proporciona módulos centrales estándar que cualquier cadena puede importar y utilizar directamente, como módulos de participación, autenticación, gobierno y menta.
fuente:
Módulo bancario
El módulo bancario en Cosmos SDK se encarga de todas las funciones relacionadas con la gestión de tokens, como la transferencia de tokens nativos. El envío de tokens debe cumplir con muchas restricciones y condiciones, como tener suficientes tokens disponibles en la cuenta, excluyendo aquellos que han sido apostados, bloqueados o que se están desvinculando. Con el apoyo de módulos como staking y autenticación, el módulo bancario gestiona todo el proceso de envío de tokens. Aunque el módulo bancario depende de varios otros módulos, dado que están fuera del alcance de esta verificación formal, hacemos algunas suposiciones sobre su funcionalidad para simplificar el proceso.
El módulo bancario del SDK se compone de varios submódulos, incluidos el guardián y los tipos, que son los componentes principales que definen el comportamiento del módulo y los tipos de datos. Nos centraremos en el submódulo Keeper, ya que cubre la funcionalidad y características principales del módulo.
El submódulo guardián tiene dos componentes clave: ver y enviar. El encargado de la vista es responsable de administrar las cuentas y los saldos, mientras que el encargado del envío es responsable de cambiar los saldos de las cuentas, como transferir y apostar tokens bloqueados o desbloqueados. El flujo del módulo de banco se muestra en la siguiente figura. Las flechas indican la dirección desde los componentes a las funciones o Keepers.
fuente:
Método de autentificación
Como se mencionó anteriormente, el alcance de esta verificación se limita al módulo bancario. Antes de que comience la verificación, primero formulamos especificaciones formales para los tipos de datos en el módulo bancario. Por ejemplo, hay una estructura de datos de token en el módulo bancario, que contiene la denominación del tipo de cadena y la cantidad del tipo big.Int, que se define en el código fuente de la siguiente manera:
Esta estructura es muy simple, usamos Coq (nuestro lenguaje de modelado y verificación formal) para definirla de la siguiente manera:
Con base en esta definición, primero probamos algunas propiedades sobre las operaciones básicas de las monedas para sentar las bases de la integridad funcional del módulo bancario, porque requiere modificaciones y manipulaciones frecuentes del tipo de moneda. Por ejemplo:
Este lema demuestra una invariancia fundamental: restar dos monedas no cambia su denominación ni provoca un saldo negativo.
De manera similar al ejemplo anterior, los componentes subyacentes de cada transición de estado se modelan en Coq. Estos componentes incluyen KV Store, GasMeter, Error Handling y Context.
Para obtener especificaciones detalladas de los tipos de datos y su verificación, consulte:
Modela al guardián
Después de completar el modelado de los componentes básicos, podemos modelar el guardián central del módulo bancario para describir las funciones del módulo. El encargado del banco tiene dos interfaces, una para acceso de solo lectura a los datos de los tokens y la otra para la transferencia de tokens y el mantenimiento del suministro.
View keeper es responsable de manejar el acceso de solo lectura a los saldos de las cuentas y contiene cuatro funciones para calcular los saldos de las cuentas:
GetBalance: Consulta el saldo de la cuenta de una denominación específica por dirección. Considera dos casos: secuencia de bytes vacía y secuencia de bytes no vacía. La verificación formal garantiza que la función GetBalance produzca resultados correctos en ambos casos.
LockedCoins: Devuelve todos los tokens no consumibles de la cuenta correspondientes a una dirección. Debido a limitaciones de tiempo, hicimos suposiciones sobre algunas implementaciones del módulo de autenticación.
GetAllBalances: devuelve todos los saldos de las cuentas en la dirección especificada.
GetAccountsBalances: devuelve todos los saldos de cuentas almacenados, con los campos BAddress y BCoins como registros.
El administrador de envío maneja las transferencias y el suministro de tokens. Durante el proceso de transferencia, mantiene el suministro de tokens para que no se acuñen nuevos tokens.
SetBalance: establece el saldo del token de la cuenta a través de la dirección. Esta función considera dos casos: saldos establecidos en cero y saldos establecidos en distinto de cero. En ambos casos se demuestra la exactitud de SetBalance.
subUnlockedCoin: deduce la cantidad especificada (token) de una dirección. La función recursiva subUnlockedCoins hace lo mismo para un conjunto de tokens. Las propiedades relevantes de estas funciones se tratan como supuestos axiomáticos.
addCoin: agrega una cantidad específica (token) a una dirección. La función recursiva addCoins realiza la misma operación en un conjunto de tokens. Las propiedades relevantes de estas funciones se tratan como supuestos axiomáticos.
SendCoins: envía el monto de una dirección de cuenta a otra dirección de cuenta para que los fondos de ambas direcciones se actualicen. Si el destinatario no existe, se creará una nueva cuenta para él.
Utilizando el modelo de los componentes principales anteriores, podemos comenzar a verificar.
Proceso de verificación
Nuestra verificación se realiza describiendo formalmente las propiedades invariantes de estas funciones y probándolas en un sistema de prueba auxiliar, enfocándonos en las funciones principales de "View Keeper" y "Send Keeper".
Por ejemplo, la especificación y el lema setBalance_ok demuestran la exactitud de la función setBalance del módulo BaseSendKeeper, demostrando específicamente las siguientes propiedades:
Cuando send.setBalance vuelve al estado "Ok", hay un nuevo MultiStore. En este momento, el entorno actualizado uctx se deriva del antiguo entorno original ctx actualizando newMultiStore.
El saldo que se establece es un token válido (tiene las propiedades requeridas de un token en el sistema).
La relación de setBalance_prop se mantiene para garantizar que la función actualice el saldo en newMultiStore de la manera esperada y genere el entorno actualizado uctx.
Una vez completada la configuración del saldo, utilice la dirección de la cuenta y el saldo de denominación (Denom) para llamar a view.GetBalance en el entorno actualizado uctx, y se devolverá el mismo saldo establecido por send.setBalance.
Estas propiedades se describen en el lenguaje de especificación de Coq de la siguiente manera:
Para códigos Coq de otras propiedades, visite:
futura carrera
La base de esta verificación se basa en varios supuestos y axiomas, que podemos verificar más profundamente para ampliar el alcance de la verificación. El trabajo futuro se centra en las siguientes áreas:
Verificación de supuestos: La verificación actual se basa en una serie de supuestos como base para la prueba. Estos supuestos se pueden probar en el futuro para garantizar que reflejen con precisión el comportamiento y las propiedades esperados del sistema.
Autenticación del módulo de autenticación: este módulo es responsable de administrar los datos de la cuenta y los mecanismos de firma, y es el componente principal del SDK de Cosmos. En el futuro, se podrá verificar completamente formalmente para garantizar que la implementación del módulo y la interacción con otros módulos sean precisas.
Más teoremas sobre la encomienda, acuñación y venta de monedas: ampliar el alcance de la verificación e introducir más teoremas sobre la encomienda, acuñación y venta de monedas ayudará a comprender el mecanismo operativo del sistema de manera más integral. Estos teoremas se pueden combinar con la verificación del módulo de autenticación para garantizar la coherencia y corrección general del sistema.
Ampliar toda la infraestructura de Cosmos SDK: el trabajo de verificación actual se centra principalmente en el módulo bancario y sus componentes relacionados. En el futuro, el proceso de verificación formal se puede extender a toda la infraestructura de Cosmos SDK, mejorando así la precisión, seguridad y estabilidad generales de la plataforma y proporcionando un entorno más estable y confiable para desarrolladores y usuarios.
Integración con otros módulos: dado que Cosmos SDK incluye varios módulos interconectados, es beneficioso explorar las interacciones y dependencias entre ellos. Esto requiere verificar la exactitud de las interacciones entre módulos y garantizar que cualquier cambio en un módulo no afecte negativamente a otros módulos.
Modelado y verificación de mecanismos de incentivos: Cosmos SDK también integra mecanismos de incentivos como apuestas y distribución de recompensas. Investigaciones futuras modelarán y validarán estos mecanismos para garantizar que sean correctos y consistentes con los incentivos económicos esperados.
Este artículo presenta el primer caso exitoso de una verificación formal avanzada del módulo Cosmos SDKbank, lo que hace un trabajo efectivo para la base de seguridad y confiabilidad del ecosistema blockchain. El trabajo futuro ampliará este logro validando suposiciones, validando otros módulos y cubriendo toda la infraestructura de Cosmos SDK, construyendo en última instancia una plataforma más sólida y creíble para desarrolladores y usuarios.
Ver originales
Esta página puede contener contenido de terceros, que se proporciona únicamente con fines informativos (sin garantías ni declaraciones) y no debe considerarse como un respaldo por parte de Gate a las opiniones expresadas ni como asesoramiento financiero o profesional. Consulte el Descargo de responsabilidad para obtener más detalles.
Explicación detallada de la verificación formal de los módulos estándar Cosmos SDK
/ Verificación formal avanzada de la pila de software completa Web3 /
CertiK publicó recientemente un informe de verificación formal avanzada sobre el módulo Cosmos SDK Bank, que, hasta donde sabemos, es el primer intento exitoso de verificación formal del Cosmos SDK. La verificación formal es una técnica que utiliza lógica matemática para garantizar que un sistema cumpla con las especificaciones para que se comporte como se espera en todas las entradas y condiciones posibles. En este artículo, presentaremos los pasos específicos para verificar formalmente el módulo Cosmos SDK Bank, así como algunos resultados de la verificación.
¿Qué es el SDK de Cosmos?
El kit de desarrollo de software Cosmos (SDK para abreviar) es un marco que permite a los desarrolladores crear aplicaciones blockchain personalizadas. Con el SDK de Cosmos, los desarrolladores pueden lanzar fácilmente su propia cadena de bloques de Capa 1 sin tener que preocuparse por el diseño y la implementación desde la capa de consenso hasta la capa de aplicación. El SDK de Cosmos proporciona módulos centrales estándar que cualquier cadena puede importar y utilizar directamente, como módulos de participación, autenticación, gobierno y menta.
fuente:
Módulo bancario
El módulo bancario en Cosmos SDK se encarga de todas las funciones relacionadas con la gestión de tokens, como la transferencia de tokens nativos. El envío de tokens debe cumplir con muchas restricciones y condiciones, como tener suficientes tokens disponibles en la cuenta, excluyendo aquellos que han sido apostados, bloqueados o que se están desvinculando. Con el apoyo de módulos como staking y autenticación, el módulo bancario gestiona todo el proceso de envío de tokens. Aunque el módulo bancario depende de varios otros módulos, dado que están fuera del alcance de esta verificación formal, hacemos algunas suposiciones sobre su funcionalidad para simplificar el proceso.
El módulo bancario del SDK se compone de varios submódulos, incluidos el guardián y los tipos, que son los componentes principales que definen el comportamiento del módulo y los tipos de datos. Nos centraremos en el submódulo Keeper, ya que cubre la funcionalidad y características principales del módulo.
El submódulo guardián tiene dos componentes clave: ver y enviar. El encargado de la vista es responsable de administrar las cuentas y los saldos, mientras que el encargado del envío es responsable de cambiar los saldos de las cuentas, como transferir y apostar tokens bloqueados o desbloqueados. El flujo del módulo de banco se muestra en la siguiente figura. Las flechas indican la dirección desde los componentes a las funciones o Keepers.
fuente:
Método de autentificación
Como se mencionó anteriormente, el alcance de esta verificación se limita al módulo bancario. Antes de que comience la verificación, primero formulamos especificaciones formales para los tipos de datos en el módulo bancario. Por ejemplo, hay una estructura de datos de token en el módulo bancario, que contiene la denominación del tipo de cadena y la cantidad del tipo big.Int, que se define en el código fuente de la siguiente manera:
Esta estructura es muy simple, usamos Coq (nuestro lenguaje de modelado y verificación formal) para definirla de la siguiente manera:
Con base en esta definición, primero probamos algunas propiedades sobre las operaciones básicas de las monedas para sentar las bases de la integridad funcional del módulo bancario, porque requiere modificaciones y manipulaciones frecuentes del tipo de moneda. Por ejemplo:
Este lema demuestra una invariancia fundamental: restar dos monedas no cambia su denominación ni provoca un saldo negativo.
De manera similar al ejemplo anterior, los componentes subyacentes de cada transición de estado se modelan en Coq. Estos componentes incluyen KV Store, GasMeter, Error Handling y Context.
Para obtener especificaciones detalladas de los tipos de datos y su verificación, consulte:
Modela al guardián
Después de completar el modelado de los componentes básicos, podemos modelar el guardián central del módulo bancario para describir las funciones del módulo. El encargado del banco tiene dos interfaces, una para acceso de solo lectura a los datos de los tokens y la otra para la transferencia de tokens y el mantenimiento del suministro.
View keeper es responsable de manejar el acceso de solo lectura a los saldos de las cuentas y contiene cuatro funciones para calcular los saldos de las cuentas:
GetBalance: Consulta el saldo de la cuenta de una denominación específica por dirección. Considera dos casos: secuencia de bytes vacía y secuencia de bytes no vacía. La verificación formal garantiza que la función GetBalance produzca resultados correctos en ambos casos.
LockedCoins: Devuelve todos los tokens no consumibles de la cuenta correspondientes a una dirección. Debido a limitaciones de tiempo, hicimos suposiciones sobre algunas implementaciones del módulo de autenticación.
GetAllBalances: devuelve todos los saldos de las cuentas en la dirección especificada.
GetAccountsBalances: devuelve todos los saldos de cuentas almacenados, con los campos BAddress y BCoins como registros.
El administrador de envío maneja las transferencias y el suministro de tokens. Durante el proceso de transferencia, mantiene el suministro de tokens para que no se acuñen nuevos tokens.
SetBalance: establece el saldo del token de la cuenta a través de la dirección. Esta función considera dos casos: saldos establecidos en cero y saldos establecidos en distinto de cero. En ambos casos se demuestra la exactitud de SetBalance.
subUnlockedCoin: deduce la cantidad especificada (token) de una dirección. La función recursiva subUnlockedCoins hace lo mismo para un conjunto de tokens. Las propiedades relevantes de estas funciones se tratan como supuestos axiomáticos.
addCoin: agrega una cantidad específica (token) a una dirección. La función recursiva addCoins realiza la misma operación en un conjunto de tokens. Las propiedades relevantes de estas funciones se tratan como supuestos axiomáticos.
SendCoins: envía el monto de una dirección de cuenta a otra dirección de cuenta para que los fondos de ambas direcciones se actualicen. Si el destinatario no existe, se creará una nueva cuenta para él.
Utilizando el modelo de los componentes principales anteriores, podemos comenzar a verificar.
Proceso de verificación
Nuestra verificación se realiza describiendo formalmente las propiedades invariantes de estas funciones y probándolas en un sistema de prueba auxiliar, enfocándonos en las funciones principales de "View Keeper" y "Send Keeper".
Por ejemplo, la especificación y el lema setBalance_ok demuestran la exactitud de la función setBalance del módulo BaseSendKeeper, demostrando específicamente las siguientes propiedades:
Cuando send.setBalance vuelve al estado "Ok", hay un nuevo MultiStore. En este momento, el entorno actualizado uctx se deriva del antiguo entorno original ctx actualizando newMultiStore.
El saldo que se establece es un token válido (tiene las propiedades requeridas de un token en el sistema).
La relación de setBalance_prop se mantiene para garantizar que la función actualice el saldo en newMultiStore de la manera esperada y genere el entorno actualizado uctx.
Una vez completada la configuración del saldo, utilice la dirección de la cuenta y el saldo de denominación (Denom) para llamar a view.GetBalance en el entorno actualizado uctx, y se devolverá el mismo saldo establecido por send.setBalance.
Estas propiedades se describen en el lenguaje de especificación de Coq de la siguiente manera:
Para códigos Coq de otras propiedades, visite:
futura carrera
La base de esta verificación se basa en varios supuestos y axiomas, que podemos verificar más profundamente para ampliar el alcance de la verificación. El trabajo futuro se centra en las siguientes áreas:
Verificación de supuestos: La verificación actual se basa en una serie de supuestos como base para la prueba. Estos supuestos se pueden probar en el futuro para garantizar que reflejen con precisión el comportamiento y las propiedades esperados del sistema.
Autenticación del módulo de autenticación: este módulo es responsable de administrar los datos de la cuenta y los mecanismos de firma, y es el componente principal del SDK de Cosmos. En el futuro, se podrá verificar completamente formalmente para garantizar que la implementación del módulo y la interacción con otros módulos sean precisas.
Más teoremas sobre la encomienda, acuñación y venta de monedas: ampliar el alcance de la verificación e introducir más teoremas sobre la encomienda, acuñación y venta de monedas ayudará a comprender el mecanismo operativo del sistema de manera más integral. Estos teoremas se pueden combinar con la verificación del módulo de autenticación para garantizar la coherencia y corrección general del sistema.
Ampliar toda la infraestructura de Cosmos SDK: el trabajo de verificación actual se centra principalmente en el módulo bancario y sus componentes relacionados. En el futuro, el proceso de verificación formal se puede extender a toda la infraestructura de Cosmos SDK, mejorando así la precisión, seguridad y estabilidad generales de la plataforma y proporcionando un entorno más estable y confiable para desarrolladores y usuarios.
Integración con otros módulos: dado que Cosmos SDK incluye varios módulos interconectados, es beneficioso explorar las interacciones y dependencias entre ellos. Esto requiere verificar la exactitud de las interacciones entre módulos y garantizar que cualquier cambio en un módulo no afecte negativamente a otros módulos.
Modelado y verificación de mecanismos de incentivos: Cosmos SDK también integra mecanismos de incentivos como apuestas y distribución de recompensas. Investigaciones futuras modelarán y validarán estos mecanismos para garantizar que sean correctos y consistentes con los incentivos económicos esperados.
Este artículo presenta el primer caso exitoso de una verificación formal avanzada del módulo Cosmos SDKbank, lo que hace un trabajo efectivo para la base de seguridad y confiabilidad del ecosistema blockchain. El trabajo futuro ampliará este logro validando suposiciones, validando otros módulos y cubriendo toda la infraestructura de Cosmos SDK, construyendo en última instancia una plataforma más sólida y creíble para desarrolladores y usuarios.