Способ генерации баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации

Изобретение относится к средствам автоматизации обучения и научных исследований и может быть использовано в интерактивных системах в процессе верификации программного обеспечения (ПО) распределенных вычислительных комплексов. Технический результат заключается в расширении функциональных возможностей процессов верификации ПО. В способе и устройстве обеспечивают полную управляемость и наблюдаемость основных процессов проверки исходного кода ПО, совмещают процессы ввода и обработки исходного кода ПО по зависимым или независимым интерфейсным каналам. Участки или точки уязвимости исходного кода ПО определяют на основе преобразования исходного кода ПО во внутреннее представление, которое хранят в виде баз знаний, а точки или участки уязвимости исходного кода ПО определяют на основе автоматического составления и решения соответствующих систем уравнений. При этом в процессе верификации осуществляют синтаксическую подсветку на экране участков уязвимости исходного кода ПО, используя граф операторов исходного кода ПО во внутреннем представлении инструкций языка программирования. 2 н. и 7 з.п. ф-лы, 39 ил.

 

Изобретение относится к средствам автоматизации обучения и научных исследований и предназначено для использования в интерактивных системах автоматизации научно-исследовательских работ в процессе верификации (проверки, тестирования и т.п.) программного обеспечения (ПО) распределенных вычислительных комплексов (РВК).

Известны интерактивные системы автоматизации основных процессов научных исследований в процессе верификации (проверки, тестирования и т.п.) ПО РВК (см. например, DE 10247914 A1 (BOSCH GMBH ROBERT (DE)) 22.04.2004, G 09 В 9/08; DE 10141737 A1 (DAIMLER CHRYSLER AG (DE)) 03.04.2003, G 09 В 9/08; H 04 L 9/30; H 04 L 12/40; B 60 R 16/02; FR 2559599 A1 (GAUER BERNARD (FR)) 16.08.1985, G 09 В 9/08; GB 2366640 A (IBM) 13.03.2002 G 06 F 1/00; GB 2283341 (SOPHOS PLC (GB)) 03.05.1995 G 06 F 1/00; JP 2004302584 A (NIPPON ELECTRIC CO) 28.10.2004, G 09 В 9/08; JP 2004164617 A (MICROSOFT CORP) 10.06.2004, G 09 В 9/08). В основе работы вышеперечисленных систем использованы способы динамического или статического тестирования ПО. Вышеперечисленные технические решения позволяют для некоторых классов ПО избежать их некорректного исполнения, однако существенным недостатком таких решений является сложность выявления скрытых уязвимостей в исходном коде (ИК) ПО РВК, а также невозможность гарантировать правильность полученных результатов на ранних стадиях проектирования ПО РВК. При этом технические реализации статического способа анализа ПО, как правило, представляют различные модификации лексических сканеров ИК ПО и не позволяют осуществить глубокий анализ ни хода выполнения ПО РВК, ни содержания используемой памяти (например, массивов, переменных и т.п.).

В этой связи главный недостаток известных технических решений предопределен тем, что процессы верификации ПО РВК, как правило, представляют ненаблюдаемые/неуправляемые во времени процессы. При этом сам процесс поиска уязвимости в ИК ПО представляет в большей степени искусство, нежели какую-либо формализованную процедуру. При этом низкая производительность данного класса технических решений обусловлена потерей времени, затрачиваемого на формирование тестовых наборов данных, выбора количественных и качественных характеристик, позволяющих оценить уязвимость ИК ПО, определения входных данных определенных типов, в особенности строкового или процедурного типа, являющиеся наиболее распространенными в практике разработки ПО РВК.

Достижению требуемого технического результата во всех приведенных аналогах, включая соответствующий способ верификации ПО, препятствует то, что ни одно из них не может обеспечить полную наблюдаемость/управляемость за динамикой процесса генерации баз знаний на основных этапах верификации ИК ПО РВК систем автоматизации научно-исследовательских работ.

Задачей изобретения является расширение функциональных возможностей интерактивных процессов выполнения научно-исследовательских работ на основе автоматизации основных процессов генерации баз знаний для верификации ПО РВК, а также повышение точности и достоверности выявления уязвимостей в ИК ПО на основных этапах проектирования и сопровождения (аудита) программного кода сложных вычислительных систем и сетей.

Для решения поставленной задачи предложен способ генерации баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов и устройство для его реализации.

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

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

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

Точки или участки уязвимости исходного кода ПО определяют на основе автоматического составления и решения линейных систем уравнений.

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

В качестве независимых каналов используют интерфейс последовательного порта или сетевой интерфейс.

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

При этом генерацию баз знаний осуществляют на основе использования аннотаций внешних функций ИК ПО РВК.

База знаний представляет набор правил или моделей протоколов верификации ИК ПО, обеспечивающих поддержку интерактивных процессов поиска уязвимости ПО.

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

Диагностику процесса верификации ИК ПО осуществляют на основе измерения длительности выполнения основных этапов (циклов и т.п.) поиска уязвимости и сопоставления полученных значений с ранее предписанными или предсказанными оценками показателя (степени, энтропии и т.п.) критичности уязвимости ИК ПО.

Визуальный язык в виде раскрасок графа максимально приближен к профессиональному языку специалистов в прикладной области.

Для реализации предлагаемого способа генерации баз знаний предлагается интерактивное программируемое устройство (ИПУ) для систем верификации программного обеспечения распределенных вычислительных комплексов (СВПО РВК), содержащее аппаратно-программный блок (АПБ) лексического и семантического анализа/разбора, АПБ преобразования кода, АПБ анализа кода; АПБ процессорного управления, видео адаптер, интерфейсы жестких, гибких и оптических дисков, интерфейс последовательного порта, сетевой интерфейс и системную память, которые объединены системной шиной, при этом системная память содержит постоянное запоминающее устройство (ROM) и оперативное запоминающее устройство (RAM/ОЗУ), в ячейках оперативной памяти и жестких дисков размещают/записывают операционные системы, прикладные программы, базы данных и базы знаний, которые содержат листинги исходных программ, грамматику языка программирования (например, грамматику языка программирования Си), правила преобразования дерева разбора листинга программы, дерево разбора листинга программы, таблицу типов языка программирования, аннотации внешних функций, включающие их грамматику и семантику, код программ на языке внутреннего представления, условия корректности языка внутреннего представления исходного кода программы, условия проверки корректности подозрительных точек исходного кода программы, информационную базу, содержащую системы ограничений в виде алгебраических уравнений и неравенств, отчеты об обнаруженных уязвимостях программного кода, включающие:

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

указание причины переполнения буфера запоминающего устройства - значения исходных переменных, приводящих к возникновению уязвимости исходного кода программного обеспечения;

показатель или степень критичности обнаруженной уязвимости исходного кода программного обеспечения;

указание на перечень правил или алгоритмов для устранения уязвимости исходного кода программного обеспечения.

При этом аппаратно-программный блок процессорного управления, обеспечивающий синхронизацию основных режимов интерактивной верификации программного обеспечения распределенных вычислительных комплексов, содержит последовательно соединенные блок нормирующих преобразователей (БНП), модуль коммутатора, модуль аналого-цифрового преобразователя (АЦП), модуль формирования статических координат графоаналитического растра (МФСКГАР), блок видеоконтроля (БВ), импульсный регулятор (ИР) и модуль формирования динамической развертки графоаналитического растра (МФДРГАР), первый и второй информационные входы/выходы которого соединены соответственно с управляющими входами модуля коммутации и аналого-цифрового преобразователя, а третий, четвертый, пятый, шестой, седьмой и восьмой - с вторым, третьим, четвертым, пятым, шестым и седьмым информационными входами/выходами МФСКГАР, при этом второй вход блока видеоконтроля объединен с седьмым информационным входом/выходом МФСКГАР и восьмым информационным входом/выходом МФДРГАР.

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

При этом оптический коэффициент пропускания маски, через которую проходит оптический сигнал, имеет одно и то же значение для точек одной гипотезы/энтропии о состоянии уязвимости ИК ПО и различное для других значений гипотез.

Маска изготовлена так, что в пространстве ее координат (X, Y, Z) выделены области уязвимости ИК ПО и соответствующие значения могут быть определены на основе оценки степени уязвимости ИК ПО ВРК.

В качестве оценки степени уязвимости ИК ПО ВРК могут быть использованы значения энтропии состояния верифицируемого ИК ПО.

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

Предлагаемое изобретение поясняется чертежами.

На фиг.1 приведена структура интерактивного программируемого устройства (ИПУ) для систем верификации программного обеспечения распределенных вычислительных комплексов (СВПО РВК), содержащая аппаратно-программный блок (АПБ) лексического и семантического анализа/разбора (АПБ-А), АПБ преобразования кода (АПБ-В), АПБ анализа кода (АПБ-С), АПБ процессорного управления (АПБ-У), видеоадаптер, интерфейсы жестких, гибких и оптических дисков, интерфейс последовательного порта, сетевой интерфейс и системную память, которые объединены системной шиной, при этом системная память содержит постоянное запоминающее устройство (ROM) и оперативное запоминающее устройство (RAM/ОЗУ), в ячейках оперативной памяти и жестких дисков размещают/записывают операционные системы, прикладные программы, базы данных и базы знаний, которые содержат листинги исходных программ (D1), грамматику языка программирования (D2) (например, грамматику языка программирования Си), правила преобразования дерева разбора листинга программы (D3), дерево разбора листинга программы (D4), таблицу типов языка программирования (D5), аннотации внешних функций, включающие их грамматику и семантику (D6), код программ на языке внутреннего представления (D7), условия корректности языка внутреннего представления исходного кода программы (D8), условия проверки корректности подозрительных точек исходного кода программы (D9), информационную базу (D10), содержащую системы ограничений в виде алгебраических уравнений и неравенств, отчеты об обнаруженных уязвимостях программного кода (D11), включающие:

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

указание причины переполнения буфера запоминающего устройства - значения исходных переменных, приводящих к возникновению уязвимости исходного кода программного обеспечения;

показатель или степень критичности обнаруженной уязвимости исходного кода программного обеспечения;

указание на перечень правил или алгоритмов для устранения уязвимости исходного кода программного обеспечения.

На фиг.2 приведен пример реализации аппаратно-программного блока (АПБ) лексического и семантического анализа/разбора (АПБ - А), в котором приняты следующие обозначения:

Обозначение	Описание
D1	База данных, содержащая листинги исходных программ (D1): набор файлов с исходными текстами (листингами) анализируемой программы
Вход 1: чтение файлов листингов программ
D2	База данных, содержащая грамматику языка программирования (D2): грамматика языка (правила лексического и синтаксического разбора)
Вход 1: чтение правил грамматики языка
D3	База знаний, содержащая правила преобразования дерева разбора листинга программы (D3): правила преобразования дерева
Вход 1: чтение правил преобразования дерева разбора
D4	База данных дерева разбора листинга программы (D4): дерево разбора после выполнения части А
Вход 1: сохранение дерева разбора
D5	База данных, содержащая таблицу типов языка программирования (D5): таблица типов после работы АПБ-А
Вход 1: сохранение таблицы типов
A.1	Блок проверки условия: остались ли листинги программ для разбора?
	Выход 1: переход в случае истинности условия
Выход 2: переход в случае ложности условия
А.2	Вызов процедуры PARSE FILE аппаратно-программного модуля А1 ”Лексический и синтаксический разбор” для разбора очередного листинга программы. Работа данного модуля раскрыта на схеме, изображенной на фиг.3.
	Вход 1: прием управляющего сигнала
	Выход 1: обращение на чтение к данным - файлам листингов программ
	Выход 2: обращение на чтение к данным - грамматике языка программирования
	Выход 3: обращение на запись к данным - дереву разбора листингов программ после выполнения модуля А1
	Выход 4: обращение на запись к данным - таблице типов А.5 после выполнения модуля А1
Выход 5: передача управления и полученных результатов (дерево разбора и таблица типов) в следующий этап обработки А.3.
А.3	Вызов процедуры SIMPLIFY SYNTAX TREE аппаратно-программного модуля А2 ”Преобразование дерева разбора листингов программ к виду, пригодному для перевода во внутреннее представление” для обработки результатов выполнения результатов работы этапа А.2. Пример реализации процедуры SIMPLIFY SYNTAX TREE аппаратно-программного модуля А2 раскрыт на фиг.4.
	Вход 1: передача управления и получение результатов выполнения процедуры PARSE FILE аппаратно-программного модуля А1
	Выход 1: передача управления на вход А.1
	Выход 2: обращение на чтение к данным - дереву разбора после выполнения аппаратно-программного модуля А1
	Выход 3: обращение на чтение к данным - таблице типов после выполнения аппаратно-программного модуля А1
	Выход 4: обращение на запись к данным - дереву разбора после выполнения - модуля А2
	Выход 5: обращение на запись к данным - таблице типов после выполнения - модуля А2
Выход 6: обращение на чтение к базе данных D3
А.4	Данные - дерево разбора листингов программ после выполнения моду ля А 1.
	Вход 1: обращение из модуля А1
Вход 2: обращение из модуля А2
А.5	Данные - таблица типов после выполнения модуля А1.
	Вход 1: обращение из модуля А1
Вход 2: обращение из модуля А2
А.6	Данные - дерево разбора листингов программ после выполнения модуля А2.
	Вход 1: обращение из модуля А2
Вход 2: обращение из модуля A3
А.7	Данные - таблица типов после выполнения аппаратно-программного
	модуля А2.
	Вход 1: обращение из модуля А2
Вход 2: обращение из модуля A3
А.8	Вызов процедуры MERGE SYNTAX TREES аппаратно-программного модуля A3 ”Поддержка многофайловых проектов”. Пример реализации модуля A3 раскрыт на фиг.7.
	Выход 1: передача управления
	Выход 2: обращение на чтение к данным - дереву разбора после выполнения модуля А2
	Выход 3: обращение на чтение к данным - таблице типов после выполнения модуля А2
	Выход 4: сохранение итоговой таблицы типов
Выход 5: сохранение итогового дерева разбора

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

На фиг.3-7 приведены примеры реализации основных модулей АПБ-А.

На фиг.3 приведен пример реализации модуля А1 АПБ-А. Аппаратно программный модуль А1 обеспечивает режим ”лексического и синтаксического разбора исходных текстов программ”, перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
А1.1	Разбиение исходного файла программы на поток лексем
	Вход 1: прием управляющего сигнала
	Выход 1: обращение на чтение к базе данных D1, содержащей листинги исходных программ
	Выход 2: обращение на чтение к базе данных D2, содержащей грамматику языка программирования
Выход 3: передача управления
А1.2	Инициализация стека ОЗУ, после этой операции стек пуст
А1.3	Проверка условия: остались непрочитанные лексемы в потоке лексем?
	Выход 1: передача управления в случае, когда остались лексемы
	Выход 2: передача управления в случае, когда весть поток лексем
уже обработан
А1.4	Извлечение лексемы из потока и помещение ее на вершину стека ОЗУ
А1.5	Инициация чтения синтаксических правил грамматики языка программирования, начиная с первого правила
А1.6	Проверка условия: остались непрочитанные синтаксические правила?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
А1.7	Получение следующего синтаксического правила
	Выход 1: передача сигнала управления
Выход 2: обращение на чтение к данным - грамматике языка
А1.8	Проверка условия: возможно ли применение правила к последовательности элементов на вершине стека?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
А1.9	Замена последовательности элементов на вершине стека, подходящей под правило, на поддерево разбора, соответствующее правилу
А1.10	Проверка условия: синтаксическое правило соответствует введению нового типа?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
A1.11	Добавление записи в таблицу типов
	Выход 1: передача управления
Выход 2: обращение на запись к данным - таблице типов после выполнения модуля А1.
A1.12	Проверка условия: в стеке ровно один элемент, соответствующий дереву разбора исходного текста?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
A1.13	Извлечение дерева разбора из стека
	Выход 1: обращение на запись к данным - дереву разбора после выполнения модуля А1
Выход 2: передача управляющего сигнала

В основе работы данного модуля использован алгоритм LR-разбора файла с исходным текстом программы по набору лексических и синтаксических правил разбора. В процессе синтаксического разбора строится дерево разбора и таблица типов.

На фиг.4 приведен пример реализации модуля А2 АПБ-А. Аппаратно программный модуль А2 обеспечивает режим ”преобразования дерева разбора кода программы к виду, пригодному для перевода его во внутреннее представление”, перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
А2.1	Вызов процедуры MARK SCOPES модуля А2 для корневой вершины дерева разбора. Пример реализации данной процедуры приведен на фиг.5.
	Вход 1: прием управляющего сигнала
	Выход 1: передача управления и результатов выполнения
	Выход 2: обращение на чтение к данным - дереву разбора после выполнения модуля А1
