Preview

Труды Института системного программирования РАН

Расширенный поиск
Том 38, № 5: сентябрь-октябрь
Скачать выпуск PDF
7-20
Аннотация

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

21-36
Аннотация

В данной статье представлена архитектура сетевого стека UDP/IP для операционной системы реального времени (ОСРВ) с поддержкой стандарта ARINC 653. Целевое применение транспортного протокола UDP/IP в системах интегрированной модульной авионики приводит к требованию на сертификацию программного обеспечения (ПО) по КТ178-С. Поэтому мы рассматриваем разработку сетевого стека с нуля и акцентируем внимание на его составных элементах: архитектуре нижележащего сетевого драйвера, динамическом распределении памяти, структуре данных для обработки сетевых пакетов, организации очередей пакетов и очередей таймаутов. Для тестирования нашего сетевого стека и сетевых драйверов мы предлагаем архитектуру тестовой системы, а также набор подходов по интеграции сети. Рассматриваемое ПО способно производить фрагментацию и сборку IP-пакетов, а также управлять формой трафика.

37-50
Аннотация

Оптимистическая репликация является одним из ключевых подходов к обеспечению высокой доступности географически распределённых систем, позволяя репликам временно расходиться в состоянии с последующим асинхронным согласованием. Несмотря на то, что широко распространённые бесконфликтные реплицируемые типы данных (Conflict-free Replicated Data Types, CRDT) гарантируют сильную сходимость, встроенные в них механизмы разрешения конфликтов, как правило, являются неявными и недостаточно гибкими, что ограничивает их применение в сценариях, требующих семантической прозрачности и участия пользователя в процессе разрешения конфликтов. В работе исследуется эпистемическая модель конфликтов – формальная модель, обеспечивающая явное, гибкое и не требующее координации разрешение конфликтов при сохранении гарантий сходимости. Во-первых, показано, что CRDT, основанные на состоянии, на операциях и на дельта-состояниях (delta-CRDT), естественным образом формализуются в рамках эпистемической модели, которая предоставляет единый аппарат для их бесконфликтного представления. Во-вторых, множества рассматриваются как фундаментальный реплицируемый тип данных, лежащий в основе более сложных реплицируемых структур, таких как списки, графы и отображения. Для них в рамках эпистемической модели определяются соответствующие процедуры разрешения конфликтов, реализующие семантики, известные в теории CRDT. Тем самым демонстрируется, что эпистемическая модель конфликтов обладает достаточной выразительной мощностью для формализации семантики существующих реализаций CRDT, одновременно сохраняя их интерпретируемость и семантическую прозрачность.

51-72
Аннотация

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

73-90
Аннотация

Ограничения при выполнении задач, требующих точного извлечения информации из сверхдлинных последовательностей, приводят к снижению качества генерации и отладки кода крупных объектно-ориентированных систем, характеризующихся сложными межклассовыми зависимостями и необходимостью анализа длинных трассировок выполнения, превышающих размеры стандартных контекстных окон. Предлагается технология JavaCapsule для генерации и отладки Java-кода, реализующая итеративную отладку на основе структурированной обратной связи, включающей результаты выполнения тестов и трассировки выполнения. Для обработки сверхдлинного контекста исследуется Ассоциативный рекуррентный трансформер с памятью (Associative Recurrent Memory Transformer, ARMT), демонстрирующий точность извлечения информации до 99% на последовательностях длиной до 1 миллиона токенов. Для корректной оценки разработан JavaBench+ – модернизированный набор задач с устраненными дефектами, предоставляющий расширенный цикл обратной связи. Экспериментальные результаты показывают, что JavaCapsule обеспечивает увеличение качества генерации на 20 процентов по метрике Pass@1 по сравнению с базовой моделью Google Gemma-3-27B-it, а исследование архитектуры ARMT подтверждает возможность эффективной обработки сверхдлинных последовательностей.

91-102
Аннотация

