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