Información general

La verificación en tiempo de ejecución es un método de análisis y ejecución de sistemas computacionales diseñado para extraer información de un sistema en ejecución para detectar y posiblemente responder si el comportamiento observado cumple o viola ciertos atributos. Esta técnica se puede utilizar para una variedad de propósitos, como monitoreo de políticas de seguridad o seguridad, depuración, pruebas, verificación, validación, análisis de rendimiento, seguridad contra fallos, modificación de comportamiento y más. Evita las complejidades de las técnicas tradicionales de verificación formal analizando un pequeño número de trayectorias de ejecución y trabajando directamente con el sistema real.

Runtime Verificación Inc. es una empresa centrada en la máquina virtual y las auditorías de seguridad de contratos inteligentes utilizando técnicas de verificación en tiempo de ejecución. Los servicios que proporcionan incluyen revisión de diseño, revisión de código, auditoría y verificación formal de contratos y protocolos inteligentes.

¿Qué productos ofrece actualmente Runtime Verificación Inc.?

Runtime Verificación Inc. Actualmente está desarrollando tres productos principales: RV-Predict es una herramienta de análisis predictivo de tiempo de ejecución que se enfoca en detectar automáticamente errores concurrentes en un programa. RV-Monitor es una metodología de desarrollo y una herramienta de generación de bibliotecas que permite que las propiedades seleccionadas por el usuario sean monitoreadas y ejecutadas en tiempo de ejecución. RV-Match es una herramienta que permite realizar una validación exhaustiva en tiempo de ejecución simbólicamente en todas las rutas de programa posibles, probando así que ciertas propiedades son correctas para todas las posibles ejecuciones de un programa dado.

¿Cuándo y por qué se debe usar RV-Predict?

Siempre que la corrección de la concurrencia sea importante para aplicaciones multihilo, se debe usar RV-Predict. RV-Predict es capaz de detectar de manera eficiente y sin problemas problemas problemas de concurrencia y contención de datos en un programa, es muy fácil de ejecutar y generalmente no requiere ninguna configuración. RV-Predict también utiliza capacidades únicas de predicción para detectar posibles contenciones, incluso si no se producen en el seguimiento de ejecución de los registros de RV-Predict.

¿Cuándo y por qué se debe usar RV-Monitor?

RV-Monitor permite monitorear aplicaciones o sistemas complejos y realizar propiedades de ejecución de seguimiento en ellos. RV-Monitor debe usarse mientras exista una especificación para administrar el desarrollo de programas, y el cumplimiento de esta especificación es una característica crítica del software. RV-Monitor también se puede usar para monitorear el cumplimiento con API comunes, incluidas las API de Android y Java.

¿Cuándo y por qué se debe usar RV-Match?

RV-Monitor puede verificar y hacer cumplir con ciertas propiedades de la ejecución de un programa dado, mientras que RV-Match puede demostrar la corrección de un programa en tiempo de ejecución, analizando así los rastros de ejecución en todas las rutas de ejecución posibles y todas las entradas posibles. RV-Match proporciona fuertes garantías de corrección, simulando la ejecución de manera simbólica utilizando la semántica formalmente definida del lenguaje de destino. Cuando se requieren fuertes garantías de validación formal, se debe usar RV-Match, y también se puede usar con RV-Monitor para eliminar el monitoreo de áreas que pueden demostrar que las propiedades nunca han sido violadas.

¿Qué licencias están cubiertas por los productos de Runtime Verificación Inc.?

Los proyectos desarrollados por RV se dividen en dos categorías: productos patentados y aquellos con licencia abierta (como parte del ecosistema de código abierto de RV).

Los productos patentados incluyen todos los productos no con licencia expresa bajo una licencia abierta y se utilizan solo para evaluación y con fines académicos / no comerciales. Los trabajos derivados no pueden crearse utilizando productos patentados de RV sin permiso previo, y RV se reserva todos los derechos sobre productos patentados. Los productos patentados no pueden ser de ingeniería inversa de ninguna manera.

Auditoría de proyectos de cadena de bloques

Verificación en tiempo de ejecución ha estado involucrada en la auditoría de múltiples proyectos de cadena de bloques, incluyendo pero no limitado a lo siguiente:

- Auditoría de seguridad de contratos inteligentes: proporcionan auditorías de bajo costo de contratos como ERC-20, ERC-721, ERC-4626, etc.

- Auditoría de seguridad de protocolos: incluye protocolos para operaciones relacionadas con préstamos.

- Verificación formal: proporciona herramientas de verificación formal y desarrollo de código abierto para reducir los costos de auditoría y permitir la verificación formal continua.

Sus auditorías suelen incluir revisiones manuales y verificaciones formales para garantizar altos niveles de seguridad y confiabilidad del código.