В статье описан следующий шаг развития мутационного дифференциального фаззера файловых систем DIFFuzzer, предполагающий интеграцию формальных спецификаций для улучшения его возможностей тестирования. Изначально DIFFuzzer разрабатывался на основе дифференциального подхода с интеграцией в исходный код модели POSIX, что ограничивало гибкость и масштабируемость инструмента. Предлагаемый улучшенный подход разделяет логику фаззера и модель при помощи выделения последней во внешнюю формальную спецификацию, написанную на языке LibSL. Это позволяет создавать более точные тестовые оракулы и облегчает генерацию рабочей нагрузки. В данной работе мы подробно описываем текущее состояние проекта, включая расширение LibSL и реализацию тестового оракула на основе спецификаций. Также описаны направления будущей работы и связанные с ними проблемы, такие как совершенствование формальной спецификации POSIX и развитие модуля генерации рабочей нагрузки на основе спецификаций.

102-118
Аннотация

Традиционный подход к процессному анализу (Process Mining) при работе с плоскими журналами событий в первую очередь фокусируется на аспекте потока управления, тогда как объектно-центрический подход открывает аналитические перспективы для сильно распределенных и взаимозависимых данных о событиях, порождаемых системами, основанными на сервис-ориентированной архитектуре (СОА). В частности, объектно-центрический процессный анализ (Object-Centric Process Mining, OCPM) решает эту проблему, сохраняя связи между множеством взаимодействующих объектов в более точном представлении поведения системы. В данной работе мы представляем сравнительное исследование традиционного и объектно-центрического подходов к процессному анализу, применяемых к СОА-системам, и показываем, как моделирование множества взаимодействующих объектов облегчает анализ сервисных взаимодействий. Для поддержки перехода от объектно-центрических данных о событиях к практикам разработки программного обеспечения мы разрабатываем новый инструмент, который автоматически визуализирует объектно-центрические журналы событий (восстановленные из плоских журналов) в виде объектно-центрических диаграмм последовательности (Object-Centric Sequence Diagrams, OCSD). Наш метод дополняет существующие визуализации в формате OCEL, предоставляя (i) детальную информацию о временных взаимодействиях и (ii) контекстное отслеживание. Реальное практическое исследование показывает, что наш инструмент выявляет закономерности, скрытые в сервисных взаимодействиях, такие как избыточные обращения к объектам и временные узкие места, что способствует диагностике и оптимизации распределенных сервисов.

119-132
Аннотация

В работе исследуется применимость формализма SOFA/SODA, изначально предложенного для обнаружения проблем проектирования в сервис-ориентированных системах, к задаче структурного анализа многомодульных программных проектов. Обнаружение проблем проектирования формулируется как вычисление декларативных правил над статическим графом компонентных зависимостей; предложена подключаемая архитектура, в которой любой проект, способный предоставить свой граф компонентов через небольшой интерфейс-адаптер, становится допустимым входом для анализатора. Слой SOFA реализован как фиксированный набор графовых метрик, а слой SODA – как набор декларативных карточек правил. Прототип консольной утилиты реализован на языке Go с внешними компонентами расширения правил; два адаптера покрывают инфраструктуру инструментов SwiftPM и Gradle. Оценка на двух эталонных проектах с размеченными нарушениями даёт F1=1.00 на Swift-проекте (13 нарушений, без ложных срабатываний), ноль ложных срабатываний на контрольном Kotlin-проекте и 80% правил, переиспользуемых между двумя инфраструктурами инструментов. Полученные результаты показывают, что SOFA/SODA можно переносить из сервис-ориентированных систем на структурный анализ многомодульных проектов в целом при условии наличия подходящего адаптера проекта.

133-154
Аннотация

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

155-174
Аннотация

Дистилляция диффузионных моделей является одним из наиболее многообещающих подходов к синтезу высококачественных изображений, основанных на текстовых описаниях, с минимальным количеством шагов генерации. Однако, несмотря на успехи последних лет, существующие дистиллированные модели по-прежнему не обладают всем спектром возможностей диффузионных моделей – в частности, инверсией реальных изображений, которая лежит в основе многих точных методов редактирования изображений. Настоящая работа посвящена разработке эффективных методов кодирования реальных изображений в скрытое пространство с использованием дистиллированных диффузионных моделей. Для достижения этой цели мы предлагаем обратимую дистилляцию согласованности (invertible Consistency Distillation, iCD) – обобщённый подход дистилляции согласованности, обеспечивающий как высококачественный синтез изображений, так и качественное кодирование изображений всего за 3–4 прогона нейронной сети. Хотя задача инверсии для диффузионных моделей усложняется при высоких значениях управления без классификатора (classifier-free guidance), мы показываем, что динамическое управление (dynamic guidance) существенно снижает ошибку реконструкции без заметной потери качества генерации. В результате мы демонстрируем, что iCD в сочетании с динамическим управлением может служить высокоэффективным инструментом редактирования изображений по текстовому описанию без дополнительного дообучения (zero-shot), конкурируя с более затратными современными альтернативами.

