Верификация программного обеспечения. Текущее состояние и проблемы

• 1 слайд

  Верификация программного обеспечения.
  Текущее состояние и проблемы
  ИВАННИКОВ Виктор Петрович,
  Институт системного программирования РАН (ИСП РАН)
  [e-mail]
  http://ispras.ru/
  16 апреля 2012 года
  

• 2 слайд

  Сложность современного ПО
  2
  

• 3 слайд

  Статистика ошибок
  Количество ошибок на 1000 строк кода (до тестирования) остается практически неизменным за 30 лет
  3
  

• 4 слайд

  Верификация и информационная безопасность программ
  Наличие ошибки в программе часто означает наличие уязвимости
  Технологии верификации одновременно являются средствами оценки и обеспечения информационной безопасности программ
  
  Вывод:
  повышение информационной безопасности программ без развития технологий верификации невозможно
  4
  

• 5 слайд

  Технологии верификации
  Экспертиза
  Тестирование (динамические испытания)
  Аналитическая верификация
  Статический анализ
  Комбинированные подходы
  5
  

• 6 слайд

  Экспертиза
  Поиск ошибок, оценка и анализ свойств ПО человеком (обычно группа 2-5 человек)
  Техники
  Списки важных ограничений и шаблонов ошибок
  Групповые обсуждения
  Производительность : 100-150 строк / час
  Не более 2-3 часов в день
  Результаты : выявляется 50-90% ошибок (обнаруживаемых за все время жизни ПО)
  Нужны настоящие эксперты, программисты с менее чем 10-летним стажем могут участвовать лишь как обучающиеся
  6
  

• 7 слайд

  Тестирование
  Оценка корректности системы по ее работе в выбранных ситуациях, с определенными данными
  Техники:
  Шаблоны сценариев, перебор и фильтрация
  Синтез тестов по структуре реализации или модели
  Производительность : сильно зависит от целей, техники, опыта и пр.
  Microsoft : производительность разработки тестов и тестирования примерно такая же, как у создателей кода, 10 строк/час
  Результаты : выявляется 30-80% ошибок
  Часто используется неопытный персонал, что отрицательно сказывается на качестве
  7
  

• 8 слайд

  Пример : проект DMS (ИСП РАН)
  Разработка тестов для ОС телефонного коммутатора Nortel Networks с использованием формальных методов
  Размер системы : 250 000 строк, 230 интерфейсных функций
  Трудоемкость : ~ 10 человеко-лет
  Результаты:
  Тестовый набор использовался для проверки всех новых версий ОС
  > 300 ошибок в системе с заявленной надежностью 99.9999%
  12 ошибок, требующих холодного рестарта
  ~ 50% всех ошибок найдены в ходе экспертизы
  Остальные выявлены тестами, сгенерированными из формальных спецификаций и нацеленными на их покрытие
  8
  

• 9 слайд

  Показатели качества тестирования
  Метрики тестового покрытия
  Функциональности программы и требований
  Структуры кода: строк, ветвлений, комбинаций условий в ветвлениях
  Для адекватной оценки нужно сочетание нескольких метрик
  Примеры достигаемого тестового покрытия :
  Обычное коммерческое ПО : 15-20% ветвлений в коде
  Системное ПО : 60-80% ветвлений в коде
  Тесты на базе формальных моделей : 70-80% ветвлений в коде
  Аналитическая верификация : 100% ветвлений в коде
  9
  

• 10 слайд

  Аналитическая верификация
  Формальное описание семантики программы и требований и доказательство выполнения требований
  Техники:
  Метод Флойда (дедуктивный метод)
  Provers, solvers, интерактивные инструменты
  Инструменты:
  Мировые лидеры: PVS, Isabelle/HOL, Frama-C
  Примеры приложений: микропроцессоры, ядро операционной системы seL4
  Опыт ИСП РАН: практикум по верификации с помощью Frama-C (~ 100 человеко-часов на программу размером порядка 100 строк)
  10
  

• 11 слайд

  Пример: верификация ядра ОС seL4
  Ядро встроенной ОС seL4
  8700 строк на C, 600 строк на ассемблере
  Для реализации ~2.5 человеко-года
  Верификация
  200 000 строк формальной модели
  Инструмент: Isabelle/HOL
  Трудоемкость – 20 человеко-лет (12 чел.)
  Доказано ~10000 лемм
  11
  

