Верификация байт- кода в среде смарт- карт: использование криптографических методов К. Н. Хюппенен Кафедра информатики и математического обеспечения ПетрГУ 20 июня 2003 г.

2 Содержание Загрузка апплетов на смарт-карты Алгоритм верификации байт-кода компании Sun Разделенная модель верификации байт-кода Описание разработанного прототипа

3 Современная архитектура Java Card Ресурсы микросхемы Рабочая среда (ОС) Виртуальная машина API Приложение a Приложение b Приложение c Приложение...

4 Загрузка апплета JCVM Системные ресурсы Контекст s Собственный код Апплет Верификация Контекст 2 Требования Апплет типа 2 Контекст 1 Апплет типа 1 Собственный код Апплет типа s

5 Верификация байт-кода Верификация байт-кода Java: –Статический и структурный анализ загружаемого пакета –Проверяет, что байт-код пакета оперирует верными типами данных. Верификация байт-кода – это крайне важный элемент защиты: –Предотвращает нелегальные операции: Подделка ссылок на объекты. Неверное преобразование ссылок. –Созданные со злым умыслом апплеты способны: Полностью считать память карты. Получить доступ к частным данным.

6 Как работает верификация Что такое верификатор? –Это программа, которая определяет, является ли апплет «безопасным» или «небезопасным». Что значит «безопасный»? –Апплет удовлетворяет набору свойств, которые необходимы, но не достаточны для обеспечения реальной защиты.

7 Как работает верификация Тесты, которые могут осуществляться: –Переменные имеют верные типы во всех ситуациях Нелегальные преобразования типов (напр., чтение целочисленного типа как ссылки на объект) не происходят. –Код является замкнутым Команды перехода не выводят интерпретатор за границы метода. –Стек ограничен Не возникает переполнение или незагруженность стека. –Объекты используются безопасно Все переменные инициализируются перед использованием. –И прочие...

8 Виртуальная машина Java Card Имеет стековую архитектуру Регистры Регистр 3 Регистр 2 Регистр 1 Регистр 0 Системная область Стек операндов Ячейка стека 0 Ячейка стека 2 Ячейка стека 1 Стековый кадр Куча Объект 67 Объект 42 Объект 2 Объект 3 Ссылка

9 Работа алгоритма верификации Sun 0 iload_1. L i i ? 1 iload_2 ? ? ? ? ? 2 if_icmpne 12 ? ? ? ? ? 5 iload_1 ? ? ? ? ? 6 iload_2 ? ? ? ? ? 7 iadd ? ? ? ? ? 8 istore_3 ? ? ? ? ? 9 goto 16 ? ? ? ? ? 12 iload_1 ? ? ? ? ? 13 iload_1 ? ? ? ? ? 14 imul ? ? ? ? ? 15 istore_3 ? ? ? ? ? 16 iload_3 ? ? ? ? ? 17 ireturn ? ? ? ? ? Стек Регистры

10 0 iload_1. L i i ? 1 iload_2 i L i i ? 2 if_icmpne 12 ? ? ? ? ? 5 iload_1 ? ? ? ? ? 6 iload_2 ? ? ? ? ? 7 iadd ? ? ? ? ? 8 istore_3 ? ? ? ? ? 9 goto 16 ? ? ? ? ? 12 iload_1 ? ? ? ? ? 13 iload_1 ? ? ? ? ? 14 imul ? ? ? ? ? 15 istore_3 ? ? ? ? ? 16 iload_3 ? ? ? ? ? 17 ireturn ? ? ? ? ? Стек Регистры Работа алгоритма верификации Sun

11 0 iload_1. L i i ? 1 iload_2 i L i i ? 2 if_icmpne 12 i,i L i i ? 5 iload_1 ? ? ? ? ? 6 iload_2 ? ? ? ? ? 7 iadd ? ? ? ? ? 8 istore_3 ? ? ? ? ? 9 goto 16 ? ? ? ? ? 12 iload_1 ? ? ? ? ? 13 iload_1 ? ? ? ? ? 14 imul ? ? ? ? ? 15 istore_3 ? ? ? ? ? 16 iload_3 ? ? ? ? ? 17 ireturn ? ? ? ? ? Стек Регистры Работа алгоритма верификации Sun

12 0 iload_1. L i i ? 1 iload_2 i L i i ? 2 if_icmpne 12 i,i L i i ? 5 iload_1. L i i ? 6 iload_2 ? ? ? ? ? 7 iadd ? ? ? ? ? 8 istore_3 ? ? ? ? ? 9 goto 16 ? ? ? ? ? 12 iload_1. L i i ? 13 iload_1 ? ? ? ? ? 14 imul ? ? ? ? ? 15 istore_3 ? ? ? ? ? 16 iload_3 ? ? ? ? ? 17 ireturn ? ? ? ? ? Стек Регистры Работа алгоритма верификации Sun

13 Разделенная модель верификации байт-кода Терминал используется как внешний источник памяти. Для защиты данных применяются криптографические методы. Требования к памяти сокращаются до O(S log S), где S – количество байт- кодов в методе. Верификация производится на карте

14 Постановка задачи Исследовать применимость модели разделенной верификации байт-кода к технологии Java Card Реализовать прототип верификатора Провести тесты и измерения

15 Разделенная модель верификации Карта Счетчики Терминал Хранилище кадров Frame 0: MAC, PC=0, un/changed bit, types of variables Frame 0: MAC, PC=0, un/changed bit, types of variables Frame 0: MAC, PC=0, un/changed bit, types of variables Frame 0: MAC, PC=0, un/changed bit, types of variables Frame i: MAC, PC=i, un/changed bit, types of variables Frame i: MAC, PC=i, un/changed bit, types of variables Данные Процедура верификации со стороны терминала Программа Запись кадра Кадр i Чтение кадра проверить Процедура верификации со стороны карты подписать С[i] C[i]++ C[i] Входящий кадрИсходящий кадр MAC-функция f с эфемерным ключом k

16 Оптимизации модели Экспорт счетчиков на терминал –Дальнейшее сокращение объема требуемой для работы оперативной памяти. Неявные запросы –Уменьшение объема передаваемых данных и снижение нагрузки на карту.

17 Архитектура прототипа Проверяемый апплет Апплет, исполняемый на терминале Апплет, исполняемый на карте Содержимое пакета Команды Принять/отвергнуть Кадры

18 Тестирование прототипа Оценен объем требуемой памяти Оценен объем передаваемых данных Проведены измерения времени работы программы Проведено тестирование на реальных смарт-картах Доказана применимость модели разделенной верификации

19 Результаты работы Разделенная модель верификации байт-кода исследована и адаптирована к технологии Java Card; Предложено несколько оптимизаций модели; Реализован прототип верификатора, экспериментально подтверждающий применимость данного метода.