Санкт-Петербургская группа тестирования JVM

Верификация байт-кода в JVM

При исполнении программы в JVM, требуется, чтобы она “оставалась в своей песочнице”, не нарушая работу JVM и подчиняясь ограничениям безопасности. Это особенно важно для классов, загружаемых из Интернета (как, впрочем, и для стабильной работы JVM).

Про ограничения безопасности мы поговорим в отдельной статье, а сейчас остановимся на проверке корректности исполнения программы в JVM.

Конечно же, компилятор javac порождает корректный байткод, но кто сказал, что класс создан именно javac? Ведь существуют и библиотеки (ASM, BCEL, SERP) для создания классов из байткода, компиляторы других фирм, Java-ассемблеры и прочие средства. Кроме того, используемые класс-файлы могут изменяться и компилироваться независимо друг от друга.

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

Вот список того, что проверяет JVM, согласно спецификации:

На проходе 1 (загрузка, loading):

1. Формат класс-файла (magic number, длина)

На проходе 2 (связывание, linking):

1. Соблюдение правил использования модификатора final

2. Наличие суперкласса (кроме java.lang.Object)

3. Формат constant-pool, ссылки внутри него

Проход 3 (собственно, верификация на этапе связывания):

1. Формат команд байт-кода, аргументы и индексы

2. Семантику команд:

   1. Соблюдение типов во время присвоения значений полям класса

   2. Доступ к локальным переменным в методе

   3. Размер стека операндов метода, типы значений в нем. То же для локальных переменных.

   4. Аргументы при вызове метода

3. Входы в обработчики исключений (только через исключение)

4. Инструкции jsr/ret

Проход 4 (виртуальный, на этапе выполнения инструкции):

1. Вызываемый методы или переменная, к которой производится доступ действительно существует в соответствующем классе

2. Тип переменной или сигнатура вызываемого метода совпадают с теми, которые записаны в вызывающий метод компилятором

3. Флаги доступа вызываемого методу разрешают доступ из вызывающего метода. То же для переменных.

В данной статье мы затронем 3-й проход: верификацию байт-кода, так как в JVM 1.6.0 появился новый верификатор.

Надо сказать, что в общем случае алгоритмическая задача верификации (т.е., доказательства корректности программы) неразрешима за конечное время, так как фактически доказательство корректности эквивалентно исполнению проверяемой программы. А что будет, если она выделяет память в бесконечном цикле? (Готов поспорить, что как минимум одна подобная программа сейчас запущена на вашем компьютере) Верификация сводится, таким образом, к решению проблемы зависания (Halting Problem), неразрешимость которой еще в 1936 году была доказана Тьюрингом и Чёрчем. Постойте, — скажете вы, — но ведь на машине с конечным объемом памяти можно просто перечислить все возможные состояния. Действительно, верификация в этом случае разрешима, но какой ценой? Например, 64 Мб оперативной памяти, отведенные под процесс Java будут иметь около 10^178956970 состояний. Для сравнения: количество элементарных частиц во вселенной оценивается в 10⁷³—10⁸⁸ штук.

Как же быть с верификатором Java? Можно пойти следующим путем: во всем множестве корректных программ выделить такое подмножество, для которого мы сможем доказать корректность за приемлемое конечное время и используя конечный объем памяти (подумайте, как это важно, например, для мобильников или JavaCard).

Но и в этом случае не существует серебрянной пули: построив верификатор нам нужно будет доказать корректность самого верификатора. В литературе можно найти несколько моделей Java-верификатора, корректность которых доказана средствами математической логики¹. Но эти модели используют усеченный вариант байт-кода, не подходящий для применения в реалиях нашего мира JVM, где есть еще и загрузчики классов, сборщик мусора, отладчики, JNI и агенты. Так что, приходится лишь довольствоваться здравым смыслом.

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

Для каждой инструкции старый верификатор вычислял и запоминал состояние стека и переменных, стек подпрограмм (jsr/ret). Для подпрограмм запоминалась еще битовая маска модифицированных локальных переменных².

