Runtime Verification

Informations générales

La vérification d'exécution est une méthode d'analyse et d'exécution de système informatique conçue pour extraire des informations d'un système en cours d'exécution afin de détecter et éventuellement de déterminer si le comportement observé respecte ou enfreint certains attributs. Cette technique peut être utilisée à diverses fins, telles que la surveillance des politiques de sécurité ou de sécurité, le débogage, les tests, la vérification, la validation, l'analyse des performances, la sécurité intégrée, la modification du comportement, etc. Elle évite les complexités des techniques de vérification formelles traditionnelles en analysant un petit nombre de trajectoires d'exécution et en travaillant directement avec le système réel.

Runtime Verification Inc. est une entreprise axée sur les audits de sécurité des machines virtuelles et des contrats intelligents à l'aide de techniques de vérification d'exécution. Les services qu'ils fournissent comprennent des revues de conception, des revues de code, des audits et la vérification formelle des contrats et protocoles intelligents.

Quels sont les produits actuellement proposés par Runtime Verification Inc.?

Runtime Verification Inc. développe actuellement trois produits de base : RV-Predict est un outil d'analyse prédictive d'exécution qui se concentre sur la détection automatique des erreurs concomitantes dans un programme. RV-Monitor est une méthodologie de développement et un outil de génération de bibliothèque qui permet de surveiller et d'exécuter les propriétés sélectionnées par l'utilisateur au moment de l'exécution. RV-Match est un outil qui permet d'effectuer une validation d'exécution exhaustive de manière symbolique sur tous les chemins de programme possibles, prouvant ainsi que certaines propriétés sont correctes pour toutes les exécutions possibles d'un programme donné.

Quand et pourquoi utiliser RV-Predict?

Chaque fois que l'exactitude de la concurrence est importante pour les applications multithread, RV-Predict doit être utilisé. RV-Predict est capable de détecter efficacement et de manière transparente les problèmes de concurrence et les conflits de données dans un programme, est très facile à exécuter et ne nécessite généralement aucune configuration. RV-Predict utilise également des capacités de prédiction uniques pour détecter les conflits possibles, même s'ils ne se produisent pas dans la trace d'exécution des enregistrements RV-Predict.

Quand et pourquoi utiliser RV-Monitor?

RV-Monitor permet de surveiller des applications ou des systèmes complexes et d'y exécuter des propriétés d'exécution de trace. RV-Monitor doit être utilisé tant qu'une spécification existe pour gérer le développement de programmes, et le respect de cette spécification est une caractéristique essentielle du logiciel. RV-Monitor peut également être utilisé pour surveiller la conformité avec les API courantes, y compris les API Android et Java.

Quand et pourquoi utiliser RV-Match?

RV-Monitor peut vérifier et appliquer la conformité avec certaines propriétés de l'exécution d'un programme donné, tandis que RV-Match peut prouver l'exactitude d'un programme au moment de l'exécution, analysant ainsi les traces d'exécution sur tous les chemins d'exécution possibles et toutes les entrées possibles. RV-Match fournit de solides garanties d'exactitude, simulant l'exécution de manière symbolique en utilisant la sémantique formellement définie du langage cible. Lorsque de solides garanties de validation formelle sont requises, RV-Match doit être utilisé et peut également être utilisé avec RV-Monitor pour éliminer la surveillance des zones qui peuvent prouver que les propriétés n'ont jamais été violées.

Quelles licences sont couvertes par les produits de Runtime Verification Inc.?

Les projets développés par RV se divisent en deux catégories : les produits propriétaires et ceux concédés sous licence ouverte (dans le cadre de l'écosystème open source de RV).

Les produits propriétaires incluent tous les produits qui ne sont pas expressément concédés sous licence ouverte et sont utilisés uniquement à des fins d'évaluation et à des fins académiques / non commerciales. Les œuvres dérivées ne peuvent pas être créées à l'aide de produits RV propriétaires sans autorisation préalable, et RV se réserve tous les droits sur les produits propriétaires. Les produits propriétaires ne peuvent en aucun cas faire l'objet d'une ingénierie inverse.

Audit de projet blockchain

La vérification d'exécution a été impliquée dans l'audit de plusieurs projets blockchain, y compris, mais sans s'y limiter :

- Audit de sécurité des contrats intelligents : Ils fournissent des audits à faible coût de contrats tels que ERC-20, ERC-721, ERC-4626, etc.

- Audit de sécurité des protocoles : Comprend des protocoles pour les opérations liées aux prêts.

- Vérification formelle : Fournit une vérification formelle open source et des outils de développement pour réduire les coûts d'audit et permettre une vérification formelle continue. Leurs audits et vérifications manuelles pour garantir une fiabilité élevées.