Общая информация
Проверка во время выполнения - это метод анализа и выполнения вычислительной системы, предназначенный для извлечения информации из работающей системы для обнаружения и, возможно, реагирования на то, соответствует ли наблюдаемое поведение определенным атрибутам или нарушает их. Этот метод можно использовать для различных целей, таких как мониторинг политики безопасности или безопасности, отладка, тестирование, проверка, проверка, анализ производительности, отказоустойчивость, модификация поведения и многое другое. Он позволяет избежать сложностей традиционных формальных методов проверки за счет анализа небольшого числа траекторий выполнения и работы непосредственно с реальной системой.
Runtime Verification Inc. - компания, специализирующаяся на аудитах безопасности виртуальных машин и смарт-контрактов с использованием методов проверки во время выполнения. Услуги, которые они предоставляют, включают обзоры проектирования, обзоры кода, аудиты и формальную проверку смарт-контрактов и протоколов.
Какие продукты в настоящее время предлагает Runtime Verification Inc.?
Runtime Verification Inc. в настоящее время разрабатывает три основных продукта: RV-Predict - это инструмент прогнозного анализа времени выполнения, который фокусируется на автоматическом обнаружении одновременных ошибок в программе. RV-Monitor - это методология разработки и инструмент генерации библиотек, который позволяет отслеживать и выполнять выбранные пользователем свойства во время выполнения. RV-Match - это инструмент, который позволяет символически выполнять исчерпывающую проверку во время выполнения по всем возможным путям программы, тем самым доказывая, что определенные свойства правильны для всех возможных исполнений данной программы.
Когда и почему следует использовать RV-Predict?
Всякий раз, когда для многопоточных приложений важна корректность параллелизма, следует использовать RV-Predict. RV-Predict способен эффективно и беспрепятственно обнаруживать проблемы параллелизма и конкуренции данных в программе, очень прост в запуске и обычно не требует никакой конфигурации. RV-Predict также использует уникальные возможности прогнозирования для обнаружения возможных конфликтов, даже если они не встречаются в трассировке выполнения записей RV-Predict.
Когда и почему следует использовать RV-Monitor?
RV-Monitor позволяет отслеживать сложные приложения или системы и выполнять над ними свойства трассировки выполнения. RV-Monitor следует использовать до тех пор, пока существует спецификация для управления разработкой программ, и соблюдение этой спецификации является важной особенностью программного обеспечения. RV-Monitor также можно использовать для контроля соответствия общим API, включая API Android и Java.
Когда и почему следует использовать RV-Match?
RV-Monitor может проверять и обеспечивать соблюдение определенных свойств выполнения данной программы, в то время как RV-Match может доказывать правильность работы программы во время выполнения, тем самым анализируя следы выполнения на всех возможных путях выполнения и всех возможных входах. RV-Match обеспечивает надежные гарантии правильности, имитируя выполнение символическим образом с использованием формально определенной семантики целевого языка. Когда требуются строгие гарантии формальной проверки, следует использовать RV-Match, а также можно использовать с RV-Monitor для устранения мониторинга областей, которые могут доказать, что свойства никогда не нарушались.
Какие лицензии охватываются продуктами Runtime Verification Inc.?
Проекты, разработанные RV, делятся на две категории: проприетарные продукты и продукты, лицензированные по открытой лицензии (как часть экосистемы RV с открытым исходным кодом).
Проприетарные продукты включают все продукты, не лицензированные явно по открытой лицензии, и используются только для оценки и академических / некоммерческих целей. Производные работы не могут быть созданы с использованием проприетарных продуктов RV без предварительного разрешения, и RV оставляет за собой все права на проприетарные продукты. Собственные продукты не могут быть реконструированы каким-либо образом.
Аудит блокчейн-проекта
Runtime Verification участвует в аудите нескольких блокчейн-проектов, включая, помимо прочего, следующее:
- Аудит безопасности смарт-контрактов: они обеспечивают недорогой аудит таких контрактов, как ERC-20, ERC-721, ERC-4626 и т. д.
- Аудит безопасности протоколов: протоколы для операций, связанных с кредитованием.
- Официальная проверка: предоставляет инструменты для формальной проверки с открытым исходным кодом и разработки для снижения затрат на аудит и обеспечения непрерывной формальной проверки.
Их обычно включают ручные проверки и формальные проверки для обеспечения высокого уровня безопасности и надежности кода.