Остается проблема завершения верификации. Даже самые современные, самые быстрые вычислительные машины пока еще не научились выполнять бесконечный цикл за время, о котором не стыдно рассказать коллеге. Однако, старый верификатор решал эту проблему так: если программа снова приходит в некоторую свою точку и состояние стека и локальных переменных эквивалентно предыдущему, уже проверенному в этой точке состоянию, мы смело можем пропустить данный адрес и перейти к следующему непровереннму. Если же состояние изменилось, верификатор заново проходит путь от данной точки. Но при этом необходимо было обеспечить сходимость процесса.

В старом верификаторе, его авторы, James Gosling и Frank Yellin, решили пойти следующим путем: JVM требует, чтобы в точках программы, в которые могут привести 2 или более путей выполнения длины стека и локальных переменных должны совпадать, а состояния — быть совместимыми.

Совместимыми — это значит у двух типов находящихся в одной ячейке локальных переменных или стека должен быть общий супертип. Дерево типов верификатора расширяет дерево типов Java-объектов следующим образом³:

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

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

Таким образом, верификатор пытался определить типы, имитируя выполнение программы. В худшем случае, сложность верификации была O(n * log₂ t), где t — количество типов в дереве типов (включая классы Java), а n — количество инструкций⁴.

Такая сложность оказалась слишком велика для Java Mobile Edition, поэтому в виртуальной машине KVM (Kilobyte Virtual Machine), используемой в Java ME вместо обычного верификатора, называемого еще Type Inferencer был применен другой верификатор, так называемый Type Checker или Split-Verifier (см. Appendix 1 спецификации CLDC 1.1)⁵.

Новый верификатор был доработан и перенесен в Java 6.0. Его спецификация была разработана в рамках JSR 202. Отмечу, что в качестве нотации для формул используется язык Пролог. Старая спецификация излагала требования простым английским.

Split-Verifier не пытается определить типы самостоятельно, а сверяет состояния стека и локальных переменных, с образцом, уже сгенерированные компилятором. Эти состояния компилятор помещает в атрибут StackMapTable, который появляется начиная с версии 50 класс-файла. Этот атрибут является обязательным, если в методе присутствует хоть одна команда ветвления или обработчик исключения. Изначальное состояние стека и переменных при входе в метод формируется самим верификатором.

Если же требуемый атрибут StackMapTable отстутствует, версия class-файла меньше, чем 50 или в байт-коде присутствуют инструкции jsr/ret то используется старый верификатор, который может быть вообще исключен в следующих версиях Java SE.

Это может представлять проблему для генерации или инструментирования байт-кода, т. к. теперь библиотеки должны еще и обновлять StackMapTable. Насколько известно автору, в настоящий момент этот атрибут поддерживается только библиотекой ASM 3.0.

Можно, также, возразить, что StackMapTable будет занимать много места. Однако, если добавить его во все классы из rt.jar (“стандартной библиотеки Java”) это увеличит объем всего лишь на 4%. Но в целях сокращения размера дистрибутива JRE, версия классов rt.jar была оставлена 49-й и StackMapTable в ней отсутствует.

Новый верификатор проходит код всего один раз и сложность проверки сокращается до O(n). Конечно, множество верифицируемых программ еще более сокращается, но это лишь требует изменений в компиляторах и никак не сказывается на Java-программах.

В новой версии класс-файла также запрещены инструкции jsr и ret, которые так насолили⁶ авторам верификаторов.

Новый верификатор не проверят классы java.lang.Object, Class, String и Throwable, т.к. они “известны” JVM. Верификация выключена и для байткода сгенерированного через Reflection, что в отладочной версии JVM может быть обратно включено опцией -XX:+VerifyReflectionBytecodes⁷.

Отключить старый верификатор вы можете опцией -XX:-FallOverToOldVerifier. В этом случае, версия класс-файла меньше 50 не будет допускаться.

Кирилл Широков