• 12 слайд

  
  Статический
  анализ
  программ
  
  12
  

• 13 слайд

  f(char * p)
  {char s[6];
  strcpy(s,p);
  }
  main1 ()
  {f(“hello”);
  }
  main2 ()
  {f(“privet”);
  }
  
  \0
  o
  l
  l
  e
  h
  t
  \0
  e
  v
  i
  r
  p
  Стек после выполнения функции f, вызванной из main1
  массив s
  Стек после выполнения функции f, вызванной из main2
  В случае main2 адрес возврата перезапишется и управление будет передано не на main2, а на другой участок кода
  адрес возврата
  На место адреса main2 записали лишний байт
  Адрес main1
  Простейший пример
  13
  

• 14 слайд

  Альтернативы решения
  Тестирование
  Проверки времени выполнения
  Статический анализ программы
  Смешанный
  
  14
  

• 15 слайд

  Можно использовать специальные функции с дополнительными параметрами – ограничениями сверху на объем записываемой информации. Например, вместо strcpy(a,b) использовать strncpy(a,b,n), где n-максимальное количество переписываемых символов
  Вставка проверок подразумевает инструментацию исходного кода и так как такие проверки должны присутствовать во всех потенциально опасных местах, инструментированный код может работать на порядок медленнее исходного
  
  f(char * p)
  {char s[10];
  strcpy(s,p);
  }
  f(char * p)
  {char s[10];
  if (strlen(p)<10)
  strcpy(s,p);
  }
  f(char * p)
  {char s[10];
  strncpy(s,p,10);
  }
  Динамические проверки
  15
  

• 16 слайд

  От динамической защиты к статическому обнаружению
  Даже в случае минимизации количества проверок инструментированный код работает гораздо медленнее исходного
  Среди вставляемых проверок много «бесполезных», то есть тех, которые проверяют заведомо истинные условия
  Необходимо статически обнаружить в тексте программы только те места, в которых действительно возможно нарушение системы защиты
  16
  

• 17 слайд

  Цели статического анализа –
  выявление дефектов в программах
  Дефекты (ситуации в исходном коде) могут приводить к:
  Уязвимостям ⃰ защиты
  Потере стабильности работы программы
  
  
  ⃰Уязвимость защиты (security vulnerability) – ошибка в тексте программы, которая позволяет пользователю при некоторых сценариях использования программы обходить средства разграничения прав доступа программы или ОС, в которой программа выполняется.
  
  17
  

• 18 слайд

  Рассматриваемые виды дефектов
  Переполнение буфера
  Format string: недостаточный контроль параметров при использовании функций семейства printf/scanf
  Tainted input: некорректное использование непроверяемых на корректность пользовательских данных
  Разыменование нулевого указателя
  Утечки памяти
  Использование неинициализированных данных
  
  
  18
  

• 19 слайд

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

• 20 слайд

  Первое поколение анализаторов
  Flowfinder, ITS4, RATS, Pscan (распространяются бесплатно)
  CodeSurfer (инструмент для обнаружения уязвимостей на базе CodeSurfer’а недоступен)
  FlexeLint (продается на рынке), Splint (распространяется бесплатно)
  20
  

• 21 слайд

  Недостатки первого поколения
  Большое число ложных срабатываний – 90% и выше
  Пропуск реальных уязвимостей
  Необходима ручная проверка результатов работы, которая требует привлечения значительных ресурсов (материальных, людских, временных)
  21
  

• 22 слайд

  Современные анализаторы
  Coverity Prevent
  
  Klockwork Insight
  
  Svace
  22
  

• 23 слайд

  Наш подход
  Для обнаружения уязвимостей мы предлагаем применять следующее:
  
  Межпроцедурный data-flow анализ с итерациями на внутрипроцедурном уровне
  Анализ указателей
  Анализ интервалов и значений целочисленных объектов
  Контекстно-зависимый (использующий индивидуальные входные параметры для каждой точки вызова) анализ
  23
  