175-194
Аннотация

Современные методы дистилляции диффузионных моделей достигли значительного прогресса, обеспечивая качественную генерацию примерно за 4 шага для крупномасштабных диффузионных моделей генерации изображений и видео по текстовому описанию. Однако дальнейшее уменьшение количества шагов генерации становится всё более сложной задачей. Это наводит на мысль о том, что для повышения эффективности, возможно, стоит обратить внимание на другие степени свободы. Руководствуясь этой идеей, мы представляем SwD – подход для дистилляции диффузионных моделей с постепенным увеличением масштаба генерируемого изображения (Scale-wise Distillation, SwD), который наделяет малошаговые модели способностью к прогрессивной генерации, избегая избыточных вычислений на промежуточных шагах диффузионного процесса. Помимо повышения эффективности, SwD расширяет семейство методов дистилляции, предлагая простую функцию потерь дистилляции на уровне локальных фрагментов изображения или видео, основанную на метрике Maximum Mean Discrepancy (MMD). Эта функция потерь значительно повышает эффективность существующих методов дистилляции и демонстрирует конкурентное качество при использовании в качестве самостоятельного метода. Применённый к современным диффузионным моделям генерации изображений и видео по тексту, SwD приближается по скорости генерации к двум полноразмерным шагам и значительно превосходит альтернативы при сопоставимых вычислительных затратах, что подтверждается автоматическими метриками и исследованиями пользовательских предпочтений.

195-216
Аннотация

Производительность графовых нейронных сетей (GNN) ограничена разреженным нерегулярным доступом к памяти. Популярные библиотеки, такие как DGL и PyTorch Geometric, поддерживают обобщённую передачу сообщений, однако сложные слои нередко материализуют промежуточные тензоры по рёбрам, увеличивая трафик памяти и ограничивая масштабируемость на больших графах. Мы применяем подход, ориентированный на операции ввода-вывода и арифметическую интенсивность, и показываем, что широко используемые слои классифицируются на три семейства: свёртки на основе умножения разреженной матрицы на плотную (Sparse-Dense Matrix Multiplication, SpMM), агрегации на основе редукции и слои на основе внимания (GATv2/граф-трансформер). Для каждого семейства мы разрабатываем ядра для GPU, снижающие перемещение данных, улучшающие локальность и остающиеся устойчивыми на реалистичных графах. Мы также исследуем перестановку вершин графа и обнаруживаем, что её влияние зависит от отображения ядра: она устойчивее помогает ядрам с параллелизмом по соседям (в которых доминирует gather), чем проектам с параллелизмом по признакам. Эмпирически наши слитые ядра внимания достигают ускорения до 3,9 раз для граф-трансформера (медиана 1,6 раз), а варианты с тензорными ядрами Tensor Cores (блочно-разреженные) – до 7,3x на локально плотных графах; для слоя GATv2 мы достигаем ускорения до 8,5 раз (медиана 2,0 раз) при снижении пикового потребления памяти до 76 раз (медиана 6 раз). Наши ядра редукции с учётом степеней достигают ускорения до 10 раз (медиана 2,6 раз). Для слоёв на основе SpMM корректно кэшированный cuSPARSE (библиотека NVIDIA для разреженной линейной алгебры) достигает ускорения до 8 раз над DGL (самой популярной библиотекой для графового машинного обучения Deep Graph Library) и превосходит оцениваемые пользовательские базовые решения в большинстве оценок. Мы выпускаем наши реализации как готовые замены для поддержки воспроизводимого, учитывающего оборудование ускорения GNN.

217-234
Аннотация

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

235-256
Аннотация