Выход 3: обращение на чтение к данным - таблице типов после выполнения модуля А1
А2.2	Инициация обхода детей корневой вершины дерева разбора начиная с первой вершины-ребенка
А2.3	Условие: остались дети корневой вершины с типом ”определение функции”?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
А2.4	Найти все объявления в поддереве, соответствующем телу функции, и переместить их таким образом, что они станут детьми текущей вершины с типом ”определение функции”
А2.5	Переход к обработке следующей вершины-ребенка корневой вершины
А2.6	Вызов процедуры TRANSFORM SYNTAX TREE модуля А2, раскрываемой на фиг.6.
	Вход 1: передача управления
	Выход 1: передача управления
	Выход 2: обращение на чтение к данным - правилам преобразования дерева
Выход 3: обращение на запись к данным - дереву разбора после выполнения модуля А2
	Выход 4: обращение на запись к данным - таблице типов после выполнения модуля А2

Модуль А2 представляет процедуру ”SIMPLIFY SYNTAX TREE”, производящую надлежащее упрощение дерева разбора, результатом которого является дерево разбора и таблица типов, преобразование которых ко внутреннему представлению значительно проще по сравнению с преобразованием ”сырого” дерева разбора.

Схема процедуры ”SIMPLIFY SYNTAX TREE” представлена на фиг.4. В работе процедуры используются две внутренние рекурсивные процедуры ”MARK SCOPES” и ”TRANSFORM SYNTAX TREE”, осуществляющие, соответственно, пометку областей видимости объявлений и определений в дереве разбора и преобразование дерева разбора по заранее заданному набору правил.

На фиг.5 приведен пример реализации рекурсивной процедуры А2.1. ”MARK SCOPES”, при этом приняты следующие обозначения:

Обозначение	Описание
А2.1.1	Синтез дерева разбора и таблицы типов
	Вход: прием управляющего сигнала
	Выход 1: передача управления
	Выход 2: обращение на чтение к данным - дереву разбора после выполнения модуля А1
Выход 3: обращение на чтение к данным - таблице типов после выполнения модуля А1
А2.1.2	Выбор: тип вершины?
	Выход 1: передача управления в случае, если вершина имеет тип ”блочная инструкция” или ”определение функции”
Выход 2: передача управления в других случаях
А2.1.3	Добавление к вершине атрибута ”область видимости (scope)” с уникальным значением
А2.1.4	Все идентификаторы объявляемых переменных, находящиеся в поддереве обрабатываемой вершины, пометить атрибутом ”область видимости” с полученным значением на предшествующем шаге
А2.1.5	Инициализация обработки ”детей вершины” начиная с первой вершины - ”ребенка”
А2.1.6	Проверка условия: остались необработанные ”дети вершины”?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
А2.1.7	Рекурсивный вызов процедуры MARK SCOPES модуля A3
	Вход 1: прием сигнала управления
	Выход 1: передача управления
	Выход 2: обращение на чтение к данным - дереву разбора после выполнения модуля А1
Выход 3: обращение на чтение к данным - таблице типов после выполнения модуля А1

На фиг.6 приведен пример реализации рекурсивной процедуры А2.6. ”TRANSFORM SYNTAX TREE”, при этом приняты следующие обозначения:

Обозначение	Описание
А2.6.1	Инициализация обработки ”детей” корневой вершины дерева начиная с первой вершины - ”ребенка”
А2.6.2	Проверка условия: остались необработанные дети вершины? Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
А2.6.3	Рекурсивный вызов процедуры TRANSFORM SYNTAX TREE модуля А2 для поддерева очередного ребенка обрабатываемой вершины
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
	Выход 2: обращение на чтение к данным - правилам преобразования дерева
	Выход 3: обращение на запись к данным - дереву разбора после выполнения модуля А2
Выход 4: обращение на запись к данным - таблице типов после выполнения модуля А2
А2.6.4	Сохранение полученного дерева разбора для вершины
	Выход 1: передача управления
Выход 2: обращение на запись к данным - массиву результатов преобразования для детей вершины
А2.6.5	Инициализация процесса чтения правил преобразования дерева разбора, начиная с первого правила
А2.6.6	Проверка условия: остались непрочитанные правила преобразования?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
А2.6.7	Прочесть очередное правило преобразования в D3
	Выход 1: передача управления
Выход 2: обращение на чтение к данным - правилам преобразования дерева в D3
А2.6.8	Проверка условия: правило преобразования применимо?
	Выход 1: передача управления в случае истинности условия
Выход 2: передача управления в случае ложности условия
А2.6.9	Формирования в ОЗУ временных данных: временный массив результатов - деревьев разбора для ”детей” обрабатываемой вершины
А2.6.10	Применение правила преобразования дерева к текущей вершине и набору деревьев разбора, хранимых во временном массиве результатов
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
	Выход 2: обращение на чтение к данным - массиву результатов преобразования для ”детей” вершины
	Выход 3: обращение на запись к данным - дереву разбора после выполнения модуля А2
Выход 4: обращение на запись к данным - таблице типов после выполнения модуля А2

На вход процедуры TRANSFORM SYNTAX TREE поступает дерево (или поддерево) разбора, на выходе получается результирующее преобразованное дерево разбора. Внутри процедуры происходит рекурсивный вызов этой процедуры и сохранение результатов (дерева разбора) выполнения этого вызова во временном массиве результатов, который размещается в ОЗУ.

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

На фиг.7 приведен пример реализации аппаратно-программного модуля A3, обеспечивающего режим верификации многофайловых программных проектов на основе реализации процедуры ”MERGE SYNTAX TREES” для компоновки деревьев разбора и таблиц типов, при этом приняты следующие обозначения:

Обозначения	Описание
А3.1	Инициализация результирующего дерева разбора и таблицы типов
A3.2	Проверка условия: остались деревья разбора для компоновки?
	Выход 1: передача сигнала управления в случае истинности условия
Выход 2: передача сигнала управления в случае ложности условия
А3.3	Получение очередного дерева разбора
	Выход 1: передача сигнала управления
Выход 2: обращение на чтение к данным - набору деревьев разбора после выполнения модуля А2
A3.4	Проверка условия: остались необработанные дети корневой вершины?
	Выход 1: передача сигнала управления в случае истинности условия
Выход 2: передача сигнала управления в случае ложности условия
A3.5	Добавить поддерево, в котором корневой вершиной является очередной ”ребенок”, в результирующее дерево разбора таким образом, что корневая вершина добавляемого дерева окажется ”ребенком” корневой вершины результирующего дерева
	Выход 1: передача сигнала управления
Выход 2: обращение на запись к данным D4 - дереву разбора после выполнения части А
А3.6	Проверка условия: остались таблицы типов для компоновки?
	Выход 1: передача сигнала управления в случае истинности условия
Выход 2: передача сигнала управления в случае ложности условия
А3.7	Получение очередной таблицы типов
	Выход 1: передача сигнала управления
Выход 2: обращение на чтение к данным - набору таблиц типов после
	выполнения модуля А2
А3.8	Добавление всех элементов из таблицы типов в результирующую таблицу типов
	Выход 1: передача сигнала управления
Выход 2: обращение на запись к данным - таблице типов после выполнения части А

На фиг.8 приведен пример реализации аппаратно-программного блока (АПБ) преобразования кода (АПБ-В), обеспечивающего преобразование дерева разбора исходной программы к внутреннему представлению, при этом приняты следующие обозначения:

Обозначение	Описание
В1	Обращение к аппаратно-программному модулю В1 ”Встраивание функций”. Работа данного модуля раскрыта на схеме, изображенной на фиг.9.
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
Выход 2: обращение к базе данных D4 дерева разбора листинга программы
В2	Обращение к аппаратно-программному модулю В2 ”Разворачивания структур”. Работа данного модуля раскрыта на схеме, изображенной на фиг.11.
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
Выход 2: обращение к базе данных D5 таблиц типов языка программирования
В3	Обращение к аппаратно-программному модулю В3 ”Разворачивания выражений”. Работа данного модуля раскрыта на схеме, изображенной на фиг.12.
	Вход 1; прием сигнала управления
Выход 1: передача сигнала управления
В4	Обращение к аппаратно-программному модулю В4 ”Преобразования к внутреннему представлению”. Работа данного модуля раскрыта на схеме, изображенной на фиг.13.
Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
	Выход 2: сохранение в базе данных D7 программы на языке внутреннего представления
	Выход 3: сохранение базы условий корректности в базе данных D8
	Выход 4: сохранение базы соответствия условий корректности подозрительным точкам исходного кода в базе данных D9
Выход 5: обращение к базе знаний D6 аннотаций внешних функций
D4	База данных D4 дерева разбора листинга программы
Вход 2: обращение к дереву разбора листинга программы
D5	База данных D5 таблиц типов языка программирования
Вход 2: обращение к дереву разбора листинга программы
D6	База знаний D6 аннотаций внешних функций
Вход 1: обращение к базе аннотаций
D7	База данных D7 программ на языке внутреннего представления
Вход 1: сохранение программы на языке внутреннего представления
D8	Базы данных D8 условий корректности языка внутреннего представления исходного кода программы
Вход 1: сохранение базы условий корректности
D9	База знаний D9 условий проверки корректности подозрительных точек исходного кода программы
Вход 1: сохранение базы соответствия условий корректности подозрительным точкам исходного кода

На фиг.9 приведен пример реализации модуля В1 АПБ-В. Аппаратно программный модуль В1 (встраивание функций) обеспечивает режим модифицирования дерева разбора, которое находится в базе данных D4. Перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
В1.1	Проверка условия: есть ли необработанные локальные переменные.
	Выход 1: да
	Выход 2: нет
Выход 3: обращение к дереву разбора программы
В1.2	Убрать вершину, помеченную как объявление переменной х, из детей вершины, помеченной как объявление функции f, добавить к дереву вершину, помеченную как объявление переменной x@f.
В1.3	Для всех потомков вершины-ребенка функции f, которые помечены
Обозначение	Описание
В1.4	как идентификаторы х заменить их на идентификаторы x@f.Вызов процедуры UF (разворачивание функций) для дерева разбора с выделенной вершиной, соответствующей функции main.
D4	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
	База данных дерева разбора листинга программы программы
Вход 2: обращение к дереву разбора программы

На фиг.10 приведен пример реализации процедуры разворачивания функций (Unwinding Functions - UF). На вход процедуры подается дерево разбора с выделенной вершиной, соответствующей некоторой функции, на выходе получается дерево разбора. На фиг.10 приняты следующие обозначения:

Обозначение	Описание
UF.1	Добавить в стек (ОЗУ) вызовов имя вызываемой функции.
UF.2	Проверить условие: есть ли необработанные вызовы функций.
	Выход 1: да
Выход 2: нет
UF.3	Взять следующий необработанный вызов функции f.
UF.4	Проверить условие: лежит f в стеке вызовов.
	Выход 1: да
Выход 2: нет
UF.5	Добавить переменную того же типа, что и возвращаемое значение функции f.
UF.6	Проверить условие: является ли вызов функции ребенком цикла, условной конструкции или тела функции?
	Выход 1: да
Выход 2: нет
UF.7	Заменить вершину, соответствующую вызову идентификатором временной переменной.
UF.8	Вызов процедуры UF с помеченной вершиной, соответствующей функции f.
Обозначение	Описание
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
UF.9	Вставить вместо вызова f ее текст.
UF.10	Добавить в конец текста f метку и заменить во вставленном тексте вершины return на переход на эту метку.
UF.11	Добавить перед вставленным текстом f присваивания аргументов из вызова параметрам функции.

На фиг.11 приведен пример реализации модуля В2 АПБ-В (аппаратно-программный модуль разворачивания структур). На вход модуля В2 подается дерево разбора и таблица типов, на выходе получают модифицированное дерево разбора. Перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
В2.1	Проверка условия: есть ли необработанные структурные типы.
	Вход 1: прием сигнала управления
	Выход 1: да
	Выход 2: нет
Выход 3: обращение к таблице типов
В2.2	Взять следующий необработанный тип t с полями а0,…, а n с типами t0,…, tn.
В2.3	Заменить каждое объявление переменной х типа t на объявления переменных х.а0,…,х.а n типа t 0,…,t n.
В2.4	Для каждого структурного типа s с полем х типа t заменить на поля s.x.a 0,…, s.x.a n типа t 0,…, t n.
В2.5	Каждое присваивание переменных х=у типа t заменить на семейство присваиваний х.а0=у.а 0,…, х.а n=у.а n
D5	База данных D5 таблиц типов языка программирования
	Вход 2: обращение к таблице типов

На фиг.12 приведен пример реализации модуля В3 АПБ-В. На вход аппаратно-программного модуля В3 (модуль разворачивания выражений) подается преобразованное дерево разбора, а на его выходе получается новое преобразованное дерево разбора. Перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
В3.1	Проверить условие: есть ли необработанные циклы.
	Выход 1: да
	Выход 2: нет
В3.2	Вместо вершины? отвечающей циклу? дописывается список ее детей, в начале и в конце добавляются метки. Потомки вершины-цикла, помеченные continue заменяются на goto к метке в начале цикла, потомки break заменяются на goto к метке в конце цикла. Перейти к следующему циклу.
В3.3	Проверить условие: есть ли необработанные условные конструкции.
	Выход 1: да
	Выход 2: нет
В3.4	Добавить три метки. Заменить условную конструкцию на cond-goto, с тем же условием, что и условная конструкция, которая переходит на первую метку в случае истинности условия и на вторую в случае его ложности. После cond-goto добавить первую метку, после нее добавить детей потмока, помеченного true-branch, после чего добавить вторую метку и добавлить детей потомка, помеченного false-branch.
В3.5	Проверить условие: присутствуют ли обращения к массивам внутри арифметических выражений.
	Выход 1: да
	Выход 2: нет
В3.6	Добавить переменную, соответствующую типу элемента массива.
В3.7	Добавить присваивание временной переменной элемента массива и заменить обращение к массиву на временную переменную.

На фиг.13 приведен пример реализации модуля В4 АПБ-В (аппаратно-программный модуль преобразования к внутреннему представлению). На вход модуля В4 подается дерево в виде преобразованного дерева разбора исходного кода и база знаний D6 аннотаций внешних функций, на выходе модуля В4 получают базу данных D7 программ на языке внутреннего представления, базу данных D8 условий корректности языка внутреннего представления исходного кода программы и базу знаний D9 условий проверки корректности подозрительных точек исходного кода программы. Перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
В4.1	Установить счетчик меток в ноль. Сделать таблицу меток пустой. Таблица меток представляет собой таблицу соответствия символьных меток, встречающихся в дереве, поступающему на вход алгоритму, числовым меткам, которыми будут помечены все инструкции внутреннего представления (метки имеют вид Lxx, где хх - номер инструкции). Счетчик меток содержит последний использованный числовой идентификатор.
В4.2	Проверка условия: есть ли необработанные дети тела функции main.
	Выход 1: да
Выход 2: нет
В4.3	Взять следующую необработанную вершину.
В4.4	Определить тип вершины.
	Выход 1: присваивание
	Выход 2: переход
	Выход 3: метка
Выход 4: вызов функции
В4.5	Вызвать процедуру AT (преобразования присваиваний) для поддерева с корнем в избранной вершине.
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
	Выход 2: модификация программы на языке внутреннего представления
	Выход 3: пополнение базы данных D8 условий корректности языка внутреннего представления исходного кода программы
Выход 4: пополнение базы знаний D9 условий проверки корректности подозрительных точек исходного кода программы подозрительными точкам исходного кода
В4.6	Вызвать процедуру GT (преобразования переходов) для поддерева с корнем в избранной вершине.
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
Выход 2: модификация программы на языке внутреннего представления
В4.7	Добавить в таблицу меток связь символьной метки, которой помечена вершина с текущим счетчиком меток.
В4.8	Проверить условие: присутствует ли функция в базе аннотаций.
	Выход 1: да
Выход 2: нет
Обозначение	Описание
В4.9	Из базы аннотаций D6 взять код функции, произвести подстановку меток, к номерам меток, присутствующим в базе добавить текущий номер метки, после этого увеличить его на число инструкций. Произвести подстановку параметров, которыми заменить метки вершин-детей обрабатываемой вершины, начиная со второй, меткой последней вершины-ребенка заменить выходное значение. Для параметров-массивов произвести подстановку ассоциированных переменных.
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
	Выход 2: модификация программы на языке внутреннего представления
	Выход 3: пополнение базы условий корректности
