Подход на основе трассировки для анализа безопасности кода

Основная информация

• ID статьи: 2510.10410
• Название: A Trace-based Approach for Code Safety Analysis
• Автор: Hui Xu (Фуданьский университет)
• Классификация: cs.PL (Языки программирования), cs.SE (Инженерия программного обеспечения)
• Время публикации: Октябрь 2025
• Ссылка на статью: https://arxiv.org/abs/2510.10410

Аннотация

Rust — это язык программирования с гарантией безопасности памяти, запрещающий неопределённое поведение. Его гарантии безопасности подтверждены многочисленными эмпирическими исследованиями сообщества, что является причиной его значительного успеха. Однако код unsafe остаётся критической проблемой в Rust. В данной статье путём анализа дизайна безопасности Rust и реальных проектов на Rust устанавливается систематическая база для понимания кода unsafe и неопределённого поведения, обобщаются стандарты корректности кода Rust и предлагаются практические рекомендации по реализации корректной инкапсуляции.

Исследовательский контекст и мотивация

Проблемный фон

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

Значимость исследования

• Широкое применение Rust в системном программировании делает безопасность кода unsafe критически важной
• Установление теоретической базы помогает разработчикам лучше понимать и использовать код unsafe
• Обеспечивает научную основу для аудита безопасности экосистемы Rust

Ограничения существующих подходов

• Отсутствует формальное описание ограничений безопасности кода unsafe
• Нет единого стандарта проверки корректности
• Отсутствует систематический метод анализа от функций к структурам и модулям

Основные вклады

1. Установление главной теоремы: Формальное доказательство отношения между неопределённым поведением и кодом unsafe, подтверждающее принцип "неопределённое поведение возникает только из кода unsafe и полностью определяется его ограничениями безопасности"
2. Предложение стандартов корректности: Установление критериев определения корректности для безопасных и небезопасных функций, структур и модулей
3. Разработка рекомендаций по инкапсуляции: Вывод практических принципов и следствий для реализации корректной инкапсуляции
4. Построение структуры аудита: Предложение систематического метода аудита на основе графа распространения небезопасности (UPG)

Подробное описание методики

Определение задачи

Основная задача статьи — установить теоретическую базу для анализа безопасности небезопасных частей кода Rust, включая:

• Входные данные: Программы на Rust, содержащие код unsafe
• Выходные данные: Определение корректности и рекомендации по инкапсуляции
• Ограничения: На основе системы типов Rust и ограничений безопасности

Архитектура теоретической базы

1. Основная теорема

Главная теорема (Theorem 1): Для хорошо типизированной программы Rust P неопределённое поведение возникает только если P содержит код unsafe и нарушает соответствующие ограничения безопасности:

P ⊢ UB ⇒ (P ∋ UC) ∧ (P ⊬ SC_UC)

где UC обозначает код unsafe, а SC_UC обозначает ограничения безопасности кода unsafe.

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

Предположение 1: Каждая функция unsafe имеет явные ограничения безопасности, обладающие:

• Универсальностью: Каждая функция unsafe имеет обязательные ограничения безопасности
• Согласованностью: Ограничения безопасности данной функции остаются неизменными во всех точках вызова

3. Стандарты корректности

Корректность безопасной функции (Definition 2):

∀P_fs, P_fs ⊬ UB

Корректность функции unsafe (Definition 3):

∀P_fu, P_fu ⊢ SC_fu ⇒ P_fu ⊬ UB

Вывод принципов инкапсуляции

Инкапсуляция функции (Corollary 4)

Унифицированное условие корректности функции:

∀fu ∈ UnsafeCallee(f), (f ∪ SC_f) ⊢ SC_fu ⇒ ∀P_f ⊢ SC_f, P_f ⊬ UB

Инкапсуляция структуры (Corollary 7)

Требования корректности структуры S = {C, F, M, d}:

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

Технические инновации

1. Метод анализа на основе трассировки: Аналогично анализу потоков данных, рассматривает код unsafe как источник загрязнения, а выход функции как приёмник
2. Иерархическая корректность: Прогрессивный анализ от функций → структур → модулей → крейтов
3. Обработка деструктивных методов: Инновационный учёт влияния изменяемых методов на инварианты безопасности других методов
4. Граф распространения небезопасности: Предоставляет визуальный инструмент аудита

Экспериментальная установка

Методы теоретической проверки

Данная работа в основном является теоретической; методы проверки включают:

1. Формальное доказательство: Логическое доказательство корректности теорем и следствий
2. Анализ реальных проектов: Проверка применимости теории на основе реальных проектов Rust
3. Тематические исследования: Демонстрация практичности метода на конкретных примерах

Критерии оценки

• Полнота теории: охватывает ли она основные сценарии кода unsafe в Rust
• Практичность: являются ли выведенные принципы практически применимыми
• Согласованность: соответствие официальным обещаниям безопасности Rust

Результаты экспериментов

Основные теоретические результаты

1. Доказательство главной теоремы: Успешно установлена причинно-следственная связь между неопределённым поведением и кодом unsafe
2. Принципы инкапсуляции: Выведены 4 основных следствия, охватывающих корректную инкапсуляцию функций и структур
3. Расширение на модули: Расширение теории на уровень модулей и крейтов, поддерживающее сильную и слабую корректность

Прикладная структура

Определение графа распространения небезопасности (UPG):

UPG G(F, E, S(C, M, d))

• F: множество узлов функций и статических методов
• E: множество рёбер, включающих вызовы unsafe
• S: множество структур, содержащих вызовы unsafe

Типы подграфов аудита

1. Узлы unsafe: требуют явной спецификации ограничений безопасности
2. Вызовы unsafe: должны удовлетворять Corollary 4 или первой части Corollary 7
3. Структуры: должны удовлетворять второй части Corollary 7

Связанные работы

Основные направления исследований

1. Исследования безопасности Rust: Эмпирические исследования сообщества гарантий безопасности Rust
2. Формальная верификация: Методы формальной верификации программ на Rust
3. Анализ кода unsafe: Инструменты статического анализа для кода unsafe

Сравнение вклада данной работы

• Теоретическая инновация: Первое установление формального отношения между кодом unsafe и неопределённым поведением
• Систематичность: Предоставление полной структуры анализа от функций до крейтов
• Практичность: Вывод практически применимых рекомендаций по аудиту

Заключение и обсуждение

Основные выводы

1. Установлена теоретическая основа для анализа безопасности кода unsafe
2. Предоставлены систематические стандарты определения корректности
3. Разработаны практически применимые методы аудита

Ограничения

1. Зависимость от предположений: Теория построена на предположениях о свойствах ограничений безопасности
2. Сложность: UPG больших проектов может быть чрезмерно сложным
3. Степень автоматизации: Требует ручного указания ограничений безопасности и инвариантов

Направления будущих исследований

1. Разработка автоматизированных инструментов для построения и анализа UPG
2. Расширение на более сложные сценарии операций unsafe
3. Интеграция с существующими инструментами статического анализа

Глубокая оценка

Преимущества

1. Теоретическая строгость: Установлена полная формальная база с чёткими доказательствами
2. Практическая ценность: Предоставлены практически применимые рекомендации по аудиту, помогающие реальной разработке
3. Сильная систематичность: Полное охватывание от функций до крейтов
4. Инновационность: Введение метода анализа на основе трассировки является новаторским

Недостатки

1. Недостаточная экспериментальная проверка: Отсутствуют проверки на больших реальных проектах
2. Отсутствие инструментальной поддержки: Не предоставлены автоматизированные инструменты реализации
3. Отсутствие анализа производительности: Не обсуждаются вычислительная сложность и масштабируемость метода
4. Ограничения предположений: Предположения о свойствах ограничений безопасности могут быть чрезмерно идеализированными

Влияние

1. Академический вклад: Предоставляет теоретическую основу для исследований безопасности Rust
2. Практическая ценность: Может направлять практику аудита безопасности проектов Rust
3. Разработка инструментов: Обеспечивает теоретическую поддержку для разработки автоматизированных инструментов анализа безопасности

Применимые сценарии

• Аудит безопасности системных проектов на Rust
• Проверка корректности стандартной библиотеки Rust и основных крейтов
• Теоретические исследования безопасности языков программирования
• Проектирование и реализация инструментов статического анализа

Библиография

1. Rust Team. Soundness (of code / a library). Rust Unsafe Code Guidelines.
2. Zihao Rao, et al. Annotating and Auditing the Safety Properties of Unsafe Rust. arXiv preprint arXiv:2504.21312, 2025.

Общая оценка: Данная статья вносит важный теоретический вклад в анализ безопасности кода unsafe в Rust, устанавливая систематическую структуру анализа. Хотя в области экспериментальной проверки и реализации инструментов есть место для улучшений, её теоретическая ценность и практический потенциал заслуживают признания. Данная работа обеспечивает прочную теоретическую основу для исследований и практики безопасности Rust.