В надёжных системах принятия решений на основе машинного обучения модели должны быть устойчивы к сдвигам распределения или обеспечивать меры неопределённости своих предсказаний. В задачах предсказания на уровне вершин в графовых данных сдвиги распределения особенно сложны ввиду взаимозависимости объектов. Большинство существующих графовых наборов данных разделяют вершины на обучающую и тестовую части случайным образом, не учитывая структурные свойства графа, тогда как именно они существенны для задач обучения на графах. В данной работе предлагается универсальный подход к созданию разнообразных структурных сдвигов распределения, основанный на свойствах вершин: популярности, локальности и плотности. Эмпирическое сравнение показывает, что предложенные сдвиги весьма сложны для существующих графовых методов: сдвиг на основе локальности является наиболее трудным с точки зрения устойчивости предсказания, а сдвиг на основе плотности – наиболее сложным для OOD-детекции. Мы обнаруживаем, что простые методы нередко превосходят более сложные подходы на рассмотренных структурных сдвигах, при этом существует определенный компромисс между качеством предсказания при сдвиге и способностью к OOD-детекции.

257-286
Аннотация

Хотя данные, которые можно естественным образом представить в виде графов, широко распространены в реальных приложениях самых разных отраслей, популярные наборы задач машинного обучения на графах (МО на графах) для предсказания свойств вершин охватывают удивительно узкий набор предметных областей, а графовые нейронные сети (GNN) нередко оцениваются лишь на нескольких академических сетях цитирований. Эта проблема особенно насущна в свете растущего интереса к разработке графовых фундаментальных моделей (GFM). Предполагается, что такие модели способны переносить знания на разнообразные графовые наборы данных из различных областей, однако предлагаемые GFM нередко оцениваются лишь на весьма ограниченном наборе данных из узкого круга приложений. Для восполнения этого пробела мы представляем GraphLand – 14 разнообразных графовых наборов данных для предсказания свойств вершин из широкого спектра различных промышленных приложений. GraphLand позволяет оценивать модели МО на графах на широком спектре графов с разнообразными размерами, структурными характеристиками и наборами признаков в едином формате. Помимо этого, GraphLand позволяет исследовать ранее слабо изученные научные вопросы, в частности как реалистичные временны́е сдвиги распределения в трансдуктивном и индуктивном режимах влияют на качество моделей МО на графах. Симулируя реалистичные промышленные условия, мы используем GraphLand для сравнения GNN с моделями градиентного бустинга над решающими деревьями (GBDT), популярными в промышленных приложениях, и показываем, что GBDT, снабжённые дополнительными признаками на основе графа, могут в ряде случаев быть весьма сильными базовыми моделями. Также мы оцениваем современные универсальные GFM и обнаруживаем, что они не достигают конкурентных результатов на предложенных наборах данных. Исходный код и наборы данных доступны в нашем репозитории на GitHub. Кроме того, наборы данных интегрированы в PyTorch Geometric.

287-304
Аннотация

Надежный прогресс в глубоком обучении на табличных данных начинается с трудной задачи сравнения. Если сравнить простые полносвязные нейросетевые модели (MLP), специализированные архитектуры для табличных данных и методы градиентного бустинга над деревьями решений (GBDT) на академических наборах данных в едином и тщательном протоколе, то хорошо настроенные MLP-подобные модели зачастую трудно превзойти более продвинутыми методами, а GBDT остается сильным конкурентом и задает высокую планку для области. В этой работе мы используем такой строгий протокол оценки, чтобы продемонстрировать два механизма, которые улучшают табличные нейросетевые модели относительно сильных MLP-подобных методов и GBDT. Первый механизм связан с улучшенной методологией обучения: двухэтапным обучением с искажением входных данных, вспомогательными функциями потерь и более длительным обучением. Второй механизм связан с использованием непараметрической компоненты, которые во время предсказания используют представления и метки похожих объектов из обучающей выборки. На рассмотренных открытых академических наборах данных оба направления устойчиво улучшают качество тщательно настроенных параметрических нейросетей и часто достигают уровня качества GBDT или превосходят его. Эти результаты показывают, что глубокое обучение на табличных данных может быть конкурентоспособным с методами на основе решающих деревьев при строгой оценке относительно сильных простых моделей.

305-324
Аннотация