Выход 4: пополнение базы соответствия условий корректности подозрительным точкам исходного кода
В4.10	Перейти к следующей вершине.
В4.11	Проверить условие: есть ли условные или безусловные переходы на символьные метки, а не на метки вида Lxx.
	Выход 1: да
	Выход 2: нет
Выход 3: обращение к базе знаний аннотаций D6
В4.12	Взять инструкцию перехода и заменить символьную метку в соответствии с таблицей меток.
D6	База знаний D6 аннотаций внешних функций
Вход 1: обращение к базе аннотаций
D7	База данных D7 программ на языке внутреннего представления
Вход 1: сохранение программы на языке внутреннего представления
D8	Базы данных D8 условий корректности языка внутреннего представления исходного кода программы
Вход 1: сохранение базы условий корректности
D9	База знаний D9 условий проверки корректности подозрительных точек исходного кода программы
Вход 1: сохранение базы соответствия условий корректности подозрительным точкам исходного кода

На фиг.14 приведен пример реализации процедуры преобразования присваиваний (Assign Transform - AT). На вход процедуры AT подается вершина дерева, соответствующая присваиванию, на выходе процедуры получают инструкции внутреннего представления. На фиг.14 приняты следующие обозначения:

Обозначение	Описание
АТ.1	Проверить условие: является ли левый операнд а обращением к массиву.
	Выход 1: да
Выход 2: нет
АТ.2	Преобразовать индекс массива а к выражению во внутреннем представлении х процедурой SAE.
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
АТ.3	Проверить условие: является ли правый операнд b обращением к массиву.
	Выход 1: да
Выход 2: нет
АТ.4	Преобразовать правый операнд к выражению во внутреннем представлении у процедурой SAE.
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
АТ.5	Передать следующему шагу инструкцию внутреннего представления assign a а[х]=у, условие корректности х+a@offset<a@size и соответствие условий корректности точке в исходном коде и увеличить счетчик меток.
АТ.6	Добавить временную переменную t.
АТ.7	Передать следующему шагу инструкцию внутреннего представления assign a t=а[х], условие корректности х+a@offset<a@size и соответствие условий корректности точке в исходном коде и увеличить счетчик меток.
АТ.8	Преобразовать индекс массива b к выражению во внутреннем представлении у процедурой SAE.
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
АТ.9	Передать следующему шагу инструкцию внутреннего представления a assign b[y]=t, условие корректности у+b@offset<b@size и соответствие условий корректности точке в исходном коде и
Обозначение	Описание
	увеличить счетчик меток.
AT.10	Проверить условие: является ли правый операнд b обращением к массиву.
	Выход 1: да
Выход 2: нет
AT.11	Преобразовать индекс массива b к выражению во внутреннем представлении х с помощью процедуры SAE.
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
AT.12	Передать следующему шагу инструкцию внутреннего представления a assign а=b[х], условие корректности х+b@offset<b@size и соответствие условий корректности точке в исходном коде и увеличить счетчик меток.
AT.13	Преобразовать правый операнд к выражению во внутреннем представлении х с помощью процедуры SAE.
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
AT.14	Передать следующему шагу инструкцию внутреннего представления assign a=х и увеличить счетчик меток.
AT.15	Модификация программы на языке внутреннего представления, запись в базу условий корректности и базу соответствия условий корректности подозрительным точкам исходного кода в соответствии с переданными данными.
	Вход 1: прием сигнала управления
	Выход 1: передача управления
	Выход 2: модификация программы на языке внутреннего представления
	Выход 3: пополнение базы условий корректности
Выход 4: пополнение базы соответствия условий корректности подозрительным точкам исходного кода
AT.16	Модификация программы на языке внутреннего представления, запись в базу условий корректности и базу соответствия условий корректности подозрительным точкам исходного кода в соответствии с переданными данными.
	Выход 1: передача сигнала управления
	Выход 2: модификация программы на языке внутреннего представления
	Выход 3: пополнение базы условий корректности
Выход 4: пополнение базы соответствия условий корректности
Обозначение	Описание
	подозрительным точкам исходного кода
D7	База данных D7 программ на языке внутреннего представления
Вход 1: модификация программы на языке внутреннего представления
D8	Базы данных D8 условий корректности языка внутреннего представления исходного кода программы
Вход 1: пополнение базы условий корректности
D9	База знаний D9 условий проверки корректности подозрительных точек исходного кода программы
Вход 1: пополнение базы соответствия условий корректности подозрительным точкам исходного кода

На фиг.15 приведен пример реализации процедуры преобразования переходов (Goto Transform - GT). На вход процедуры подается вершина, соответствующая условному/безусловному переходу, на выходе процедуры получается набор инструкций внутреннего представления. На фиг.15 приняты следующие обозначения:

Обозначение	Описание
GT.1	Проверить условие: является ли переход условным.
	Выход 1: да
Выход 2: нет
GT.2	Проверить условие: имеет ли условие вид сравнения (”равно”, ”больше” и т.п.)
	Выход 1: да
Выход 2: нет
GT.3	Преобразовать левый операнд в выражение во внутреннем представлении х процедурой SAE.
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
GT.4	Преобразовать левый операнд в выражение во внутреннем представлении у процедурой SAE.
Обозначение	Описание
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
GT.5	Проверить условие: равны ли х или у unknown .
	Выход 1: да
Выход 2: нет
GT.6	Задать условие condition unknown .
GT.7	Задать условие х предикат у.
GT.8	Добавить инструкцию condition с заданным условием и увеличить на единицу счетчик меток.
	Выход 1: передача сигнала управления
Выход 2: модификация программы на языке внутреннего представления
GT.9	Добавить во внутреннее представление инструкцию goto и увеличить на единицу счетчик меток.
	Выход 1: передача сигнала управления
Выход 2: модификация программы на языке внутреннего представления
D7	База данных D7 программ на языке внутреннего представления
Вход 1: модификация программы на языке внутреннего представления

На фиг.16 приведен пример реализации процедуры преобразования выражений (Simple Arithmetic Expression transform - SAE). На вход процедуры подается вершина, соответствующая арифметическому выражению, на выходе - получают выражение на языке внутреннего представления. На фиг.16 приняты следующие обозначения:

Обозначение	Описание
SAE.1	Проверка условия: является ли вершина является операцией.
	Выход 1:да
Выход 2: нет
SAE.2	Преобразовать левый операнд в выражение во внутреннем представлении х процедурой SAE.
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
Обозначение	Описание
SAE.3	Преобразовать правый операнд в выражение во внутреннем представлении у процедурой SAE.
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
SAE.4	Проверка условия: равны ли х или у unknown .
	Выход 1: да
	Выход 2: нет
SAE.5	Вернуть unknown .
SAE.6	Вернуть х операнд у.
SAE.7	Тип переменной х, которой помечена вершина численный?
	Выход 1: да
	Выход 2: нет
SAE.8	Вернуть unknown .
SAE.9	Вернуть идентификатор переменной, которой помечена вершина.

На фиг.17 приведен пример реализации аппаратно-программного блока анализа кода (АПБ-С) программы на языке внутреннего представления и формирование отчета об обнаруженных ”уязвимостях”, при этом приняты следующие обозначения:

Обозначение	Описание
С1	Обращение к аппаратно-программному модулю С1 (получение инвариантов в точках внутреннего представления)
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
Выход 2: считывание инструкций программы на языке внутреннего представления
С2	Обращение к аппаратно-программному модулю С2 (генерация систем информационной базы)
	Вход 1: прием сигнала управления
	Выход 1 передача сигнала управления
	Выход 2 считывание базы условий корректности
Выход 3 сохранение информационной базы
С3	Обращение к аппаратно-программному модулю С3 (исследование систем ограничений информационной базы)
Обозначение	Описание
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
Выход 2: считывание систем ограничений информационной базы
С4	Обращение к аппаратно-программному модулю С4 (формирование отчета о возможных уязвимостях)
	Вход 1: прием сигнала управления
	Выход 1: передача сигнала управления
	Выход 2: считывание записей базы соответствия условий корректности подозрительным точкам исходного кода
Выход 3: вывод отчета об обнаруженных уязвимостях
D7	База данных D7 программ на языке внутреннего представления
Вход 2: обращение к программе на языке внутреннего представления
D8	Базы данных D8 условий корректности языка внутреннего представления исходного кода программы
Вход 2: обращение к базе условий корректности
D9	База знаний D9 условий проверки корректности подозрительных точек исходного кода программы
Вход 2: обращение к базе соответствия условий корректности подозрительным точкам исходного кода
D10	Информационная база знаний (D10), содержащая системы ограничений в виде алгебраических уравнений и неравенств
	Вход 1: сохранение информационной базы
Вход 2: извлечение систем ограничений информационной базы
D11	База данных (D11) отчетов об обнаруженных уязвимостях программного кода
Вход 1: вывод отчета об обнаруженных уязвимостях

На фиг.18-27 приведены примеры реализации основных модулей АПБ-С. На фиг.18 приведен пример реализации модуля С1 АПБ-С. Аппаратно программный модуль С1 обеспечивает поддержку режима ”получения инвариантов в точках внутреннего представления”, перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
С1.1	Считать инструкции программы и создать граф управления программы процедурой GG (см. пояснение 1 в тексте описания).
Вход 1: прием управляющего сигнала
Обозначение	Описание
	Выход 1: передача сигнала управления
Выход 2: программа на языке внутреннего представления
С1.2	Найти максимальные простые пути, ведущие из начальной вершины графа процедурой SP (см. пояснение 2 в тексте описания).
С1.3	Инициализация таблицы инвариантов (см. пояснение 3 в тексте описания).
С1.4	Проверка условия: есть ли необработанные простые пути.
	Выход 1: да
Выход 2: нет
С1.5	Вычислить инварианты вдоль очередного простого пути L процедурой PI (см. пояснение 4 в тексте описания).
С1.6	Уточнить таблицу инвариантов и закончить обработку пути L (см. пояснение 5 в тексте описания).
D7	База данных D7 программ на языке внутреннего представления
Вход 2: обращение к программе на языке внутреннего представления

На фиг.19 приведен пример реализации процедуры определения инвариантов вдоль одного простого пути (Path Invariants - PI). На ее вход поступает некоторый простой путь L=(L[0],…,L[m-1]) управляющего графа программы. На фиг.19 приняты следующие обозначения:

Обозначение	Описание
PI.1	Присваивание р=0
PI.2	Проверка условия: р<m-1
	Выход 1: да
Выход 2: нет
PI.3	Вычисление: Y=YS(L, р+1) (см. пояснение в тексте описания).
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
PI.4	Присваивание: U=ТР[р]
PI.5	Определение вида инструкции L[p] (см. пояснение 6 в тексте описания).
Обозначение	Описание
	Выход 1: assign( a) x=expr
	Выход 2: condition x R const
	Выход 3: condition expr1 R expr2
Выход 4: другой
PI.6	Пересчет спектра переменной х (см. пояснение 7 в тексте описания).
PI.7	Пересчет множества предикатов U (см. пояснение 8 в тексте
	описания).
PI.8	Пересчет спектра переменной х (см. пояснение 9 в тексте описания).
PI.9	Пополнение множества предикатов U новым предикатом (см.
пояснение 10 в тексте описания).
PI.10	Запись спектров всех переменных во временную таблицу S (см.
пояснение 11 в тексте описания).
PI.11	Фильтрация спектров всех переменных и всех предикатов с
	помощью процедуры YF (см. пояснение 12 в тексте описания).
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
PI.12	Заполнение (р+1)-го столбца таблицы спектров и (р+1)-го элемента
таблицы предикатов (см. пояснение 13 в тексте описания).
PI.13	Присваивание р=р+1

На фиг.20 приведен пример реализации процедуры фильтрации спектров и предикатов (Y-Filter-YF). На фиг.20 приняты следующие обозначения:

Обозначение	Описание
YF.1	Проверка условия: есть ли в множестве Y необработанные инструкции?
	Выход 1: да
Выход 2: нет
YF.2	Определение вида очередной инструкции у из множества Y (см. пояснение 14 в тексте описания).
	Выход 1: assign x=x+const
	Выход 2: assign x=const
	Выход 3: assign( a) x= …
Выход 4: другой
YF.3	Сравнение const, 0
	Выход 1: const<0
Выход 2: const>0
Обозначение	Описание
YF.4	Проверка условия: ограниченности S[x] сверху (или sup S[x])?
	Выход 1: да
Выход 2: нет
YF.5	Проверка условия: ограниченности S[x] снизу (или inf[x])?
	Выход 1: да
Выход 2: нет
YF.6	Присваивание: S[x]=(-inf, +inf)
YF.7	Присваивание: S[x]=(-inf, max(S[x]))
YF.8	Присваивание: S[x]=(min(S[x]), +inf)
YF.9	Объединение (join) спектр переменной х со спектром {const} (см. пояснение 15 в тексте описания).
YF.10	Удалить из множества U все предикаты, куда входит переменная х (см. пояснение 16 в тексте описания).
YF.11	Окончание обработки инструкции у.

На фиг.21 приведен пример реализации процедуры вычисление множества Y (Y-Set-YS). На фиг.21 приняты следующие обозначения:

Обозначение	Описание
YS.1	Очистка множеств А, В, С, D.
YS.2	Присваивание А=A∪B.
YS.3	Инициализизация множества В.
УЗД	Проверка условия: есть необработанные элементы в А.
	Выход 1: да
Выход 2: нет
YS.5	Взять из А очередную необработанную вершину и пополнить множество В, закончить обработку вершины (см. пояснение 17 в тексте описания).
YS.6	Проверка В⊆А.
	Выход 1: да
Выход 2: нет
YS.7	Присваивание С=С∪D.
YS.8	Инициализизация множества D.
YS.9	Проверка, есть необработанные элементы в С?
	Выход 1: да
Выход 2: нет
YS.10	Взять из С очередную необработанную вершину v, пополнить множество D, закончить обработку вершины v (см. пояснение 18 в
Обозначение	Описание
	тексте описания).
YS.11	Проверка D⊆С.
	Выход 1: да
Выход 2: нет
YS.12	Присваивание Y=А∩С.

На фиг.22 приведен пример реализации процедуры определения максимально простых путей в графе (Simple Paths-SP). На фиг.22 приняты следующие обозначения:

Идентификатор	Описание
SP.1	Инициализировать очереди Q, R (см. пояснение 19 в тексте описания).
SP.2	Проверка условия: пуста ли очередь Q.
	Выход 1: да
Выход 2: нет
SP.3	Взять путь L из начала очереди Q.
SP.4	Присваивание max=false
SP.5	Взять v - конец пути L и А - множество соседних с v вершин.
SP.6	Проверка условия: есть в А необработанные вершины.
	Выход 1: да
Выход 2: нет
SP.7	Определить значение max.
	Выход 1: true
Выход 2: false
SP.8	Добавить путь L в очередь R.
SP.9	Взять очередную вершину и из А.
SP.10	Проверка условия: проходит ли путь L через и.
	Выход 1: да
Выход 2: нет
SP.11	Присваивание L'=(L, u) (см. пояснение 20 в тексте описания)
SP.12	Добавить путь L' в конец очереди Q.
SP.13	Присвоить max=true

На фиг.23 приведен пример реализации процедуры генерации управляющего графа программы (Generate Graph - GG). На фиг.23 приняты следующие обозначения:

Обозначение	Описание
GG.1	Считать инструкции внутреннего представления в массив Р; N - их число.
	Выход 1: передача сигнала управления
Выход 2: считывание инструкций программы на языке внутреннего представления
GG.2	Присвоить i=0.
GG.3	Проверка условия i<N.
	Выход 1: да
Выход 2: нет
GG.4	Создать в графе G новую вершину с пометкой P[i].
GG.5	Взять id - идентификатор инструкции P[i] и добавить пару (id, i) в словарь D.
GG.6	i=i+1
GG.7	i=0
GG.8	Проверка условия i<N.
	Выход 1: да
Выход 2: нет
GG.9	Определить вид инструкции P[i] (см. пояснение 21 в тексте описания).
	выход 1: инструкция P[i] имеет тип assign, a assign, assign a
	Выход 2: инструкция P[i] имеет вид goto id;
	Выход 3: инструкция P[i] имеет вид condition…? Id1: id2;
Выход 4: инструкция P[i] имеет тип stop
GG.10	Определить значения j1, j2, соответствующие ключам id1, id2 в словаре D.
GG.11	Создать в графе G пару ребер (i, j1) и (i, j2).
GG.12	Определить значение j, соответствующее ключу id в словаре D.
GG.13	Создать в графе G ребро (i, j).
GG.14	Создать в графе G ребро (i, i+1).
GG.15	Присваивание i=i+1
D7	База данных D7 программ на языке внутреннего представления
Вход 2: считывание инструкций программы на языке внутреннего представления