• 24 слайд

  Целью целочисленного анализа программы является получение необходимой информации о значении целочисленных атрибутов объектов программы (значение переменной, размер массива и т.д.)
  Чем точнее и полнее представляются целочисленные значения, тем точнее возможно проведение поиска уязвимостей
  void f(int i)
  { char p[5];
  int a;
  if (i>0)
  a=4;
  else
  a=3;
  p[a]=0;
  }
  
  
  i>0
  a=4
  a=3
  p[a]=0
  yes
  no
  Value(a)=3
  Value(a)=4
  Value(a)=[3..4]
  - нет уязвимости
  Целочисленный анализ на основе интервалов
  24
  

• 25 слайд

  Потеря точности в некоторых случаях.
  Отсутствие информации о связях между переменными: в случае анализа на основе интервалов в последней инструкции примера будет обнаружена ложная уязвимость.
  void f(int i)
  { char p[5];
  int a,b,c;
  if (i>0)
  a=0;
  else
  a=1;
  b=a+4;
  c=b-a;
  p[c]=0
  }
  
  
  
  i>0
  a=0
  a=1
  b=a+4
  yes
  no
  Value(a)=1
  Value(a)=0
  Value(a)=[0..1]
  c=b-a
  p[c]=0
  Value(a)=[0..1]
  Value(b)=[4..5]
  Value(c)=[3..5]
  Value(a)=[0..1]
  Value(b)=[4..5]
  Value(a)=[0..1]
  Value(b)=a+4
  Value(a)=[0..1]
  Value(b)=a+4
  Value(c)=4
  Size(p)=5
  Value(c)<Size(p)
  Value(c) может быть равным Size(p) => ложная ошибка
  Недостатки целочисленного
  анализа интервалов
  25
  

• 26 слайд

  Необходимость межпроцедурного анализа
  f(char *p, char *s)
  {strcpy(p,s); // произойдет копирование 6 байт, включая //конец строки
  }
  
  main()
  {char *p;
  p=malloc(5);
  f(p,”hello”);
  }
  В приведенном примере указатель на объект размером 5 байт передается в функцию f, поэтому без межпроцедурного анализа эта информация никаким образом не попадет на вход вызову функции strcpy и ошибку не зафиксируется
  26
  

• 27 слайд

  Необходимость анализа указателей
  
  …
  char a[10];
  char * p;
  p=a;
  p[10]=0;
  …
  
  Для данного примера в случае отсутствия анализа указателей невозможно сделать никаких предположений о размере массива, на который указывает p и, следовательно, невозможно определить наличие ошибки
  27
  

• 28 слайд

  Спецификация окружения
  char* strcpy(char *dst, const char *src) {
  char d1 = *dst;//dst и src
  char d2 = *src;// разыменовываются в функции
  
  //необходимо проверить на корректность src
  //(в случае пользовательского ввода)
  sf_set_trusted_sink_ptr(src);
  
  //содержимое src копируется в dst
  sf_copy_string(dst, src);
  
  //возвращается входной параметр
  return dst;
  }
  
  28
  Внутренние обработчики инфраструктуры анализа
  

• 29 слайд

  Схема работы Svace
  Анализируемая программа
  Система сборки
  Файлы с исходным кодом
  Утилита
  перехвата
  Компилятор LLVM-GCC
  или CLANG
  Исходный код
  Измененная командная строка
  Командная строка
  Биткод-файл
  Входные биткод-файлы
  Биткод-файлы
  для исходных
  файлов
  Биткод-файлы
  спецификаций
  библиотек
  Инфраструктура
  анализа
  Детекторы
  Вызовы внутреннего
  интерфейса
  Инструмент статического анализа
  Биткод-файлы
  Исходный код
  Работа с результатами анализа через компонент Eclipse
  Список
  предупреж-дений
  Биткод-файл
  29
  

• 30 слайд

  Построение аннотаций
  Биткод-файлы
  для исходных
  файлов
  Спецификации библиотечных
  функций на языке Си
  Биткод-файлы спецификаций
  библиотек
  Компилятор LLVM-GCC или CLANG
  Функции анализируемой
  программы
  Функции спецификаций
  Построение графа вызовов
  Аннотации
  Анализ
  Анализ*
  *Анализ отдельной функции
  Анализ вызова функции
  Вызов подпрограммы
  Вызов подпрограммы
  30
  

