General Information

Runtime Verification ist eine Methode der rechnerischen Systemanalyse und -ausführung, die entwickelt wurde, um Informationen aus einem laufenden System zu extrahieren, um zu erkennen und möglicherweise darauf zu reagieren, ob beobachtetes Verhalten bestimmte Attribute erfüllt oder verletzt. Diese Technik kann für eine Vielzahl von Zwecken verwendet werden, wie z. B. Überwachung von Sicherheits- oder Sicherheitsrichtlinien, Debugging, Testen, Verifizierung, Validierung, Leistungsanalyse, Failsafe, Verhaltensänderung und mehr. Sie vermeidet die Komplexität herkömmlicher formaler Verifizierungstechniken, indem sie eine kleine Anzahl von Ausführungstrajektorien analysiert und direkt mit dem tatsächlichen System zusammenarbeitet.

Runtime Verification Inc. ist ein Unternehmen, das sich auf Sicherheitsaudits für virtuelle Maschinen und intelligente Verträge unter Verwendung von Laufzeitverifizierungstechniken konzentriert. Zu den Dienstleistungen, die sie anbieten, gehören Entwurfsprüfungen, Codeprüfungen, Audits und formale Verifizierung von intelligenten Verträgen und Protokollen.

Was Produkte werden derzeit von Runtime Verification Inc. angeboten?

Runtime Verification Inc. entwickelt derzeit drei Kernprodukte: RV-Predict ist ein prädiktives Laufzeitanalysetool, das sich auf die automatische Erkennung gleichzeitiger Fehler in einem Programm konzentriert. RV-Monitor ist eine Entwicklungsmethodik und ein Bibliothekserzeugungstool, mit dem vom Benutzer ausgewählte Eigenschaften zur Laufzeit überwacht und ausgeführt werden können. RV-Match ist ein Tool, mit dem eine erschöpfende Laufzeitvalidierung symbolisch auf allen möglichen Programmpfaden durchgeführt werden kann, wodurch bewiesen wird, dass bestimmte Eigenschaften für alle möglichen Ausführungen eines bestimmten Programms korrekt sind.

Wann und warum sollte RV-Predict verwendet werden?

Wann immer Gleichzeitigkeitskorrektheit für Anwendungen mit mehreren Threads wichtig ist, sollte RV-Predict verwendet werden. RV-Predict ist in der Lage, Gleichzeitigkeitsprobleme und Datenkonflikte in einem Programm effizient und nahtlos zu erkennen, ist sehr einfach auszuführen und erfordert im Allgemeinen keine Konfiguration. RV-Predict nutzt auch einzigartige Vorhersagefunktionen, um mögliche Streitigkeiten zu erkennen, selbst wenn sie nicht in der Ausführungsspur von RV-Predict-Datensätzen auftreten.

Wann und warum sollte RV-Monitor verwendet werden?

RV-Monitor ermöglicht es, komplexe Anwendungen oder Systeme zu überwachen und Trace-Ausführungseigenschaften auf ihnen auszuführen. RV-Monitor sollte verwendet werden, solange eine Spezifikation für die Verwaltung der Programmentwicklung existiert, und die Einhaltung dieser Spezifikation ist ein entscheidendes Merkmal der Software. RV-Monitor kann auch verwendet werden, um die Einhaltung gängiger APIs, einschließlich Android- und Java-APIs, zu überwachen.

Wann und warum sollte RV-Match verwendet werden?

RV-Monitor kann die Einhaltung bestimmter Eigenschaften der Ausführung eines bestimmten Programms überprüfen und erzwingen, während RV-Match die Korrektheit eines Programms zur Laufzeit nachweisen kann, wodurch Ausführungsspuren auf allen möglichen Ausführungspfaden und allen möglichen Eingaben analysiert werden. RV-Match bietet starke Korrektheitsgarantien und simuliert die Ausführung auf symbolische Weise unter Verwendung der formell definierten Semantik der Zielsprache. Wenn starke Garantien für die formale Validierung erforderlich sind, sollte RV-Match verwendet werden und kann auch mit RV-Monitor verwendet werden, um die Überwachung von Bereichen zu eliminieren, die beweisen können, dass Eigenschaften nie verletzt wurden.

Welche Lizenzen werden von den Produkten von Runtime Verification Inc. abgedeckt?

Projekte, die von RV entwickelt werden, fallen in zwei Kategorien: proprietäre Produkte und solche, die unter einer offenen Lizenz lizenziert sind (als Teil des Open-Source-Ökosystems von RV).

Proprietäre Produkte umfassen alle Produkte, die nicht ausdrücklich unter einer offenen Lizenz lizenziert sind und nur für Evaluierungszwecke und akademische / nicht-kommerzielle Zwecke verwendet werden. Derivative Werke dürfen ohne vorherige Genehmigung nicht mit proprietären RV-Produkten erstellt werden, und RV behält sich alle Rechte an proprietären Produkten vor. Proprietäre Produkte können in keiner Weise zurückentwickelt werden.

Blockchain Project Audit

Runtime Verification war an der Prüfung mehrerer Blockchain-Projekte beteiligt, einschließlich, aber nicht beschränkt auf die folgenden:

- Security Audit of Smart Contracts: Sie bieten kostengünstige Audits von Verträgen wie ERC-20, ERC-721, ERC-4626 usw.

- Security Audit of Protocols: Enthält Protokolle für kreditbezogene Operationen.

- Formale Verifizierung: Bietet Open-Source-Tools für formale Verifizierung und Entwickler, um die Auditkosten zu senken und eine kontinuierliche formale Verifizierung zu ermöglichen.

Ihre Audits umfassen in der Regel manuelle Überprüfungen und formale Verifizierungen, um ein hohes Maß an Codesicherheit und Zuverlässigkeit zu gewährleisten.