На фиг.24 приведен пример реализации модуля С2 АПБ-С. Аппаратно программный модуль С2 обеспечивает режим генерации систем информационной базы знаний D10 и позволяет свести задачу проверки условий корректности в программе на языке внутреннего представления к стандартной задаче линейного программирования. Перечень принятых обозначений имеет следующий вид:

Обозначение	Описание
С2.1	Считать условия корректности в массив СС.
Вход 1: передача сигнала управления
	Вход 2: считывание базы данных условий корректности условия корректности языка внутреннего представления исходного кода программы (D8)
С2.2	Блок проверки условия: если ли в массиве СС необработанные условия корректности.
	Выход 1: да
Выход 2: нет
С2.3	Взять из массива СС очередное условие корректности (Р, id) (см. пояснение 22).
С2.4	Взять из таблицы инвариантов TI множество условий W, соответствующих вершине управляющего графа, помеченной инструкцией с идентификатором id.
С2.5	Сформировать очередную систему информационной базы: W^¬Р.
	Выход 1: передача сигнала управления
Выход 2: пополнение информационной базы новой системой ограничений
С2.6	Закончить обработку условия корректности (Р, id).
D8	Базы данных условий корректности условия корректности языка внутреннего представления исходного кода программы (D8)
Вход 2: считывание базы условий корректности
D10	Информационная база знаний (D10), содержащая системы ограничений в виде алгебраических уравнений и неравенств
Вход 1: сохранение пополненной информационной базы знаний

На фиг.25 приведен пример реализации модуля С3 АПБ-С. Аппаратно-программный модуль С3 обеспечивает режим исследования систем ограничений информационной базы знаний D10. Перечень принятых обозначений на фиг.25 имеет следующий вид:

Обозначение	Описание
С3.1	Считывание систем информационной базы знаний D10 в массив Sys.
	Выход 1: передача сигнала управления
Выход 2: считывание систем ограничений информационной базы
С3.2	Формирование набора из t параллельно выполняемых задач (см. пояснение 23).
Обозначение	Описание
	Выход 1: передача сигнала управления процессу #1
	Выход 2: передача сигнала управления процессу #2
Выход t: передача сигнала управления процессу #t
С3.3	Проверка условия: есть необработанные системы для процесса #i?
	Выход 1: да
Выход 2: нет
С3.4	Взять очередную систему S
С3.5	Проверка условия: в S есть тождественно ложные предикаты или пары противоречащих друг другу предикатов(см. пояснение 24 в тексте описания)?
	Выход 1: да
Выход 2: нет
С3.6	Приведение системы S к виду задачи LP - классического линейного программирования (см. пояснение 25 в тексте описания).
С3.7	Симплекс-метод для решения задачи LP с помощью процедуры SIMPLEX-METHOD (см. пояснение 26 в тексте описания)
	Вход 1: прием сигнала управления
Выход 1: передача сигнала управления
С3.8	Сравнить L*, 0.
	Выход 1:L*<0
Выход 2: иначе
С3.9	Добавить номера системы S в список DNG.
С3.10	Закончить обработку системы S.
С3.11	Сихронизовать процессы #1,…, #t.
	Вход 1: передача сигнала управления от процесса #1
	Вход 2: передача сигнала управления от процесса #2
Вход t: передача сигнала управления от процесса #t
D10	Информационная база знаний (D10), содержащая системы ограничений в виде алгебраических уравнений и неравенств
Выход 2: считывание систем ограничений информационной базы

На фиг.26 приведен пример реализации процедуры решения задачи линейного программирования симлекс-методом (Simplex Method - SM). На фиг.26 приняты следующие обозначения:

Обозначение	Описание
SM.1	Инициализация массивов Е, В, D.
SM.2	Проверка условия: есть в массиве D отрицательные элементы?
	Выход 1: да
Выход 2: нет
SM.3	Определение min {D[i]} и выбор вектора A[k], включаемого в базис.
SM.4	Определение вектора А[В[r]] для исключения из базиса.
SM.5	Пересчет массивов Е, В для нового базиса (см. пояснение 27 в тексте описания).
SM.6	Пересчет массива D для текущей итерации (см. пояснение 28 в тексте описания).
SM.7	Вычислить L* - значение линейной формы на плане X.

На фиг.27 приведен пример реализации модуля С4 АПБ-С. Аппаратно программный модуль С4 обеспечивает режим формирования отчета об обнаруженных уязвимостях. Перечень принятых обозначений на фиг.27 имеет следующий вид:

Обозначение	Описание
С4.1	Проверка условия: есть необработанные номера в списке DNG?
	Выход 1: да
Выход 2: нет
С4.2	Взять очередной номер d из DNG.
С4.3	Извлечь из базы соответствия условий корректности подозрительным точкам исходного кода запись #d и выдать ее на экран.
	Выход 1: передача сигнала управления
	Выход 2: считывание записи #d из базы D9 соответствия условий
корректности подозрительным точкам исходного кода Выход 3: выдача на экран отчета об уязвимостях
С4.4	Закончить обработку номера d
D9	База знаний D9 условий проверки корректности подозрительных
	точек исходного кода программы
	Вход 2: считывание записи #d из базы соответствия условий
корректности подозрительным точкам исходного кода
D11	База данных отчетов об обнаруженных уязвимостях программного кода (D11)
Вход 1: выдача на экран отчета об уязвимостях

Далее приведены пояснения к обозначениям, использованным для фиг.18-27.

1. На данном шаге происходит считывание инструкций внутреннего представления программы в массив Р. Число инструкций (длина массива) предполагается равным N. Затем осуществляется вызов GG - вызов функции построения управляющего графа программы, которой передаются на вход массив Р и его размер N.

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

3. Инициализация таблицы инвариантов. Данный шаг заключается в выделении массива размера N, значениями которого являются множества инвариантов, причем i-й элемент массива будет содержать множество инвариантов, полученное в виде вершины графа с индексом i. На данном шаге множества инвариантов во всех элементах массива пусты.

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

5. Процедура уточнения таблицы инвариантов.

- Сначала для каждой вершины v простого пути L берется объединенный список Х предикатов таблиц TS(L), TP(L), соответствующих вершине

- затем, если вершина v уже обрабатывалась ранее на другом простом пути L', то из элемента таблицы TI, соответствующего вершине v, выбрасываются все предикаты, которые не встретились в списке X;

- если вершина v обрабатывается впервые, то в элемент таблицы TI, соответствующий вершине v, добавляются все предикаты из списка X.

6. Вычислить Y=Y(L, р+1). В данной функции происходит определение множества вершин v графа, таких что существует пара путей L', L”, не проходящих через вершины L[0],…, L[p], причем путь L' соединяет вершину L[p+1] с вершиной v, путь L” соединяет вершину v с вершиной L[р+1].

7. Рассматривается инструкция L[p], выделяются 4 основных случая.

- Инструкция имеет вид assign х=ехрr, либо assign_a х=…[…], где х - имя переменной, ехрr - некоторое арифметическое выражение.

- Инструкция имеет вид condition х R const, где х - имя переменной, R - один из предикатных символов {<,<=,>,>=,==,!=}, const - некоторое целое число.

- Инструкция имеет вид condition expr1 R expr2, где expr1, expr2 - некоторые арифметические выражения, R - один из предикатных символов {<,<=,>,>=,==,!=}.

- Другой вид инструкции (a_assign, goto, stop).

8. Пересчитать спектр переменной х, подставив в арифметическое выражение ехрr вместо переменных, входящих туда, их спектры из таблицы TS, столбца р. В результате получим новый спектр переменной х. Если инструкция имеет тип assign_a, то считаем, что спектр правой части равен (-inf, +inf).

9. Пересчитать множество предикатов U. Поскольку переменная х изменилась, то условия, содержащие х, которые были выполнены до инструкции L[p], перестанут быть выполнены после инструкции L[p]. В некоторых простейших случаях возможно скорректировать условие таким образом, что после инструкции L[p] оно вновь станет выполнено. Укажем эти условия.

- Пусть ехрr имеет вид х+const. Здесь const - некоторое целое число.

- Пусть предикат u имеет вид а^*х+w R с1, где а, с1 - некоторые целые числа, w - предикат, не зависящий от х, R - один из предикатных символов {<,<=,>,>=,==,!=}.

В этом случае можно скорректировать предикат следующим образом:

u'=а^*х+w R с2. Здесь с2=с1+const^*a. Если инструкция или предикат не удовлетворяют указанным условиям, то предикат необходимо из множества удалить.

10. Пересчитать спектр переменной х. Поскольку предикат, стоящий в инструкции L[p] имеет вид х R const, то ему всегда соответствует некоторый спектр s, выражающий то же самое условие. Например, предикату х<=10 будет соответствовать спектр (-inf, 11), а предикату х!=0 будет соответствовать спектр (-inf, 0)∪[1, +inf). Тогда текущий спектр переменной х нужно пересечь (с помощью операции intersect) со спектром s. При этом крайне важно учесть, какой ветке условного перехода отвечает ребро (L[p], L[p+1]). Если эта ветка соответствует ложности предиката, предикатный символ R нужно заменить на ему противоположный. Пары противоположных предикатных символов: (<,>=); (<=,>); (==, !=).

11. Пополнить множество предикатов U новым предикатом, который записан в теле инструкции условного перехода L[p]. Вне зависимости от вида данного условия, оно всегда будет выполнено. При выполнении данного шага необходимо учесть истинность иди ложность ветки условного перехода, отвечающей ребру (L[p], L[p+1]).

12. Записать спектры всех переменных из р-го столбца таблицы спектров с учетом возможных поправок спектра для отдельной переменной во временную таблицу S.

13. Произвести ”фильтрацию” спектров таблицы S и предикатов множества U. В результате фильтрации будут по-возможности скорректированы, а в худшем случае - отброшены все спектры и предикаты, которые могут оказаться неверны, если учесть инструкции из множества Y, которые могут появиться на трассе выполнения программы раньше точки L[p+1]. Такими инструкциями будут инструкции множества Y (см. шаг 1). Блок-схема работы функции YF будет далее приведена отдельно.

14. Заполнить (р+1)-й столбец таблицы спектров значениями, записанными во временной таблице S и (р+1)-й элемент таблицы предикатов положить равным U.

15. Рассматривается очередная инструкция у, выделяются 4 случая.

А. Инструкция у имеет вид assign х=х+const, где const - некоторое целое число.

В. Инструкция у имеет вид assign х=const, где const - некоторое целое число.

С. Инструкция у имеет вид assign x=…

D. Инструкция у имеет другой вид (тип отличен от assign).

16. Объединить при помощи операции join текущий спектр переменной х (из массива S) со спектром {const}.

17. Удалить из множества U все предикаты, куда входит переменная х.

18. Взять из А очередную необработанную вершину u, пополнить множество В вершинами, смежными с u, но не принадлежащими множеству {L[0],…,L[р-1]}, закончить обработку вершины u.

19. Взять из С очередную необработанную вершину u, пополнить множество D вершинами, не принадлежащими множеству {L[0],…,L[р-1]}, для которых вершина v - смежная, закончить обработку вершины v.

20. Инициализировать очереди Q, R. Очередь R изначально пуста. В очередь Q положить последовательность l={v0}, где v0 - начальная вершина графа (то есть вершина, входящая степень которой равна 0).

21. L'=(L, u). Данное выражение следует понимать следующим образом.

Путь L' получается из пути L добавлением вершины u.

22. Взять из массива СС очередное условие корректности, которое представляет собой пару вида (Р, id), где Р - предикат от переменных внутреннего представления, a id - идентификатор инструкции внутреннего представления, перед которой должен быть истинен предикат Р.

23. Формирование набора t параллельно выполняемых задач происходит путем разделения массива Sys на t примерно равных частей (частей, отличающихся не более чем на 1 систему). Затем каждый процесс будет заниматься исследованием своего подмножества информационной базы.

24. Проверка того, есть ли в системе S тождественно ложные предикаты или пары противоречащих друг другу предикатов.

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

а(1,1)^*х(1)+а(1,2)^*х(2)+…+а(1,n)^*х(n)<=b(1)

…

a(q,1)^*x(1)+a(q,2)^*x(2)+…+a(q,n)^*x(n)<=b(q)

a(q+1,1)^*x(1)+a(q+1,2)^*x(2)+…+a(q+1,n)^*x(n)==b(q+1)

…

a(m,1)^*x(1)+a(m,2)^*x(2)+…+a(m,n)^*x(n)==b(m).

Вводятся дополнительные неотрицательные переменные:

x(n+1),…, x(n+q), x'(1), x”(1),….x'(n),…,x”(n)>=0

так, чтобы выполнялись условия x(i)=x'(i)-x”(i).

Тогда систему S можно переписать в таком виде:

а(1,1)^*х'(1)-а(1,1)^*х”(1)+…+а(1,n)^*х'(n)-а(1,n)^*х”(n)+х(n+1)=b(1)

…

a(q,1)^*x'(1)-a(q,1)^*x”(1)+…+a(q,n)^*x'(n)-a(q,n)^*x”(n)+x(n+q)==b(q)

a(q+1,1)^*x'(1)-a(q+1,1)^*x”(1)+…+a(q+1,n)^*x'(n)-a(q+1,n)^*x”(n)==b(q+1)

…

a(m,1)^*x'(1)-a(m,1)^*x”(1)+…+a(m,n)^*x'(n)-a(m,n)^*x”(n)==b(m).

Для простоты записи переименуем все переменные и коэффициенты таким образом, чтобы система S приняла вид:

t(1,1)^*y(1)+…+t(1,n')^*y(n')=d(1)

…