Прогресс в исследованиях машинного обучения важен прежде всего тогда, когда он переносится с академических наборов задач в реальные приложения. Для табличного глубокого обучения это требует понимания того, какие протоколы оценки, используемые в академии, отражают практические сценарии внедрения. В этой статье мы анализируем существующие табличные наборы задач и выявляем две характеристики, типичные для промышленных задач, но слабо представленные в популярных наборах данных: временной сдвиг распределения и признаковые пространства, полученные с помощью сложных процессов сбора данных и генерации признаков. Первая характеристика требует временных разбиений на обучающую, валидационную и тестовую выборки, а вторая меняет число и структуру предиктивных, неинформативных и коррелированных признаков по сравнению с типичными академическими наборами данных. Чтобы изучить, насколько недавние достижения табличного глубокого обучения переносятся в такие условия, мы представляем TabReD – коллекцию из восьми табличных наборов данных промышленного уровня с временными разбиениями и высокоразмерными признаковыми пространствами. Мы тестируем широкий набор методов на новом наборе задач, включая градиентный бустинг над деревьями решений, полносвязные нейронные сети, векторные представления числовых признаков, модели на основе внимания, методы с непараметрической компонентой, продвинутые рецепты обучения и ансамбли. Результаты показывают, что временная оценка меняет ранжирование методов и их относительное качество по сравнению со случайными разбиениями; на TabReD наиболее устойчивыми оказываются простые полносвязные архитектуры с векторными представлениями числовых признаков и методы градиентного бустинга, тогда как ряд более сложных современных методов переносится менее надежно.

325-336
Аннотация

В работе предлагается метод автоматической проверки и исправления форматирования образовательных и научных документов, учитывающий разнообразие локальных стандартов оформления, принятых в отдельных учебных заведениях. Существующие решения либо жёстко привязаны к одному институциональному шаблону и не поддерживают автоматическое исправление, либо основаны на машинном обучении и анализируют структуру документа без детерминированной, основанной на правилах коррекции. Для устранения этого разрыва предложенный метод объединяет три компонента: древовидный расширяемый шаблон, формализующий локальные правила форматирования для каждого типа абзаца; алгоритм классификации, определяющий тип абзаца по совокупности визуальных, структурных и контекстных признаков; и механизм коррекции, сопоставляющий обнаруженные нарушения с конкретными корректирующими действиями. Метод реализован в виде клиент-серверного прототипа на базе ASP.NET Core и библиотеки OpenXML, при этом шаблон форматирования хранится в виде структурированного файла на языке XML. Апробация проводилась на выборке из 10 студенческих отчётов (1018 абзацев), ранее проверенных учебными ассистентами НИУ ВШЭ – Пермь. Точность классификации абзацев составила 87,2%, наибольшее число ошибок связано с разграничением списков, обычного текста и заголовков в документах без стилевого форматирования. Полнота выявления нарушений форматирования составила 90,8%, а 83,1% обнаруженных нарушений были устранены автоматически без внесения новых несоответствий. Автоматическая проверка документа объёмом 15-25 страниц занимала около одной минуты, тогда как большинство учебных ассистентов сообщали о затратах в 15-30 минут на ручную проверку документа сопоставимого объёма, то есть время проверки сокращается более чем в десять раз. Полученные результаты показывают, что сочетание адаптируемого шаблона правил с классификацией абзацев по нескольким признакам обеспечивает точную, прозрачную и переносимую между разными институциональными стандартами проверку форматирования, тогда как автоматическое исправление пока ограничено локально устранимыми нарушениями.

337-350
Аннотация

В рамках инструмента статической верификации программ CPAchecker рассматриваются анализ на основе символьных графов памяти (SMG) и метод мемоизации абстракций блоков (BAM), позволяющий использовать резюме процедур. SMG анализ моделирует память программы в виде графа с рёбрами между объектами в памяти и символьными значениями. С помощью этого анализа были найдены ошибки работы с памятью в драйверах операционной системы Linux. BAM позволяет, используя произвольный статический анализ, получить резюме блока (тела функции или цикла) и использовать это резюме снова, когда анализ входит в тот же блок с достаточно схожим контекстом. В этой статье представлен ряд вариантов операторов BAM, необходимых для работы этого метода с анализом SMG. Варианты различаются по точности захватываемого контекста. Использование BAM позволило анализу получить более 50 вердиктов, но привело к потере 25 вердиктов на 845 модулях драйверов.



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)