Формальная проверка бинарных файлов с помощью Rocq

Автор предполагает, что бинарные файлы можно будет преобразовывать в формальные доказательства на Rocq, подтверждающие отсутствие недопустимых состояний.

Вероятно будущее софта, любой бинарь скомпилированный для одной платформв можно преобразовать в формальную rocq доказательство и затем показать что не будет недопустимых состояний. Правда это не значит что не будет багов или код не будет содержать cveшек, зато формальная логика будет в порядке

Кратко (AI)

Автор предполагает, что в будущем бинарный файл для конкретной платформы можно будет преобразовать в формальное доказательство на Rocq, подтверждающее отсутствие недопустимых состояний. При этом такая проверка, по его словам, не гарантирует отсутствия багов и уязвимостей CVE.

Формальная проверка бинарных файлов с помощью Rocq

Кратко (AI)

Обсуждение