t(m',1)^*y(1)+…+t(m',n')^*y(n')=d(m')

y(i)>=0,i=1,…,n',

где m'=m, n'=2^*m+q, причем d(i)>=0.

Задача классического линейного программирования:

Рассмотрим задачу максимизации линейной формы при условиях

Пусть L^* - решение указанной задачи. Тогда если

- L^*<0, то множество решений системы ограничений S пусто;

- L^*=0, то система S имеет решения.

26. Вызов функции SIMPLEX-METHOD.

27. Рекуррентные формулы пересчета массивов Е, В для нового базиса.

- B[r]=k;

- E[r][j]=E[r][j]/A[r], где j=1,…,m.

- E[i][j]=E[i][j] - E[r][j]^*A[i], где j=1,…, m, i=1,…, m+1, i≠r.

28. Формулы пересчета массива D для нового базиса.

-

На фиг.28 приведен пример реализации аппаратно-программного блока процессорного управления (АПБ-У), обеспечивающего синхронизацию основных режимов интерактивной верификации программного обеспечения распределенных вычислительных комплексов. На фиг.28 приняты следующие обозначения: У1 - блок нормирующих преобразователей (БНП); У2 - модуль коммутатора; У3 - модуль аналого-цифрового преобразователя (АЦП); У4 - модуль формирования статических координат графоаналитического растра (МФСКГАР); У 5 - модуль формирования динамической развертки графоаналитического растра (МФДРГАР); У6 - блок видеоконтроля (БВ); У7 - импульсный регулятор (ИР).

На фиг.29 приведен пример реализации модуля формирования статических координат графоаналитического растра (МФСКГАР) У4 АПБ-У. На фиг.29 приняты следующие обозначения: У4.1 - первое запоминающее устройство (ЗУ); У4.2 - блок интерполирования; У4.3 - блок выделения экстремума; У4.4 - блок масштабирования; У4.5 - схема формирования дискретных приращений статических координат графоаналитического растра; У 4.6 - блок преобразования статических координат графоаналитического растра; У4.7 - второе ЗУ.

На фиг.30 приведен пример реализации модуля формирования динамических координат графоаналитического растра (МФДРГАР) У5 АПБ-У. На фиг.30 приняты следующие обозначения: У5.1 - схема формирования дискретных приращений динамических координат графоаналитического растра; У5.2 - блок задания постоянных коэффициентов; У5.3 - блок синхронизации; У 5.4 - схема формирования адреса записи.

На фиг.31 приведен пример реализации блока видеоконтроля (БВ) У6 АПБ-У. На фиг.31 приняты следующие обозначения: У6.1 - модуль регистратора (МР) АПБ-У, на выходе которого установлены маска У6.2, оптическая система У6.3 и преобразователь оптического сигнала У6.4, выходом подключенный к входу блока динамической развертки У6.5.

На фиг.32 приведен пример реализации импульсного регулятора У 7 АПБ-У, который содержит блок определения абсолютных значений У 7.1, первый релейный элемент У7.2, первый логический элемент ”И” У7.3, второй релейный элемент У7.4, блок возведения в квадрат У7.5, триггер У7.6, первый, второй и третий блоки выборки-хранения У7.7, У7.8 и У7.9, первый формирователь импульсов У 7.10, источник эталонных напряжений У7.11, первый, второй и третий сумматоры У7.12, У7.13 и У7.14, электронный ключ У7.15, второй формирователь импульсов У7.16, третий релейные элементы У7.17, второй логический элемент ”И” У7.18.

На фиг.33-39 приведены фрагменты результатов работы предлагаемого способа и устройства в процессе верификации ИК ПО распределенных вычислительных комплексов.

В качестве первого примера (пример 1) рассмотрим процесс верификации исходного текста ПО на языке программирования Си. Для ясности изложения будем полагать, что листинг исходного текста программы поступил по независимому интерфейсному каналу последовательного порта (например, введен оператором ЭВМ в ручном режиме на основе использования клавиатуры см. фиг.1, детали сопровождения (ввода, редактирования, распределенного хранения и т.п.) исходного текста ИК ПО опускаются, поскольку они в данном контексте не имеют существенного значения, т.е. в данном примере не будем рассматривать особенности процессов сопровождения ИК ПО распределенных вычислительных комплексов. Основное внимание далее уделим процессу автоматического поиска участков уязвимости в ИК ПО. При этом исходная Си программа представляет собой набор из двух фалов следующего вида:

Файл main.c:

extern int f(int ^*arr, int ind);

int main()

{

int a[100];

int i;

int j;

for(i=0; i<10; ++i)

for(j=9; j>=i; --j)

a[10^*i+j]=0;

return f(a, 55);

}

Файл f.c:

int f(int^* arr, int ind)

{

return arr[ind];

}

ИК ПО заносится в базу данных D1. После окончания ввода ИК ПО АПБ-У формирует на системной шине (см. фиг.1) управляющий сигнал в момент времени t₁, который подается на вход 1 АПБ-А (см. фиг.2). Таким образом, АПБ-У фиксирует все моменты формирования управляющих сигналов и реакций, соответствующих АПБ и их модулей, на эти воздействия. При этом для краткости изложения далее эти моменты в описании опускаются. После поступления управляющего сигнала запускается АПБ-А, а именно (см. фиг.2)тело цикла, состоящее из аппаратно-программных модулей A.1, A.2, А.3 АПБ-А (далее для краткости изложения будем обозначать первым символом - А.^*, принадлежность каждого из используемых аппаратно-программных модулей, т.е. будем идентифицировать соответствующей буквой АПБ, а именно, АПБ-А, просто A.1, A.2 и т.д., АПБ-В - B.1 … и т.п.). При этом этот цикл в рассматриваемом примере будет выполнен ровно 2 раза, так как в наборе анализируемых файлов Си ИК ПО в наличии 2 файла. Соответственно АПБ-У обеспечивает контроль и измерение длительности выполнения не только каждого цикла, но и длительность работы каждого модуля АПБ-А. После выполнения этого цикла будут выполнены действия по соединению результатов разбора листингов ИК ПО в модуле А.8.

Операции, производимые в модуле A.2, раскрыты на фиг.3. Опишем процессы модуля А1 на примере разбора фрагментов листинга из файла main.c.

В процессе выполнения модуля А 1.1 происходит разбиение листинга ИК ПО, получаемого из базы данных D1, на поток лексем согласно правилам из грамматики языка, находящихся в базе данных D2.

Фрагмент начала последовательности лексем с обозначением типа лексем представлен ниже:

'extern' - ключевое слово

'int' - ключевое слово

'f' - идентификатор

'(' - символ'('

'int' - ключевое слово

'^*' - символ '^*'

'arr' - идентификатор

',' - символ','

'int' - ключевое слово

'ind' - идентификатор

')' - символ')'

';' - символ';'

…

Приведем пример фрагмента грамматики языка программирования Си (см. стандарт ISO:IEC 9899:1999, также называемой ”С99”).

…

statement:

labeled_statement

|compound_statement

|expression_statement

|selection_statement

|iteration_statement

|jump_statement

labeled_statement:

identifier':'statement

|'case' constant_expression':'statement

|'default'':' statement

compound_statement: compound_statement_startblock_item^*'}'

compound_statement_start:'{'

block item: declaration|statement

expression_statement: expression?';'

selection_statement:

'if'('expression')' statement

|'if'('expression')' statement

'else' statement

|'switch''('expression')' statement

iteration_statement:

'while''('expression ')'statement

|'do' statement 'while''('expression')'';'

|'for''('expression?';' expression?';'expression?')' statement

|'for''('declaration expression?';'expression?')'statement

jump_statement:

'goto' identifier';'

|'continue'';'

|'break'';'

|'return' expression?';'

translation_unit: |extemal_declaration

translation_unit: translation_unit extemal_declaration

external declaration: declaration|function definition

function_definition: declaration specifiers? declarator declaration^*

compound_statement

Для синтаксического разбора рассматриваемого здесь примера ИК ПО, построения дерева разбора и таблицы типов потребуются следующие синтаксические правила, являющиеся подмножеством грамматики языка Си:

1: declaration: declaration_specifiers init_declarator';';

2: declaration_specifiers: (storage_class_specifier|type_specifier|type_qualifier|

function_specifier)+;

3: init_declarator: declarator;

4: declarator: pointer? direct_declarator;

5: direct_declarator: direct_declarator'(' parameter_list')';

6: parameter_list: parameter_declaration^*;

7: direct_declarator: identifier;

8: parameter_declaration: declaration_specifiers declarator;

9: storage_class_specifier: 'typedef|'extern'|'static'|'auto'|'register';

10: type_specifier: 'void'|'char'|'short'|'int'|'long'|'float'|'double'|'signed'|'unsigned'| 'Bool'|'_Complex'|'_Imaginary'|struct_or_union_specifier|enum_specifier|typedef_name|typeof_expr|typeof_type;

11: pointer:'^*'+;

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

В цикле, состоящем из модулей А1.3, А1.4, А1.5, А1.6, А1.7, А1.8, А1.9, А1.10 и А1.11, производится применение синтаксических правил и построение дерева разбора и таблицы типов. В процессе выполнения последовательности А1.3, А1.4, А1.5, А1.6, А1.7 и А1.8 лексемы помещаются на вершину стека до тех пор, пока не станет возможным применение одного из правил синтаксического разбора. Соответственно длительность выполнения данных циклов и им подобных контролируется АПБ-У на основе измерения соответствующих интервалов времени и сопоставления их с некоторыми наперед заданными значениями, которые соответствуют нормальному режиму работы устройства верификации в целом. Подобные временные параметры устанавливаются на основе опытных данных и при первом обращении могут быть установлены эмпирически, а затем на тестовых примерах уточнены, например, на ИК ПО с известными точками уязвимости. Таким образом, обеспечивается режим обучения (самообучения) устройства верификации в каждом цикле верификации ИК ПО.

В рассматриваем здесь примере на этапе работы модуля А 1.4 на вершину стека помещается лексема 'extern'. При выполнении модулей А1.5, А1.6, А1.7 и А1.8 последовательность из 1 элемента 'extern' приводит к срабатыванию правила 9 и к замене последовательности на поддерево с корневой вершиной sc-spec на этапе выполнения модуля А 1.9. На этапе выполнения модуля А. 10 определяется то, что в ИК ПО, приведенного выше примера, новые типы при обработке не вводятся, поэтому модуль A.11 не выполняется.

На этапе выполнения модуля А 1.4 на вершину стека, а именно в его первую ячейку, помещается лексема 'int'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 последовательность из 1 элемента 'int' приводит к срабатыванию правила 10 и замене последовательности на поддерево с корневой вершиной type-spec. На этапе выполнения модуля А. 10 определяется, что в ИК ПО приведенного выше примера новые типы при обработке не вводятся, поэтому модуль A.11 не выполняется.

На следующем этапе выполнения модуля А1.4 на вершину стека, а именно в его первую ячейку, помещается лексема 'f'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 никакое синтаксическое правило не срабатывает.

На следующем этапе выполнения модуля А1.4 на вершину стека помещается лексема '('. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 никакое синтаксическое правило не срабатывает.

На следующем этапе выполнения модуля А1.4 на вершину стека помещается лексема 'int'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 последовательность из 1 элемента 'int' приводит к срабатыванию правила 10 и замене последовательности на поддерево с корневой вершиной type-spec. На этапе выполнения модуля А.10 определяется, что новые типы при обработке не вводятся, модуль A.11 не выполняется.

На следующем этапе выполнения модуля А 1.4 на вершину стека помещается лексема '^*'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 последовательность из 1 элемента '^*' приводит к срабатыванию правила 11 и замене последовательности на поддерево с корневой вершиной pointer. На этапе выполнения модуля А.10 определяется, что новые типы при обработке не вводятся, модуль А.11 не выполняется.

На следующем этапе выполнения модуля А 1.4 на вершину стека помещается лексема 'аrr'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 срабатывает правило 8 и на шаге А1.9 производится замена последовательности на поддерево с вершиной param-decl. На этапе выполнения модуля А.10 определяется, что новые типы при обработке не вводятся, модуль А.11 не выполняется.

На следующем этапе выполнения модуля А1.4 на вершину стека помещается лексема ','. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 никакое синтаксическое правило не срабатывает.

На следующем этапе выполнения модуля А 1.4 на вершину стека помещается лексема 'inf. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 последовательность из 1 элемента 'int' приводит к срабатыванию правила 10 и замене последовательности на поддерево с корневой вершиной type-spec. На этапе выполнения модуля А.10 определяется, что новые типы при обработке не вводятся, модуль A.11 не выполняется.

На следующем этапе выполнения модуля А1.4 на вершину стека помещается лексема 'ind'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 срабатывает правило 8 и на этапе выполнения модуля А1.9 производится замена последовательности на поддерево с вершиной param-decl. На этапе выполнения модуля А.10 определяется, что новые типы при обработке не вводятся, модуль А.11 не выполняется.

На следующем этапе выполнения модуля А1.4 на вершину стека помещается лексема ')'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 срабатывает правило 5 и на этапе выполнения модуля А1.9 производится замена последовательности на поддерево с вершиной d-d-param. На этапе выполнения модуля А.10 определяется, что новые типы при обработке не вводятся, модуль A.11 не выполняется.

На следующем этапе выполнения модуля А1.4 на вершину стека помещается лексема';'. В процессе выполнения модулей А1.5, А1.6, А1.7 и А1.8 срабатывает правило 1 и на этапе выполнения модуля А1.9 производится замена последовательности на поддерево с вершиной decl. На этапе выполнения модуля А.10 определяется, что новые типы при обработке не вводятся, модуль А.11 не выполняется.

Дальнейший поток лексем обрабатывается аналогичным образом, пока на этапе выполнения модуля А1.3 не обнаружится, что поток лексем закончен. На этапе выполнения модуля А1.12 определяется, что стек содержит только один элемент - дерево разбора. При этом выполнение всех вышеперечисленных этапов контролируется АПБ-У, т.е. если, например, на этапе выполнения модуля А1.12 произойдет аварийный останов цикла разбора ИК ПО, то АПБ-У обеспечит самодиагностику данного состояния устройства разбора. На этапе выполнения модуля А1.13 производится запись дерева разбора в динамический массив А.4.

Фрагмент дерева разбора, полученного на этапе работы модуля А1, может быть представлен в БВ АПБ-У (см. фиг.28) в виде (см. фиг.33-39), приемлемом для зрительного восприятия и анализа оператором ЭВМ.

После работы модуля А2 дерево разбора для файла main.c примет вид, изображенный на фиг.33.

Фрагмент дерева разбора, полученного на этапе применения модуля лексического и синтаксического разбора к файлу f.c, приведен на фиг.35.

После работы модуля А2 дерево разбора для файла f.c примет вид, изображенный на фиг.36.

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

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

В процессе работы модуля В1 осуществляется обращение к процедуре UF для обработки функции main. При обработке вызова функции f будет вызвана процедура UF для функции f. Эта процедура оставит функцию f без изменений, так как она не содержит вызовов функций. После этого, код функции f будет добавлен в код main.

Рассмотрим для простоты преобразованное дерево в виде программы на языке Си.

int a[100];

int i;

int j;

int ^*arr;

int ind;

int f_ret;

for(i=0; i<10; ++i)

for(j=9; j>=i; --j)

a[10^*i+j]=0;

arr=a;

ind=55;

f_ret=arr[ind];

return f_ret;

В приведенном примере присутствуют лишь простые типы, поэтому модуль В2 не выполняет преобразований.

В приведенном примере присутствуют циклы, которые будут на этапе выполнения модуля В3 развернуты. Так например, при преобразовании первого цикла будет получен следующий код на ”псевдо-Си”:

int a[100];

int i;

int j;

int ^*arr;

int ind;

int f_ret;

i=0;

goto (i<10) ? label1: label2;

label1:

for(j=9; j>=i; --j)

a[10^*i+j]=0;

++i;

label2:

arr=a;

ind=55;

f_ret=arr[ind];

return f_ret;

При преобразовании второго цикла будет получен следующий код на ”псевдо-Си”:

int a[100];

int i;

int j;

int ^*arr;

int ind;

int f_ret;

i=0;

label0:

goto (i<10) ? label1: label2;

label1:

J=9;

label3:

goto (j>=i) ? label4: label5;

label3:

a[10^*i+j]=0;

j++;

goto label3;

label4:

++i;

goto label0;

label2:

arr=a;

ind=55;

f_ret=arr[ind];

return f_ret;

На следующем этапе выполнения модуля В4 получается внутреннее представление программы следующего вида:

L1 assign	a@size=100;
L2 assign	a@offset=0;
L3 assign	i=0;
L4 condition	i<10 ? L5:L12;
L5 assign	j=9;
L6 condition	j>=i ? L7: L10;
L7 a_assign	a[10*i+j]=0;
L8 assign	j=j-1;
L9 goto	L6;
L10 assign	i=i+1;
L11 goto	L4;
L12	stop;

База данных условий корректности D8 будет представлена в следующем виде:

L7 a@offset+	10*i+j<a@size;
L7 a@offset+	10*i+j>=0;
L12 a@offset+	55<a@size;
L12 a@offset+	55>=0;

База знаний D9 соответствия условий корректности подозрительным точкам исходного кода:

1 main.с:3:9:16 1.0 Unable to deduce dereferencing upper bound;

2 main.c:3:9:16 1.0 Unable to deduce dereferencing lower bound;

3 main.с:14:7:15 1.0 Unable to deduce dereferencing upper bound;

4 main.с:14:7:15 1.0 Unable to deduce dereferencing lower bound;

Далее АПБ-У передаст управление АПБ-С. Рассмотрим в рамках данного примера работу каждого из модулей АПБ-С (см. фиг.17-27).

При этом в качестве дополнительного пояснения следует указать на то, что модуль С1 АПБ-С обеспечивает детализированный статический анализ ИК ПО на упрощенном языке внутреннего представления (далее - просто программы). Он позволяет собрать по данному описанию программы сведения, необходимые для доказательства условий корректности, что эквивалентно условию отсутствия в исходной программе уязвимостей, связанных с переполнением буферов ОЗУ. Далее целесообразно изложить описание принципов работы данного модуля.

Функционирование данного модуля тесно связано со следующими объектами:

N - множество целых неотрицательных чисел;

I - множество инструкций внутреннего представления. Размеченный граф представляет собой пару G=(V, Е), где

V - множество вершин, являющееся подмножеством N×M, где М - множество меток вершин графа. Для вершины v=(n, m) число n будем называть индексом вершины, а m - ее меткой,

Е - множество ребер, E⊆V×V.

Путь в графе - последовательность вершин ν₁,…ν_n, где (ν_i, ν_i+1)∈E для каждого i=1,…,n-1. Путь называется простым, если в нем нет повторяющихся вершин.

Управляющим графом программы называют размеченный граф, для которого множество меток совпадает с множеством I - инструкцией внутреннего представления программы.

Интервал значений переменной х - это одной из следующих множеств:

- -∞<х<+∞ - undefined_value

- -∞<х<b - left_infinity

- a<x<+∞ - right_infinity

- a≤x<b - interval

- x=a - exact_value

- ⌀ - impossible_value

Здесь также указаны обозначения типов возможных интервалов. Спектром переменной х называют условие на множестве ее возможных значений, заданное в виде объединения непересекающихся интервалов. При этом количество интервалов не должно превышать некоторого наперед заданного значения М.

Над множеством спектров введем бинарные операции intersect(P, Q), join(P, Q).

При этом:

intersect(P, Q) - пересечение спектра Р со спектром Q. Можно показать, что пересечением двух семейств из не более, чем М непересекающихся интервалов является спектром, состоящим из не более, чем 2^*М непересекающихся интервалов;

join(P, Q) - объединение спектра Р со спектром Q. Объединение двух семейств из не более, чем М непересекающихся интервалов является спектром, состоящим из не более, чем 2^*М непересекающихся интервалов.

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

В данном примере изображен спектр, состоящий из трех интервалов. Если М=2, то будут случайным образом выбраны два соседних интервала (например, первый и второй) и объединены в один интервал.

Учитывая возможность выполнения подобной операции ”редукции” спектра будем считать, что введенные ранее операции join и intersect преобразуют пару спектров, состоящих из не более, чем М интервалов в спектр, также состоящий из не более чем М интервалов.

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

P+Q={y∈Z:y=p+q, p∈P, q∈Q};

P-Q={y∈Z:y=p-q, p∈P, q∈Q};

P^*Q=[y∈Z:y=p^*q, p∈P, q∈Q};

P/Q={y∈Z:y=p/q, p∈P, q∈Q}.

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

Спектр переменной х можно понимать, как некий предикат от х, например, спектру

[0,6)∪{10} соответствует предикат (0≤x<6)∨(x==10).

Пусть N - число инструкций во внутреннем представлении программы, К -число переменных.

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

Таблица спектров вдоль простого пути L=(L[1],…, L[n]) - это двумерный массив TS размера К^*n, элементами которого являются спектры переменных. TS[k][i] - спектр k-й переменной в точке L[i] программы.

Отметим, что спектр можно тоже понимать как предикат, зависящий от одной переменной. При этом указанный предикат будет обозначать условие, которое выполняется в точке L[i] при условии, что трасса выполнения программы прошла через вершины L[1],…L[i].

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

Таблица предикатов вдоль простого пути L представляет собой массив ТР длины n, элементами которого являются множества предикатов, причем TP[i] - множество предикатов, которые будут выполнены в точке L[i] программы, но тоже при условии, что трасса выполнения программы прошла через вершины L[1],…,L[i]. Использовать таблицу предикатов необходимо вместе с таблицей спектров, поскольку спектр не позволяет задавать предикаты, зависящие от нескольких переменных, а условия, хранимые в таблице предикатов, невозможно корректировать в случае, когда на простом пути встречается инструкция, изменяющая значение переменной, входящей в предикат.

Таким образом, на этапе выполнения модуля С1 (см. фиг.18) будет осуществлен вызов процедура GG, которая считает 12 инструкцией внутреннего представления и соединит их в управляющий граф. Результат ее работы представлен на фиг.38.

Далее процедура SP модуля С 1 обнаружит следующие максимальные пути в данном графе:

path1=(L1, L2, L3, L4, L5, L6, L7, L8, L9);

path2=(L1, L2, L3, L4, L5, L6, L10, L11);

path3=(L1, L2, L3, L4, L12).

Для каждого из путей path1, path2 и path3 будет вызвана процедура определения инвариантов и с ее помощью определены множество Y, таблицы спектров и таблицы предикатов вдоль каждого из них:

1) Вдоль пути pathl.

Таблица спектров и множество Y:
	Y	a@size	a@offset	i	j
L1:	{}	[-inf, +inf)	[-inf, +inf)	[-inf, +inf)	[-inf, +inf)
L2:	{}	{100}	[-inf, +inf)	[-inf, +inf)	[-inf, +inf)
L3:	{}	{100}	{0}	[-inf, +inf)	[-inf, +inf)
L4:	{L4, L5, L6, L7, L8, L9, L10, L11}	{100}	{0}	[0, +inf)	[-inf, +inf)
L5:	{}	{100}	{0}	[0, 10)	[-inf, +inf)
L6:	{L6, L7, L8, L9}	{100}	{0}	[0, 10)	[-inf, 10)
L7:	{}	{100}	{0}	[0, 10)	[-inf, 10)
L8:	{}	{100}	{0}	[0, 10)	[-inf, 10)
L9:	{}	{100}	{0}	[0, 10)	[-inf, 9)
Множество предикатов будет непусто только в точках L7, L8, L9:
L7:{j-i>=0};
L8: {j-i>=0};
L9:{j-i>=-1}.

Процедура Y-FILTER в точке L4 для спектра переменной i: {0} и множества Y={L4, L5, L6, L7, L8, L9, L10, L11} обнаружит в точке L10 инструкцию ”i=i+1” и пересчитает новый спектр для i по правилу: spec(i)=[min({0}), +inf)=[0, +inf).

Аналогично, в точке L6 для спектра переменной j: {9} и множества Y={L6, L7, L8, L9} процедура обнаружит в точке L8 инструкцию ”j=j-1” и пересчитает новый спектр для j по правилу spec(j)=[-inf, max ({9})+1)=[-inf, 10).

2) Вдоль пути path2.