• 31 слайд

  Топологический порядок
  обработки функций
  Граф вызовов функции
  main
  q
  w
  a
  b
  c
  prinf
  strcpy
  Построение топологического порядка функций
  a
  b
  c
  q
  w
  main
  Порядок анализа
  Создание аннотаций библиотечных функций
  printf
  strcpy
  a
  q
  b
  Анализ функции ‘c’
  Аннотации:
  Межпроцедурный анализ (интервальный, tainted, нулевых указателей, алиасов и др.)
  31
  

• 32 слайд

  Время анализа
  * Не учитывается время компиляции проекта
  32
  

• 33 слайд

  Сравнение с Coverity Prevent
  33
  

• 34 слайд

  Текущее состояние
  Анализ программ на Си\Си++.
  Информация об исходном коде собирается при помощи компилятора LLVM-GCC (или CLANG)
  Нет ограничений на размер программы (линейная масштабируемость)
  Полностью автоматический анализ
  Поддержка пользовательских спецификаций функций
  Набор спецификаций стандартных библиотечных функций (Си, Linux)
  Набор подсистем поиска различных дефектов (переполнение буфера, разыменование нулевого указателя и др.)
  Набор подсистем поиска дефектов расширяем
  Графический пользовательский интерфейс, реализованный в виде расширения среды Eclipse
  
  34
  

• 35 слайд

  Avalanche: Обнаружение ошибок при помощи динамического анализа
  35
  

• 36 слайд

  Динамический и статический анализ кода
  
  Динамический анализ - анализ программы во время выполнения
  Статический анализ - анализ без выполнения программы
  
  36
  

• 37 слайд

  Обнаружение ошибок при помощи анализа программ
  Динамический анализ
  Требуется набор входных данных и/или среда выполнения
  Высокие требования к ресурсам
  Высокая точность обнаружения
  Статический анализ
  Работает на исходном или бинарном коде
  Анализ абстрактной модели
  Хорошая масштабируемость
  Ложные срабатывания
  
  37
  

• 38 слайд

  Valgrind
  Фреймворк динамической инструментации
  Обнаруживаемые ошибки:
  Утечки памяти
  Ошибки работы с динамической памятью
  Неиницилизированные данные
  Ошибки в многопоточных программах
  38
  

• 39 слайд

  Valgrind: общая схема работы
  Команды
  CPU
  Базовый блок
  Valgrind IR
  Плагин
  Инструментация
  Базовый блок’
  Valgrind IR
  Команды’
  CPU
  Внутреннее представление
  команд Valgrind – абстрактная
  RISC машина
  39
  

• 40 слайд

  Трасса выполнения программы
  40
  

• 41 слайд

  Трасса выполнения программы
  41
  

• 42 слайд

  Трасса выполнения программы
  42
  

• 43 слайд

  Трасса выполнения программы
  43
  

• 44 слайд

  Работы в этой области
  EXE tool, Stanford University - символические вычисления
  SAGE framework, Microsoft Research - white-box fuzz testing
  KLEE, LLVM project
  44
  

• 45 слайд

  Пример
  char *names[] = { “one”, “two”, ...};
  
  char buf[3];
  fread(buf, 3, 1, f); // чтение 3-х байт из файла
  
  if (buf[0] == 1) { // ветвление #1
  int index;
  if (buf[1] + buf[2] > 0) { // ветвление #2
  index = ...;
  }
  name = names[index]; // index не инициализирован
  // выход за границы массива
  ...
  } else {
  ...
  }
  45
  

• 46 слайд

  Пример
  fread(buf, 3, 1, f)
  buf[0] == 1
  buf[1] + buf[2] > 0
  x1, x2, x3: byte
  
  x1 = 1
  x2 + x3 > 0
  x1 = 1
  x2 = 100
  x2 = 200
  46
  

• 47 слайд

  Пример
  fread(buf, 3, 1, f)
  buf[0] == 1
  buf[1] + buf[2] > 0
  Система уравнений:
  
  x1, x2, x3: byte
  
  ¬(x1 = 1)
  x1 = 2
  Решение:
  47
  

• 48 слайд

  Пример
  fread(buf, 3, 1, f)
  buf[0] == 1
  buf[1] + buf[2] > 0
  Система уравнений:
  
  x1, x2, x3: byte
  
  x1 = 1
  ¬(x2 + x3 > 0)
  x1 = 1
  x2 = 0
  x3 = 0
  Решение:
  48
  

