суббота, 31 июля 2010 г.

[prog] Не могу не выдернуть из контекста пассаж про верификацию программ

Персонаж с ником gandjustas у меня уже мелькал – цитировал я его высказывания с RSDN. С удовольствием сделаю это еще раз.

Итак, замечательная фраза:

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

На что его вполне резонно спросили:

А что именно значит "ничего криминального"? Если программа делит единицу на миллиардный по счету бит числа пи, как верификатор поймет, что там деление на ноль? Если идет обращение к массиву с нетривиально вычисляемым индексом, как верификатор угадает, нет ли выхода за пределы? Если идет загрузка модуля с вычисляемым именем и вызов функции из него, как статический верификатор узнает, что за функция будет вызвана?

И тут последовал совершенно феноменальный ответ:

Я с теорией верифцирования не сильно знаком, но верификация и сейчас производится.

И там же:

Верификация не обязана проверять твою программу на соотвествие спецификации (у верификатора чато и нету спецификации), но верификатор может проверить программу на отсутствие нарушений памяти, обращений по невалидным указателям итп.

Между тем понятие “верификация” является давно устоявшимся термином, который как раз таки обозначает доказательство соответствия кода программы исходной спецификации. Интересующихся отсылаю к Wikipedia и содержащимся там ссылкам:

Verification and Validation (software)
Formal methods

PS. Кстати говоря, то, о чем говорит gandjustas – проверка отсутствия обращения по неверным указателям, проверка отсутствия выхода за пределы массивов, перезапись переменных на стеке и пр. – вовсе не являются свойствами управляемого кода. Компилирующиеся в нативный код языки со сборкой мусора и контролем за массивами и отсутствием адресной арифметики (Oberon, Eiffel, OCaml и, отчасти, Ada) дают точно такую же безопасность. Может быть даже большую, поскольку Ada контролирует в run-time корректность преобразований типов (afaik, если вы объявите тип A как 1..10, а тип B как 5..11, и попробуете преобразовать значение 2 от типа A к типу B, то получите исключение в run-time).

2 комментария:

Golovach Ivan комментирует...

Ммм ...
В мире java, например, термин "verification" очень распространен. Вот, например, свята-святых - спека JVM:
http://java.sun.com/docs/books/jvms/second_edition/html/VMSpecTOC.doc.html

главы:
2.17.3 Linking: Verification, Preparation, and Resolution
4.9 Verification of class Files
4.9.1 The Verification Process
4.9.2 The Bytecode Verifier
5.4 Linking
5.4.1 Verification

P.S. Просто термин "верификация" обозначает несколько различных процессов.

eao197 комментирует...

В JVM верификация байт кода аналогична, скажем, верификации документа с цифровой подписью. Т.е. отвечает только за то, чтобы проверить, действительно ли загруженный поток байт является Java кодом или же нам jpeg какой-то подсунули.

К верификации отсутствия запрещенных действий этот процесс, afaik, не имеет никакого отношения.