Таблица спектров и множество Y:
	Y	a@size	a@offset	i	j
L1:	{}	[-inf,+inf)	[-inf, +inf)	[-inf, +inf)	[-inf, +inf)
L2:	{}	{100}	[-inf, +inf)	[-inf, +inf)	[-inf, +inf)
L3:	{}	{100}	{0}	[-inf, +inf)	[-inf, +inf)
L4:	{L4, L5, L6, L7, L8, L9, L10, L11}	{100}	{0}	[0,+inf)	[-inf, +inf)
L5:	{}	{100}	{0}	[0,10)	[-inf, +inf)
L6:	{L6, L7, L8, L9}	{100}	{0}	[0,10)	[-inf, 10)
L10:	{}	{100}	{0}	[0,10)	[-inf, 10)
L11:	{}	{100}	{0}	[1,11)	[-inf, 9)

Множество предикатов будет непусто только в точках L10, L11:

L10:{j-i<0};

L11: {j-i<-1}.

Процедура Y-FILTER на данном пути отработает точно так же как и на пути path1.

3) Вдоль пути path3

Таблица спектров и множество Y:
	Y	a@size	a@offset	i	j
L1:	{}	[-inf, +inf)	[-inf, +inf)	[-inf, +inf)	[-inf, +inf)
L2:	{}	{100}	[-inf, +inf)	[-inf, +inf”	[-inf, +inf”
L3:	{}	{100}	{0}	[-inf, +inf)	[-inf, +inf)
L4:	{L4, L5, L6, L7, L8, L9, L10, L11}	{100}	{0}	[0, +inf)	[-inf, +inf)
L12:	{}	{100}	{0}	[10, +inf)	[-inf, +inf)

Множество предикатов будет пусто во всех точках.

Процедура Y-FILTER на данном пути в точке L4 отработает точно также как и на пути path1 в точке L4. Уточнение таблицы инвариантов для каждого из путей выдаст следующий результат:

в точке L1:
в точке L2:
a@size=100	# spectrum a@size: {100}, path1, path2, path3
в точке L3:
a@size==100	# spectrum a@size: {100}, path1, path2, path3
a@offset==0	# spectrum a@offset: {0}, path1, path2, path3
в точке L4:
a@size==100	# spectrum a@size: {100}, path1, path2, path3
a@offset==0	# spectrum a@offset: {0}, path1, path2, path3
i>=0	# spectrum i: [0, +inf), path1, path2, path3
в точке L5:
a@size==100	# spectrum a@size: {100}, path1, path2
a@offset==0	# spectrum a@offset: {0}, path1, path2
i>=0	# spectrum i: [0, 10), lower bound, path1, path2
i<10	# spectrum i: [0, 10), upper bound, path1, path2
в точке L6:
a@size==100	# spectrum a@size: {100}, path1, path2
a@offset==0	# spectrum a@offset: {0}, path1, path2
i>=0	# spectrum i: [0, 10), lower bound, path1, path2
i<10	# spectrum i: [0, 10), upper bound, path1, path2
j<10	# spectrum j: [-inf, 10), path1, path2
в точках L7, L8:
a@size==100	# spectrum a@size: {100}, path1
a@offset==0	# spectrum a@offset: {0}, path1
i>=0	# spectrum i: [0, 10), lower bound, path1
i<10	# spectrum i: [0, 10), upper bound, path1
j<10	ft spectrum j: [-inf, 10), path1
j-i>=0	ft predicate, path1
в точке L9:
a@size==100	# spectrum a@size: {100}, path1
a@offset==0	# spectrum a@offset: {0}, path1
i>=0	# spectrum i: [0, 10), lower bound, path1
i<10	# spectrum i: [0, 10), upper bound, path1
J<9	# spectrum j: [-inf, 9), path1
j-i>=-1	# predicate, path1
в точке L10:
a@size==100	# spectrum a@size: {100}, path2
a@offset==0	# spectrum a@offset: {0}, path2
i>=0	# spectrum i: [0, 10), lower bound, path2
i<10	# spectrum i: [0, 10), upper bound, path2
j<10	# spectrum j: [-inf, 9), path2
j-i<0	# predicate, path1
в точке L11:
a@size==100	# spectrum a@size: {100}, path2
a@offset==0	# spectrum aSoffset: {0}, path2
i>=1	# spectrum i: [1, 11), lower bound, path2
i<11	# spectrum i: [1, 10), upper bound, path2
J<9	# spectrum j: [-inf, 9), path2
j-i<-1	# predicate, path1
в точке L12:
a@size==100	# spectrum a@size: { 100 }, path3
a@offset==0	# spectrum a@offset: { 0 }, path3
i>=10	# spectrum i: [10, +inf), lower bound, path3

После работы модуля C.1 управление передается модулю С.2 (”Генерация систем информационной базы”), который для каждого условия корректности синтезирует свою система ограничений. Предикаты записываются в форме ”expr R const”, где ехрr - некоторое арифметическое выражение, R -предикатный символ, а const - некоторое целое число.

System 1: # correctness condition ″L7 a@offset+10^*i+j<a@size;″

a@size==100

a@offset==0

i>=0

i<10

j<10

j-i>=0

a@offset+10^*i+j-a@size>=0;

System 2: # correctness condition ″L7 a@offset+10^*i+j>=0;″

a@size==100

a@offset==0

i>=0

i<10

j<10

j-i>=0

a@offset+10^*i+j<0

System 3: # correctness condition ″L12 a@offset+55<a@size;″

a@size==100

a@offset==0

i>=10

a@offset-a@size>=-55

System 4: # correctness condition ”L12 a@offset+55>=0;”

a@size==100

a@offset==0

i>=10

a@offset<-55

Далее управление передается модулю С.3 (”Исследование систем ограничений информационной базы”). В качестве примера будем полагать, что число параллельных или независимых процессов равно четырем (t=4). На этапе формирования набора параллельно выполняемых задач будет получено задание для каждого из процессов:

для процесса № i - исследовать систему № i на предмет существования решений. Рассмотрим далее работу процесса № 1.

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

-i1+i2+x1+y1==0;

i1-i2+x2+y2==9;

j1-j2+x3+y3==9;

i1-i2-j1+j2+x4+y4==0;

-10^*i1+10^*i2-j1+j2+a@size1-a@size2-a@offset1+a@offset2+x5+y5==0;

a@size1-a@size2+y6==100;

a@offset1-a@offset2+y7==0.

Здесь для простоты были введены новые неотрицательные переменные:

i1, i2,j1,:)2,a@size1, a@size2,

a@offset1,a@offset2, x1, x2, x3, x4, x5, y1, y2, y3, y4, y5, y6, y7

с условиями i=i1-i2, j=j1-j2 и т.д.

Необходимо максимизировать следующий функционал:

L(Y)=- y1-y2-y3-y4-y5-y6-y7.

Решением данной задачи является значение L^*=-1, следовательно? исходная система не имеет решений. Для остальных систем информационной базы также можно показать, что они не имеют решений. Таким образом DNG={}.

Следовательно, модуль С.4 получит на вход пустой список номеров, не выведенных без условий корректности - DNG, и выдаст в базу данных D11 отчет, подтверждающий корректность программы:

No dangerous points found

No buffer overflows are possible

Рассмотрим второй пример ИК ПО следующего вида:

Пример 2.

Исходная С программа

#include<string.h>

#include<stdio.h>

int main(int argc, char^** argv)

{

if (argc<2)

return 0;

int len=strlen(argv[1]);

char^* p=malloc(len+1);

strcpy (p, argv[1]);

printf(”%s\n”, p);

return 0;

}

На первом этапе работы АПБ-А фрагмент дерева разбора ИК ПО, полученного на этом этапе применения объединенного модуля лексического и синтаксического разбора, представлен на фиг.34.

Темным цветом на иллюстрации выделено поддерево разбора, соответствующее синтаксической конструкции

int len=strlen(argv[1]);

АПБ-А содержит обращения только к внешним библиотечным функциям, поэтому встраивание функций в данном случае не требуется.

Таблица типов пуста, поскольку в данном примере используются только простые типы данных или указатели на них.

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

Рассмотрим два случая:

случай (а): база знаний D6 содержит аннотации для функций strcpy, malloc:

function-annotation (strcpy) {

params {^*src}

output {^*dest}

pre-conditions {

m_0 src@is_string==1;

m_0 src@size>src@strlen;

m_0 dest@size>dest@offset+src@strlen;

}

instruction {

m_0 dest@is_string=1;

m_1 dest@strlen=src@strlen;

}

}

function-annotation (malloc) {

params {n}

output {^*ptr}

pre-conditions {

}

instructions {

m_0 condition _unknown__ ? m_1 : m_5;

m_1 assign ptr@is_null=0;

m_2 assign ptr@size=n;

m_3 assign ptr@offset=0;

m_4 goto m_7;

m_5 assign ptr@is_null=0;

m_6 assign ptr@size=0;

}

}

случай (б): база знаний D6 пополнена аннотацией для функции strlen:

function-annotation (strien) {

params {buf}

output {length}

pre-condition {

m_0 buf@is_string==1;

m_0 buf@size>buf@strlen;

}

instructions {

m_0 length=buf@strlen;

}

}

При этом в случаях (а) и (б) будут получены различные

внутренние представления исходной программы - база данных D7;

базы данных D8 условий корректности;

информационные базы знаний D10;

отчеты об обнаруженных уязвимостях - база данных D111.

В приведенном втором примере присутствуют лишь вызовы библиотечных функций, поэтому модули B.1 и В.2 не выполняют преобразований.

В данном примере присутствует условная конструкция if. Поэтому на этапе работы модуля В.3 она будет преобразована в конструкцию cond-goto (эта конструкция отсутствует в языке Си, однако для простоты мы будем представлять модифицированное дерево разбора в виде программы на языке ”псевдо-Си”).

После выполнения преобразования модулем В.3 из исходных данных получается следующий код:

int len;

char ^*р;

goto (argc<2) ? label1 : label2;

labell:

return 0;

label2:

len=strlen(argv[1]);

p=malloc(len+1);

strcpy (p, argv[1]);

printf(”%s\n”, p);

return 0;

Как можно видеть, добавлены 2 метки и инструкция условного перехода.

На этапе работы модуля В.4 получают внутреннее представление ИК ПО в виде:

(а)

L1 assign	argv@size=argc;
L2 condition	argc<2 ? L5 : L3;
L3 assign	argv@1@is_string=1;
L4 assign	argv@1@size=argv@1@strlen+1;
L5 assign	argv@1@offset=0;
L5 assign	len= unknown ;
L6 assign	p@size=len+1;
L7 assign	p@offset=0;
L8 assign	p@is_string=1;
L9 assign	p@strlen=argv@1@strlen;
L10	stop;

Инструкции L1, L3 и L4 соответствуют специальным аннотациям, используемым для входных параметров функции main - argc, argv в данном случае. Эти аннотации показывают, что параметр argc равен длине массива argv, а каждый используемый в исходном коде элемент argv[i] является корректной Си-строкой, то есть последовательностью char-символов, оканчивающейся символом '\0'.

Инструкция L2 соответствует проверке условия

if (argc<2)

return 0;

Инструкция L5 соответствует выражению

int len=strlen(argv[1]);

(при этом unknown указывает на неопределенность возвращаемого значения неизвестной функции strlen).

Инструкция L6 получается из выражения

р=malloc(len+1);

и правила вывода в базе аннотаций для функции maiioc (секция instructions):

buf@size=size

buf@offset=offset

применяемого к выражениям р (вместо buf) и len+1 (вместо size).

Инструкции L8, L9 получаются из выражения

strcpy (p, argv[1]);

и правил вывода в базе аннотаций (функция strcpy, секция instructions).

dest@is_string=1

dest@strlen=src@strlen

применяемым к выражениям р (вместо dest) и argv@1 (вместо src).

(б)

L1 assign	argv@size=argc;
L2 condition	argc<2 ? L10 : L3;
L3 assign	argv@1@is_string=1;
L4 assign	argv@1@size=argv@1@strlen+1;
L5 assign	len=argv@1@strlen;
L6 assign	p@size=len+1;
L7 assign	p@offset=0;
L8 assign	p@is_string=1;
L9 assign	p@strlen=argv@1@strlen;
L10	stop;

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

length=buf@strlen,

примененным к выражениям len (вместо length) и argv@1 (вместо buf), что породит инструкцию L5.

База знаний D9 условий корректности в случаях (а) и (б) будет иметь следующий вид:

L5 1<argv@size;

L5 argv@1@is_string==1;

L5 argv<?1@size>argv@1@strlen:

L8 1<argv@size;

L8 argv@1@is_string==1;

L8 argv@1@size>argv@1@strlen;

L8 p@size>p@offset+argv@1@strlen;

Жирным выделены условия, появляющиеся в D9 при пополнении базы знаний D6 аннотаций. Рассмотрим каждое из условий более подробно.

Условие:

L5 1<argv@size;

позволяет гарантировать отсутствие переполнения при разыменовании argv[1] в выражении

int len=strlen(argv[1]).

Пара условий в точке L5, выделенных жирным шрифтом:

L5 argv@1@is_string==1;

L5 argv@1@size>argv@1@strlen;

получается в случае (б) по правилам вывода в базе аннотаций (функция strlen, секция conditions):

buf@is_string==1

buf@size>buf@strlen

примененным к выражению argv@1 (вместо buf).

Условие

L8 1<argv@size;

позволяет гарантировать отсутствие переполнения при разыменовании argv [1] в выражении

strcpy(p, argv[1]);

Тройка условий в точке L8

L8 argv@1@is_string=1;

L8 argv@1@size>argv@1@strlen;

L8 p@size>p@offset+argv@1@strlen;

получается по правилам вывода в базе аннотаций (функция strcpy, секция conditions):

src@is_string==1

src@size>src@strlen

dest@size>src@strlen

примененным к выражениям argv@1 (вместо src) и р (вместо dest).

База знаний D9 соответствия условий корректности подозрительным точкам исходного кода в случае а):

