Pull to refresh

Comments 10

Вообще-то круто. Вот как-то так и нужно будет сдерживать мощь ИИ, чтобы он нас не отформатировал.
Звучит фантастически. И в прямом, и в переносном смысле.

Было бы здорово узнать, что такое формальная верификация, пару слов о принципах строгой математической проверки. Первый раз слышу. Это вообще как?

на хабре например было (а по тегу еще куча находится). На мой взгляд при этом подходе уделяется внимание не всем аспектам безопасности: например как верификация одного ПО защитит от уязвимостей в процессорах/прошивке? В ПО для верификации так же могут быть ошибки. И т.д.
UFO just landed and posted this here
наша система может защищать личные данные и вычисления, загруженные в облако, с математическими гарантиями

А по факту потом данные утекут через какую-нибудь XSS дырку или закладку АНБ. Вообще после всех историй о дырках и взломах всего, странно давать 100% гарантии.
Основная проблема систем формальной верификации в том, что они ограничены рамками математической модели. В случае полностью верифицированного ПО уязвимости надо искать в фактическом различии между реальностью и моделью.
Так, например, модель верифицирующая программу на уровне ассемблерного кода не сможет определить наличие уязвимости типа SPECTRE если:
1. Не знает о ней заранее.
2. Не умеет заглядывать на уровень процессорной архитектуры или микрокода ЦП.
Предположим, что мат.модель верификации гипервизора корректна, полна, и описывает все аспекты функционирования (API в сторону ОС, корректная работа с железом, корректная архитектура). Для формального доказательства корректности исполнения гипервизора необходимо ещё наличие верифицированного компилятора и верифицированной платформы исполнения.
Предположим, верифицированный компилятор существует (несколько реализаций ADA), но о верифицированных платформах я не слышал…
Работу, конечно, проделали коллосальную, но во многом — бессмысленную.
использовали язык с хорошей типизацией аля haskell?
Sign up to leave a comment.

Other news