En Algorand, nos centramos intensamente en la seguridad y tomamos todas las medidas posibles para garantizar que nuestra cadena de bloques sea segura. Esto incluye pruebas exhaustivas, revisiones de código y código abierto para que todos puedan examinarlo por sí mismos.
Seguridad en el código
Debido a que el código es tan seguro como el protocolo que implementa, hemos analizado y razonado cuidadosamente sobre la exactitud del protocolo Algorand. Pero también sabemos que los protocolos para sistemas distribuidos son notoriamente difíciles de hacer bien, especialmente los protocolos que se ejecutan en sistemas no seguros y permiten que cualquiera participe sin necesidad de permiso de ninguna autoridad.
Verificación certificada por Runtime Verification
Para lograr una seguridad aún mayor sobre el protocolo Algorand, y para facilitar el diseño y la validación futura de nuevos protocolos, hemos optado por mejorar nuestras pruebas matemáticas en papel con enfoques de verificación formal verificables por máquina. Para ello, contratamos a Runtime Verification , una empresa con una gran experiencia en verificación, para certificar la exactitud del protocolo de consenso de Algorand. Nos complace informar un hito importante en este esfuerzo: utilizando el comprobador del teorema de Coq, el equipo ha desarrollado un modelo matemático preciso del protocolo y ha verificado formalmente su garantía de seguridad (que la cadena de bloques nunca se bifurca). Han escrito una publicación en el blog. describiendo este esfuerzo con enlaces al repositorio que contiene el modelo y la prueba. Queremos agradecer a Grigore Rosu, Musab A. Alturki, Brandon Moore, Karl Palmskog y Lucas Pena por su gran esfuerzo y logro.
Este artículo ha sido escrito originalmente por Algorand en «Medium» y traducido por AlgoLatam
Original Article: https://medium.com/algorand/formal-verification-of-the-algorand-protocol-bbde5a52b830
Aviso de responsabilidad:
Este artículo no contiene consejos financieros, ni recomendaciones de inversión de ningún tipo. La información brindada se ofrece sólo con fines educativos y didácticos en cuanto a tecnología Web3 y análisis sobre sus casos de uso.
Las inversiones con criptomonedas, NFTs, tokens u otros activos digitales conllevan riesgos y no se encuentran regulados, por lo que los lectores deben realizar su propia investigación antes de tomar cualquier tipo de decisión bajo su entera responsabilidad, así como adaptarse y observar las diferentes regulaciones legales según su país de residencia.