1 main.с:9:20:26 0.67 Unable to deduce dereferencing upper bound;

2 main.с:11:13:19 0.67 Unable to deduce dereferencing upper bound;

3 main.с:11:3:20 1.0 Buffer is not a valid string;

4 main.с:11:3:20 1.0 Source buffer size is less than string length;

5 main.с:11:3:20 1.0 Target buffer size is less than string length;

База знаний D9 соответствия условий корректности подозрительным точкам исходного кода в случае б):

1 main.с:9:20:26 0.67 Unable to deduce dereferencing upper bound;

2 main.с:11:13:20 1.0 Buffer is not a valid string;

3 main.с:11:13:20 1.0 Target buffer size is less than string length;

4 main.с:11:13:19 0.67 Unable to deduce dereferencing upper bound;

5 main.с:11:3:20 1.0 Buffer is not a valid string;

6 main.с:11:3:20 1.0 Source buffer size is less than string length;

7 main.с:11:3:20 1.0 Target buffer size is less than string length;

На следующем этапе разбора управление передается АПБ-С. При этом работа модуля С1 достаточно полно продемонстрирована в примере 1, поэтому укажем только результат его работы:

в точке L1:

в точке L2:

argv@size - argc==0

# predicate - L1

в точке L3:

argv@size - argc==0	# predicate - L1
argc>=2	# spectrum argc: [2, +inf) - L2

в точке L4:

argv@size - argc==0	# predicate - L1
argc>=2	# spectrum argc: [2, +inf) - L2
argv@1@is_string==1	# spectrum argv@1@is_string: {1} - L3

в точке L5:

argv@size - argc==0	# predicate - L1
argc>=2	# spectrum argc: [2, +inf) - L2
argv@1@is_string==1	# spectrum argv@1@is_string: {1} - L3
argv@1@size - argv@1@strlen==1	# predicate - L4

в точке L6:

argv@size - argc==0	# predicate - L1
argc>=2	# spectrum argc: [2, +inf) - L2
argv@1@is_string==1	# spectrum argv@1@is_string: {1} - L3
argv@1@size - argv@1@strlen==1	# predicate - L4
len - argv@1@strlen==0	# predicate - L5

в точке L7:

argv@size - argc==0	# predicate - L1
argc>=2	# spectrum argc: [2,+inf) - L2
argv@1@is_string==1	# spectrum argv@l@is_string: {1} - L3
argv@1@size - argv@1@strlen==1	# predicate - L4
len - argv@1@strlen==0	# predicate - L5
p@size - len=1;	# predicate - L6

в точке L8:

argv@size - argc==0	# predicate - L1
argc >=2	# spectrum argc: [2, +inf) - L2
argv@1@is_string==1	# spectrum argv@1@is_string: {1} - L3
argv@1@size - argv@1@strlen==1	# predicate - L4
len - argv@1@strlen==0	# predicate - L5
p@size - len=1;	# predicate - L6
p@offset=0 #	spectrum p@offset: {0} - L7

в точке L9:

argv@size - argc==0	# predicate - L1
argc>=2	# spectrum argc: [2, +inf) - L2
argv@1@is_string==1	# spectrum argv@1@is_string: {1} - L3
argv@1@size - argv@1@strlen==1	# predicate - L4
len - argv@1@strlen==0	# predicate - L5
p@size - len==1;	# predicate - L6
p@offset==0	# spectrum p@offset: {0} - L7
p@is_string==1	# spectrum p@is_string: {1} - L8

в точке L10:

argv@size - argc==0	# predicate - L1
argc>==2	# spectrum argc: [2, +inf) - L2
argv@1@is_string==1	# spectrum argv@1@is_string: {1} - L3
argv@1@size - argv@1@strlen=1	# predicate - L4
len - argv@1@strlen==0	#predicate - L5
p@size - len==1;	# predicate - L6
p@offset==0	# spectrum p@offset: {0} - L7
p@is_string==1	# spectrum p@is_string: {1} - L8
p@strlen - argv1@l@strlen==0	# predicate - L9

Жирным выделены те условия, которые будут выведены при пополнении базы знаний аннотаций D6, то есть в случае (б).

На следующем этапе работы модуля С.2 осуществляется генерация информационной базы знаний D10. При этом для рассматриваемого случая - случай (а), она будет содержать следующие сведения:

System 1: # correctness condition ″L5 1<argv@size;″

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

argv@size<=1

System 2: # correctness condition ″L8 1<argv@size;″

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen=1

p@size - len==1

p@offset=0

argv@size<=1

System 3; # correctness condition ”L8 argv@1@is_string==1;”

argv@size - argc==0

argc>=2

argv@1@is_string=1

argv@1@size - argv@1@strlen==1

p@size - len=1

p@offset==0

argv@1@is_string !=1

System 4: # correctness condition ”L8 argv@1@size>argv@1@strlen;″

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

p@size - len==1

p@offset=0

argv@1@size - argv@1@strlen<=0

System 5: # correctness condition ″L8 p@size>p@offset+argv@1@strlen;″

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

p@size - len==1

p@offset=0

p@size - p@offset - argv@1@strlen<=0

для случая (б):

System 1; # correctness condition ”L5 1<argv@size;″

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen=1

argv@size<=1

System 2: # correctness condition ”L5 argv@1@is_string==1;”

argv@size - argc=0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

argv@1@is_string !=1

System 3: # correctness condition ”L5 argv@1@size>argv@1@strlen;″

argv@size - argc=0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen=1

argv@1@size - argv@1@strlen<=0

System 4: # correctness condition ”L8 1<argv@size;″

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

len - argv@1@strlen==0

p@size - len==1

p@offset==0

argv@size<=1

System 5: # correctness condition ”L8 argv@1@is_string==1;”

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

len - argv@1@strlen==0

p@size - len==1

p@offset==0

argv@l@is_string !=1

System 6: # correctness condition ”L8 argv@1@size>argv@1@strlen;″

argv@size - argc==0

argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

len - argv@1@strlen==0

p@size - len==1

p@offset==0

argv@1@size - argv@1@strlen<=0

System 7: # correctness condition ”L8 p@size>p@offset+argv@1@strlen;″

argv@size - argc==0 argc>=2

argv@1@is_string==1

argv@1@size - argv@1@strlen==1

len - argv@1@strlen==0

p@size - len==1

p@offset==0

p@size - p@offset - argv@l@strlen<=0

На следующем этапе управление передается модулю С.3. Работа данного модуля достаточно полно раскрыта в примере 1, поэтому укажем только на окончательный результаты.

В случае (а): системы 1-4 не имеют решений, система 5 имеет целочисленное решение:

argc=2

argv@size=2

argv@1@size=1

argv@1@strlen=1

argv@1@is_string=1

len=0

p@size=0

p@is_string=1

p@offset=0

В случае (б): системы 1-7 не имеют решений.

Таким образом, в случае

(a) DNG={5}

(6)DNG={}.

На следующем этапе управление передается модулю С.4 ”Формирование отчета об обнаруженных уязвимостях”.

В случае (а) список DNG={5}. Из базы соответствия условий корректности подозрительным точкам исходного кода будет извлечена запись

”5 main.c:11:3:20 1.0 Target buffer size is less than string length;”

Извлекая из 11-й строки файла main.c выражение, записанное с 3-й по 20-ю позиции, получим фрагмент исходного кода, в котором возможно переполнение буфера: strcpy(p, argv[1]).

Поэтому, будет сгенерирован отчет:

List of dangerous points:

1) Possible buffer overflow vulnerability found at line 11,

positions 3…20, danger level 1.0

Fragment of the source code:

…

strcpy(p, argv [1]);

…

Possible reasons: Target buffer size is possibly less then string length

В случае (б) список DNG пуст, поэтому будет получен отчет, подтверждающий корректность программы:

No dangerous points found

No buffer overflows are possible

Пример 3.

Поскольку в предыдущих примерах таблица типов была пуста, приведем дополнительный пример ИК ПО, демонстрирующий работу модуля С.3 (”разворачивание структур”). Данный пример для простоты будет содержать отдельные участки программного кода.

Исходный код ПО:

typedef int type0;

typedef struct

{

type0 ^*a;

char ^*b;

} type1;

typedef struct

{

type1^* el;

type1 e2;

type0^* e3;

} type2;

…

type1 x;

type2 y;

…

^*y.e1=x;

x.a[20]=^*y.e3;

Таблица типов для данной части кода:

type0: int

type1: struct {type0^* a; char^* b;}

type2: struct {type1^* el; type1 e2; type0^* e3;}

На основании таблицы типов объявление переменной х типа type1 заменяется на объявление двух переменных: х_а и х_b, соответствующих полям структуры type1. Аналогичная замена происходит с объявлением переменной у, в которой сначала разворачивается объявление типа type2, а потом разворачиваются объявления получающихся переменных типа type1, в результате чего образуются 5 переменных: y_e1_a, y_e1_b, y_е2_а, у_е2_b, y_е3.

Присваивание

^*у.е1=х;

преобразуется в пару присваиваний, соответствующих полям типа type1:

^*У_е1_а=х_а;

^*у_е2_b=х_b;

Остальные операции преобразуются аналогичным образом.

Получающийся при этом код эквивалентен коду исходной программы (в смысле операций ячейками памяти), однако содержит только переменные простых типов и указатели:

int^* х_а;

char^* x_b;

int^** y_e1_a;

char^** y_e1_b;

int^* y_e2_a;

char^* y_e2_b;

int^* y_e3;

^*y_e1_a=x_a;

^*y_e2_b=x_b;

x_a[20]=^*y_e3.

В общем случае процесс верификации ИК ПО для распределенных вычислительных комплексов представляет динамическую процедуру приема и обработки ИК ПО по зависимым и независимы каналам. При этом АПБ-У осуществляет обработку сигналов, возникающих на системной шине устройства верификации (см. фиг.1) в процессе интерактивной верификации ИК ПО и работы АПБ-А, АПБ-В и АПБ-С. Эти сигналы поступают на входы У1 (блока нормирующих преобразователей (БНП)) (см. фиг.28), при этом согласно предлагаемому способу эти сигналы разбивают на две группы. Для определенности будем полагать, что первая группа сигналов характеризует независимые по времени интерактивные процессы верификации ИК ПО, например, первая группа сигналов представляет набор наблюдаемых интерактивных процессов обработки ИК ПО, поступающих по независимым интерфейсным каналам:

{Х(1), Х(2), Y(1), Y(2), Z(1), Z(2)}, n=3.

Вторая группа сигналов поступает по зависимым интерфейсным каналам. Для определенности дальнейшего изложения будем полагать, что эти сигналы представляют работу АПБ-А, АПБ-В, АПБ-С или оператора ЭВМ (в общем случае лица, принимающего решение - ЛПР, агента и т.п.), т.е. это некоторая реакция вида:

Следовательно, в рассматриваемом примере реализации АПБ-У в первой группе будет три независимых канала (n=3) измерений состояния процесса верификации ИК ПО, а во второй - 2ⁿ (в данном случае восемь) зависимых каналов измерений состояния процесса верификации ИК ПО распределенных вычислительных комплексов. При этом согласно способу верификации ИК ПО в распределенных вычислительных сетях необходимо хранить в базе данных соответствующие оценки верхних и нижних значений результатов верификации по каждому каналу обработки ИК ПО, т.е. ∀t>0:

X(1)=inf X₁(t) или X(1)→min X₁(t),

Х(2)=sup X₁(t) или Х(2)→max X₁ (t),

аналогично

Y(1)=inf Y₁(t) или Y(1)→min Y₁(t),

Y(2)=sup Y₁(t) или Y(2)→max Y₁(t),

Z(1)=inf Z₁(t) или Z(1)→min Z₁(t),

Z(2)=sup Z₁(t) или Z(2)→max Z₁(t).

Для этого перед началом каждого цикла верификации ИК ПО, например, в момент

t₀ формируется сигнал общего сброса на все регистры памяти и обработки сигналов измерений о состоянии основных циклов верификации ИК ПО (этот процесс на фиг. не показан). На первом временном интервале с помощью модуля коммутатора У2 осуществляется опрос следующих каналов БНП У1: первый канал БНП У1 из первой группы независимых интерфейсных каналов устройства верификации ИК ПО, на который поступает в рассматриваемом случае - Х(1); третий канал - Y(1) и пятый - Z(1). Одновременно из второй группы каналов опрашивается первый канал, на который подается для измерения сигнал U(1).

Для рассматриваемого примера этот процесс комбинаторного опроса каналов системной шины устройства верификации ИК ПО из разных групп и запоминание значений сигналов завершается за восемь тактов. Описанная последовательность операций интерактивной верификации ИК ПО реализована на основе фиксации верхних {Х(2), Y(2), Z(2)} и нижних {Х(1), Y(1), Z(1)} границ изменения амплитуд сигналов первой группы каналов измерения состояния основных процессов интерактивной верификации ИК ПО.

Описанную последовательность опроса в предложенной реализации обеспечивает модуль формирования динамической развертки графоаналитического растра (МФДРГАР) У5. Эту процедуру в рассматриваем случае обеспечивает блок У5.3 синхронизации (см. фиг.30) за восемь тактов. Здесь для простоты пояснений полагаем, что значения амплитуд возмущающих воздействий, в качестве которых в данном случае выступает поток ИК ПО, поступающий по независимым интерфейсным каналам, имеет следующий вид:

{Х(1), Х(2), Y(1), Y(2), Z(1), Z(2)}, n=3.

Соответственно, реакция на эти воздействия:

исследуемого процесса верификации ИК ПО, для всех t={t₁,…,t₈}.

При этом комбинаторика процедуры (или стратегия) опроса каждого последующего цикла определения точек уязвимости в процессе верификации ИК ПО будет зависеть не только от того, какие претерпели изменения соответствующие измеряемые переменные по каждому из каналов, но и непосредственно зависеть от результатов верификации ИК ПО, которые сопровождаются визуализацией результатов - отображением на БВ У6 (см. фиг.28, 37 и 39).

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

U'(1)=f_j1(X'(1),Y'(1),Z'(1)),

U'(2)=f_j2(X'(2), Y'(2), Z'(2)),

…

U'(8)=f_j8(X'(2), Y'(2), Z'(2)).

Одновременно (в данном примере, начиная с такта t_g) в блоке выделения экстремума У4.3 МФСКГАР У4 осуществляется процедура определения maxU(.) и minU(.).