• 49 слайд

  Avalanche
  Отслеживает поток помеченных (потенциально опасных) данных
  Изменяет входные данные, чтобы спровоцировать ошибку, или обойти новые части программы
  Обнаруживает критические ошибки - разыменование нулевого указателя, деление на ноль, неинициализированные данные, ошибки работы с памятью
  Генерирует набор входных данных для каждой найденной ошибки
  49
  

• 50 слайд

  Входные данные
  Входные данные
  \
  Avalanche: итерация
  Tracegrind
  Трасса
  Управляющий модуль
  Трасса’
  STP
  Решение
  Управляющий модуль
  Входные данные
  Covgrind
  Метрики
  Управляющий модуль
  Управляющий модуль
  Управляющий модуль
  50
  

• 51 слайд

  Управляющий модуль Avalanche
  Координация работы других компонентов
  Обход различных путей исполнения программы, инвертирование условий
  Поддержка параллельного и распределенного анализа
  51
  

• 52 слайд

  Tracegrind
  Отслеживает поток помеченных данных в программе
  Все данные прочитанные из внешних источников (файлы, сетевые сокеты, аргументы коммандной строки, переменные окружения)
  Переводит трассу выполнения в булевскую формулу (STP утверждения)
  52
  

• 53 слайд

  Tracegrind
  Моделирует оперативную память, регистры и временные переменные при помощи бит-векторов
  Моделирует комманды при помощи операций и утверждений STP
  53
  

• 54 слайд

  Covgrind
  Вычисление метрики покрытия кода программы (количество новых ББ покрытых на текущей итерации)
  Перехват сигналов (обнаружение критических ошибок)
  Обнаружение ошибок работы с памятью при помощи Memcheck
  Обнаружение бесконечных циклов при помощи таймаутов
  54
  

• 55 слайд

  STP - Simple Theorem Prover
  SAT решатель (основан на MiniSat)
  Проект с открытым исходным кодом
  Поддерживает бит-векторы, широкий набор операций
  55
  

• 56 слайд

  Проект
  Опубликован на Google Code
  http://code.google.com/p/avalanche
  Лицензии:
  Valgrind и Memcheck - GPL v2
  STP - MIT license
  Драйвер Avalanche, Tracegrind, Covgrind - Apache license
  56
  

• 57 слайд

  Avalanche: возможности
  Поддержка клиентских сетевых сокетов
  Поддержка переменных окружения и параметров коммандной строки
  Поддержка платформ х86/Linux и amd64/Linux, ARM/Linux, Android
  Поддержка параллельного и распределенного анализа
  57
  

• 58 слайд

  Результаты
  Более 15-ти ошибок на проектах с открытым исходным кодом
  
  Ошибки подтверждены и/или исправлены разработчиками
  Null Pointer Dereference (разуменование нулевого указателя) = NPD
  Division By Zero (деление на ноль) = DBZ
  Unhandled Exception (необработанная исключительная ситуация) = UE
  Infinite Loop (бесконечный цикл) = IL
  58
  

• 59 слайд

  Планы на будущее
  Улучшение прозводительности
  Поддержка новых источников входных данных (серверные сетевые сокеты, и т. д.)
  Поддержка новых типов ошибок (многопоточные приложения)
  59
  

• 60 слайд

  UniTESK
  60
  

• 61 слайд

  Случай тестирования отдельной функции:
  Подобрать набор входных (тестовых) данных
  Вычислить ожидаемый результат для каждого из тестовых данных
  А если это трудно или невозможно, например для функции random() ?
  Запустить тест с каждым из тестовых данных, сопоставить результат с ожидаемым
  Принять решение о продолжении или завершении тестирования
  А каков критерий завершения ?
  Разработка теста по-простому
  61
  

• 62 слайд

  Случай тестирования группы функции, класса/объекта, модуля с несколькими интерфейсами (обычно есть переменные состояния и побочный эффект):
  Подобрать набор входных (тестовых) данных для каждой функции
  Вычислить ожидаемый результат для каждого из тестовых данных
  Новая проблема – как учесть побочный эффект?
  Вызвать каждую функцию с каждым из тестовых данных в различных состояниях модуля, сопоставить результат с ожидаемым
  Какие состояния считать различными, как прийти в нужное состояние (построить тестовую последовательность), если побочный эффект вычислить невозможно?
  Принять решение о продолжении или завершении тестирования
  А каков критерий завершения ?
  Разработка теста по-простому (2)
  62
  