Схема У 4.5 формирования дискретных приращений (см. фиг.29) статических координат графоаналитического растра обеспечивает циклическое изменение следующих переменных:

Х (t₁)→X₁, minU(.)→U₁,

YX (I)=(X₁ - BX)^*MX, I=1,N3, N3=int₂[N+1],

YU (I)=(U₁ - BU)^*MU, I=1,N3, N3=int₂[N+1], N={1, 2,…n}.

При этом на каждом i-м такте (в рассматриваемом примере начиная с t₁₈) осуществляется запоминание и накопление приращений, соответственно в XI=XI+НХ и UI=UI+HU, где HХ и HU - постоянные приращения, зависят от физических размеров окна экрана для отображения на БВ У6 результатов верификации ИК ПО. На каждом из i циклов, синхронно с изменением значения i, осуществляется запись полученных YX(.) и YU(.) во второе ЗУ У4.7 МФСКГАР У4 (см. фиг.29) по адресу (i+k), где k - некоторое фиксированное (заданное) смещение адреса в ОЗУ. Начиная с такта t_k1=19+10N3, начинает работу вторая схема У5.1 формирования дискретных приращений динамических координат графоаналитического растра МФДРГАР (см. фиг.30), которая обеспечивает приращения как со знаком ”+” так и со знаком ”-”, соответствующие амплитуды сигналов: YI⁺, ZI⁺ и YI^-, ZI; с постоянным приращением HY и HZ. Причем формирование каждого приращения

YI⁺(1) на такте t_k1=19+10N3,

YI⁺(2) на такте t_k2=24+10N3,

…

YI⁺(N3) на такте t_k3=14+15N3,

совмещено с формированием на выходах блока преобразования статических координат графоаналитического растра У4.6:

FX⁺(1) на такте t_s1, s₁=22+10N3,

FX⁺(2) на такте t_s2, s₂=27+10N3,

…

FХ+(N3) на такте t_s3, s₃=17+15N3.

Данные запоминаются во втором У4.7 по соответствующему i-му адресу. Начиная с i=N31=int₂[N3+1] такта осуществляется аналогичный циклический процесс формирования приращений ZI⁺(1),…, ZI⁺(N3) и FY⁺(1),…,FY⁺(N3).

Начиная с такта t_k9 (i=N4=int₂[2^*N+1]), осуществляется формирование на основе циклических приращений следующих переменных:

YI^-(1), YI^-(2),…. YI^-(N3) и FX^-(1), FX^-(2),…. FX^-(N3).

Особенность формирования каждого из данных сигналов (например, амплитуда FX^-(.) формируется за девять тактов), которые представляют координаты искомого отображения графоаналитического бинарного поля состояния процесса верификации ИК ПО, состоит в том, что этот процесс осуществляется без промежуточных операций запоминания соответствующих графических объектов в базах данных D4, D5 и D11.

Это позволяет достигнуть предельного быстродействия процесса генерации искомых взаимосвязанных параметрических зависимостей в базах данных и базах знаний в виде обобщенных визуальных отображений динамики процесса верификации ИК ПО распределенных вычислительных комплексов. При этом в блоке У5.3 синхронизации (см. фиг.30) достаточно наличия простого цикла счета (например, последовательного счета импульсов) для формирования адреса записи/считывания. Таким образом, описанное совмещение нескольких функций, связанных с формированием адресов (координат) записи их содержимого по каждому из данных адресов, обеспечивает наиболее высокое быстродействие получения визуальных графо-аналитических образов многомерных данных на плоскости БВ У6.

Режим вывода сформированных графических объектов о состоянии процесса верификации ИК ПО в МР У6.1 (см. фиг.31) может быть осуществлен на основе использования стандартных средств, например, используя ЭЛТ с интерфейсным блоком в виде буферного ЗУ. При этом, если количество строк (разрешение) ЭЛТ равно v, а количество точек в строке n, то объем буферного ЗУ должен составлять n ^* v. Режим вывода информации о состоянии процесса верификации ИК ПО на экран БВ У6 в этом случае будет осуществляться по аналогии режима ввода, при одном дополнительном условии - согласования его начала с началом кадрового синхроимпульса. При этом строб готовности (начало кадра) устанавливает на адресных входах буферного ЗУ нулевой адрес и по каждому синхросигналу увеличивается текущее значение адреса на единицу. В этом случае максимальный адрес будет равен (n^*v - 1). Следовательно, информация в каждой ячейке буферного ЗУ МР У6.1 должна храниться в течение времени развертки одного кадра.

Проекция электронного луча на экране электронно-лучевой трубки МР У6.1 передается на рабочую поверхность преобразователя оптического сигнала У6.4 (в простейшем случае это может быть фотодатчик или ПЗС-матрица) через оптическую систему У6.3 и маску У6.2, выполненную так, что в трехмерном пространстве выделены области, соответствующие гипотезам о различных состояниях уязвимости анализируемого ИК ПО.

При этом оптический коэффициент пропускания маски У6.2, через которую проходит оптический сигнал, имеет одно и то же значение для точек одной гипотезы о состоянии уязвимости ИК ПО и различное для других значений гипотез. Маска У6.2 изготовлена так, что в пространстве ее координат (X, Y, Z) выделены области уязвимости ИК ПО и соответствующие значения могут быть определены из следующего выражения энтропии:

где f(.) - любая интегрируемая по Риману функция или параметрическая зависимость оценки уязвимости ИК ПО (см. пример №2),

Xi, Yj и Zk - текущие значения переменных (или параметрических зависимостей) - входных переменных - (параметров) независимых (или зависимых) координат, о различных состояниях верифицируемого ИК ПО.

Оптический коэффициент пропускания маски У6.2 имеет одно и то же значение для точек, принадлежащих одному и тому же значению H_ijk(.), и различное - для других значений гипотез уязвимости H_ijk(.) ИК ПО. Данное свойство может быть реализовано, например, с помощью интенсивности почернения, густотой штриховки или частотой точек соответствующих участков маски при учете апертуры электронного луча и разрешающей способности преобразователя оптического сигнала (в простейшем случае - фотоприемника, ПЗС-матрицы и т.п.). Это позволяет при входных величинах Xi, Yj и Zk получать на выходе 2 блока динамической развертки У6.5 сигнал с амплитудой, равной H_ijk(.), и с частотой, определяемой параметрами соответствующих генераторов развертки.

В простейшем случае реализации БВ У6 электронный луч перемещается по экрану модуля регистрации У6.1 (см. фиг.31) по заданной траектории на основе управляющих сигналов, поступающих на его вход 2 из блока динамической развертки У6.5.

Рассмотрим процесс формирования периода и длительности следования управляющих воздействий на выходе 1 импульсного регулятора У7, когда на его входе 1 абсолютное значение гипотез уязвимости |H_ijk(.)| ИК ПО, получаемое на выходе блока определения абсолютных значений У7.1, меньше Δ_н/2, где Δ_н/2 - зона срабатывания первого релейного элемента У7.2 (см. фиг.32, пример реализации импульсного регулятора) и соответствующее ей нормированное значение |e(t)<1. Предполагаем, что нормирование текущих значений H_ilk(.) (соответственно значения ошибки определения точек уязвимости ИК ПО - e(t)) осуществляется с коэффициентом Δ=Δ_н/2.

Пусть в исходном положении триггер У7.6 находится в единичном состоянии, тогда на выходе первого блока выборки-хранения У7.7 будет напряжение

которое подается на первый вход первого сумматора У7.12, на второй вход которого поступает постоянное напряжение (Е) от источника эталонных напряжений У7.11.

В результате на вход первого формирователя импульсов У7.10 подается постоянное напряжение вида:

U_фi=U_i+Е.

Постоянная составляющая Е может быть выбрана, например, из интервала значений с нижней границей, определяемой длительность выполнения самой продолжительной последовательности операций преобразований (обработки) в АПБ устройства верификации ИК ПО, и верхней границей, определяемой, например, как 1/(K_f ^*F_max), где F_max - максимальная частота изменения значений Н_ijk(.), K_f - постоянный коэффициент, который согласно теореме отсчетов во временном представлении непрерывных сигналов в дискретной форме можно установить ≥2.

В этой связи верхняя граница значений данного интервала может быть априорно выбрана из необходимого условия адекватности представления процесса верификации ИК ПО своими дискретными значениями. Это позволяет обеспечить измерение и обработку значений сигнала Н_ijk(.) с наименьшей потерей информации о состоянии процесса верификации ИК ПО.

Далее в соответствии с U_фi на выходе формирователя импульсов У7.10 будет сформирован импульс длительностью:

Т_i=К_фi ^*U_фi,

где К_фi - коэффициент передачи формирователя импульсов У 7.10.

Во время действия данного периода Т_i в первом блоке выборки-хранения У7.7 формируется напряжение вида:

В конце периода Т_i формирователь импульсов У7.10 устанавливает триггер У7.6 в следующее (например, нулевое) устойчивое состояние.

Описанные выше последовательности операций непрерывно повторяются в функциональной зависимости от изменения ошибки определения точек уязвимости ИК ПО - e(t). При этом на каждом из периодов Т_i, i=1, 2,…,n, на первый вход первого логического элемента И У7.3 от первого формирователя импульсов У7.10 подается разрешающий сигнал на включение ключа У7.15, коммутирующего входную цепь второго формирователя импульсов У7.16. В момент окончания каждого периода Т_i и начала следующего Т_i+1, составляющие незначительный по продолжительности промежуток времени, формируется сигнал, достаточный для отключения электронного ключа У7.15. Этим обеспечивается требуемая степень синхронизации между началом момента формирования периода управляющих воздействий в первом формирователе импульсов У7.10 и длительности импульса во втором формирователе импульсов У7.16 для всех T_i, i=1,2,…,n.

При этом формирование напряжений на входе второго формирователя импульсов У7.16 реализовано по схеме, аналогичной вышеописанной на входе первого формирователя импульсов У7.10, с тем лишь отличием, что формирование длительности (t_i) выходных импульсов осуществляется в соответствии со значением оценки интегрального изменения квадрата нормированного сигнала H_ijk(.) (ошибки определения точки уязвимости ИК ПО) и во все периоды Т_i, для которых

где Δ_тр - зона нечувствительности второго релейного элемента У7.4, устанавливаемая на основе критерия точности воспроизведения (распознавания, прогнозирования и т.п. точек уязвимости ИК ПО распределенных вычислительных комплексов) текущих значений сигнала H_ijk(.). Контроль за выполнением этих условий реализован с помощью первого логического элемента И У7.3, управляющего состоянием электронного ключа У7.15 в соответствии с сигналами, поступающими с первого формирователя импульсов У7.10 и релейных элементов У7.2 и У7.4, контролирующих значения Δ_н/2 и Δ_тр соответственно. Следовательно, формирование каждого периода Т_i осуществляется на основе последовательности операций (К_фi ^*Е), априорных по отношению к динамике изменения значений сигнала H_ijk(.), и корректируется текущими значениями интегральных оценок нормированной ее оценки, полученными на предшествующем периоде дискретизации процесса верификации ИК ПО распределенных вычислительных комплексов.

При этом для всех e(t)∈[-Δ_н/2, Δ_н/2] и t>0 всегда выполняется неравенство вида Т_i>t_i, за исключением только тех моментов времени, для которых вероятность наличия уязвимости в ИК ПО равна нулю (т.е., e(t)=0) или она не выходит за пределы допустимых значений (а именно, не больше |e(t)|=Δ_н/2).

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

1. Способ генерации баз знаний для систем верификации программного обеспечения (ПО) распределенных вычислительных комплексов (РВК), включает совмещение процессов ввода и обработки исходного кода ПО по зависимым или независимым каналам на основе использования сенсорных или механических манипуляторов рабочего места оператора ЭВМ, сетевых интерфейсов локальной или глобальной сети, при этом участки или точки уязвимости исходного кода ПО определяют на основе преобразования исходного кода ПО во внутреннее представление, которое хранят в виде баз знаний, а точки или участки уязвимости исходного кода ПО определяют на основе автоматического составления и решения соответствующих систем уравнений, в процессе верификации исходного кода ПО на экране блока видеоконтроля (БВ) аппаратно-программного блока процессорного управления осуществляют синтаксическую подсветку для визуализации участков уязвимости исходного кода ПО, при этом используют граф операторов исходного кода ПО во внутреннем представлении инструкций языка программирования.

2. Способ по п.1, отличающийся тем, что диагностику процесса верификации исходного кода ПО осуществляют на основе измерения длительности выполнения основных этапов (циклов) поиска уязвимости и сопоставления полученных значений с ранее предписанными или предсказанными оценками показателя критичности уязвимости исходного кода ПО.

3. Способ по п.1, отличающийся тем, что внутреннее представление исходного кода ПО на языке программирования Си представляется в виде динамических массивов и соответствующих баз знаний, которые используются в реальном масштабе времени для верификации ПО распределенных вычислительных комплексов.

4. Способ по п.1, отличающийся тем, что точки или участки уязвимости исходного кода ПО определяют на основе автоматического составления и решения линейных систем уравнений.

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

6. Способ по п.1, отличающийся тем, что в качестве независимых каналов используют интерфейс последовательного порта или сетевой интерфейс.

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

8. Способ по любому из пп.1-7, отличающийся тем, что осуществляют генерацию баз знаний на основе использования аннотаций внешних функций ИК ПО РВК, при этом база знаний представляет набор правил или моделей протоколов верификации ИК ПО, обеспечивающих поддержку интерактивных процессов поиска уязвимости ПО.

9. Устройство для реализации способа генерации баз знаний для систем верификации программного обеспечения распределенных вычислительных комплексов (СВПО РВК), содержит аппаратно-программный блок (АПБ) лексического и семантического анализа/разбора, АПБ преобразования кода, АПБ анализа кода, АПБ процессорного управления, видеоадаптер, интерфейсы жестких, гибких и оптических дисков, интерфейс последовательного порта, сетевой интерфейс и системную память, которые объединены системной шиной, при этом системная память содержит постоянное запоминающее устройство (ROM) и оперативное запоминающее устройство (RAM/ОЗУ), в ячейках оперативной памяти и жестких дисков размещают/записывают операционные системы, прикладные программы, базы данных и базы знаний, которые содержат листинги исходных программ, грамматику языка программирования (например грамматику языка программирования Си), правила преобразования дерева разбора листинга программы, дерево разбора листинга программы, таблицу типов языка программирования, аннотации внешних функций, включающие их грамматику и семантику, код программ на языке внутреннего представления, условия корректности языка внутреннего представления исходного кода программы, условия проверки корректности подозрительных точек исходного кода программы, информационная база, содержащая системы ограничений в виде алгебраических уравнений и неравенств, отчеты об обнаруженных уязвимостях программного кода, включает:
указание на местоположение возможной уязвимости в исходном коде программы, которое содержит имя файла листинга программы, номер строки и номер позиции в строке программы в котором возможно переполнение буфера запоминающего устройства, контекст исходной программы, содержащий возможное переполнение или некоторую "окрестность" потенциально опасной точки переполнения буфера запоминающего устройства;
указание причины переполнения буфера запоминающего устройства - значения исходных переменных, приводящих к возникновению уязвимости исходного кода программного обеспечения;
показатель или степень критичности обнаруженной уязвимости исходного кода программного обеспечения;
указание на перечень правил или алгоритмов для устранения уязвимости исходного кода программного обеспечения,
при этом АПБ процессорного управления, обеспечивающий синхронизацию основных режимов интерактивной верификации программного обеспечения распределенных вычислительных комплексов, содержит последовательно соединенные блок нормирующих преобразователей (БНП), модуль коммутатора, модуль аналого-цифрового преобразователя (АЦП), модуль формирования статических координат графоаналитического растра (МФСКГАР), блок видеоконтроля (БВ), импульсный регулятор (ИР) и модуль формирования динамической развертки графоаналитического растра (МФДРГАР), первый и второй информационные входы/выходы которого соединены соответственно с управляющими входами модуля коммутации и аналого-цифрового преобразователя, а третий, четвертый, пятый, шестой, седьмой и восьмой - с вторым, третьим, четвертым, пятым, шестым и седьмым информационными входами/выходами МФСКГАР, при этом второй вход блока видеоконтроля объединен с седьмым информационным входом/выходом МФСКГАР и восьмым информационным входом/выходом МФДРГАР,
блок видеоконтроля (БВ) содержит модуль регистратора (МР), на выходе которого установлены маска, оптическая система и преобразователь оптического сигнала, выходом подключенный к управляющему входу блока динамической развертки, при этом оптический коэффициент пропускания маски имеет одно и то же значение для точек одной гипотезы/энтропии о состоянии уязвимости ИК ПО и различное для других значений гипотез.