• 63 слайд

  Типичные размеры тестовых наборов
  Ядро ОС Linux (LTP)
  18 Mbyte (при этом покрывает менее половины строк кода)
  Библиотеки стандарта OS Linux (LSB)
  Более 100 тысяч вариантов
  Более 80 Mbyte
  Для компилятора C (например, ACE или Perennial)
  Более 40-80 тысяч вариантов
  Более 1 Gbyte
  
  63
  Не удивительно, что на тестирование тратиться
  существенная доля усилий (в Майкрософте около 70%),
  а средняя плотность ошибок, которая считается
  приемлемой – 2-3 ошибки на 1 тысячу строк кода.
  
  

• 64 слайд

  Решения UniTESK
  Исходная точка построения теста – формализация программного контракта в форме пред- и пост-условий
  пред- и пост-условия определяют тестовые оракулы и критерии полноты покрытия
  Тестовую последовательность конструировать не вручную, а на основе интерпретации модели теста
  Нотации – максимально приближенные к языкам программирования
  
  64
  

• 65 слайд

  Формализация требований
  Выделение модельного состояния
  Описание формального контракта операций
  Предусловия – задают область определения
  Постусловия – задают основные ограничения на результаты работы операций
  Инварианты – ограничения целостности данных, общая часть всех пред- и постусловий
  Аксиоматическая часть контракта (если нужно)
  65
  

• 66 слайд

  Простой пример спецификации в JavaTESK
  public specification class SqrtSpecification {
  public specification double sqrt(double x) {
  pre { return x >= 0; }
  post {
  branch SingleCase;
  return sqrt * sqrt == x;
  }
  
  public specification int sqrt(int x) {
  pre { return x >= 0; }
  post {
  branch SingleCase;
  return sqrt * sqrt <= x
  && (sqrt + 1) * (sqrt + 1 ) > x ;
  }
  }
  }
  
  66
  

• 67 слайд

  Общая схема тестирования
  Тестовая система
  Тестируемая система
  
  
  
  
  
  
  
  Отчеты
  Тестовый сценарий
  Тестовые
  данные
  Ожидаемые
  результаты,
  критерии
  полноты
  67
  

• 68 слайд

  Общая схема.
  Данные, оракул, покрытие
  Пред-условия,
  итераторы
  Пост-условия
  Тестовая система
  Отчеты
  Тестовый сценарий
  Тестовые
  данные
  Ожидаемые
  результаты,
  критерии
  полноты
  Тестируемая система
  
  
  
  
  
  
  
  68
  

• 69 слайд

  Общая схема.
  Тестовый сценарий
  описать
  и обойти КА
  обходить и
  строить КА налету
  Тестовая система
  Отчеты
  Тестовый сценарий
  Тестовые
  данные
  Ожидаемые
  результаты,
  критерии
  полноты
  Тестируемая система
  
  
  
  
  
  
  
  написать
  вручную
  Варианты:
  69
  

• 70 слайд

  Общая схема UniTESK
  Модель состояния
  Обходчик автоматов
  Оракулы
  Генератор
  Итераторы данных
  Метрика покрытия
  Тестируемая система
  Генерация тестовой последовательности налету
  Предусловия-
  фильтры
  Постусловия
  
  
  
  
  
  
  
  Оракул
  Отчеты
  70
  

• 71 слайд

  Применение UniTESK
  Операционные системы
  Ядро ОС телефонной станции 1994-1997
  Linux Standard Base2005-2010
  Тестовый набор для ОС 2000 (НИИСИ)2005-...
  Протоколы
  IPv6 Microsoft Research2000-2001
  Мобильный IPv6 (в Windows CE 4.1)2002-2003
  IPv6 Октет2002
  Тестовый набор для IPsec2004-2008
  Тестовый набор для SMTP2010
  Оптимизаторы компиляторов Intel2001-2003
  Оптимизатор трансляции графических моделей2005
  Информационные системы
  Компоненты CRM-системы2004
  Биллинговая система и EAI2005-…
  Микропроцессоры
  Процессоры Комдив 64 (НИИСИ)2006-...
  Компоненты процессоров и шин (МЦСТ)2010-...
  
  71
  

• 72 слайд

  Спасибо!
  72