Тема: Композициональные частично определенные типы в символьном интерпретаторе для платформы .NET Framework

В области верификации есть методы, которые используют техни­ку символьного исполнения [2, 12, 13] для сведения кода к языку ло­гики первого порядка и решатели дизъюнктов Хорна [8, 9, 14] для их разрешения. Одна из главных задач, решаемых символьным интер­претатором — исследование веток выполнения кода на неопределенных входных данных.
Во время символьного исполнения .NET-кода появляется пробле­ма, порождаемая неопределенностью данных, а именно неопределен­ность динамических типов объектов. Один из самых простых примеров, демонстрирующих эту проблему — функция Object.Equals(Object). Вне контекста конкретного вызова невозможно понять, какой именно объект будет передан в качестве параметра этого метода, в частно­сти, неизвестно какой у объекта будет тип. Ситуация осложняется на­личием обобщений (generics) с ограничениями на типовые параметры, а также вариантностью для обобщенных интерфейсов. Не стоит забы­вать и о сложности системы типов .NET. В частности, решение должно естественным образом масштабироваться на массивы символьных раз­мерностей, делегаты, unsafe-указатели и т. д.
Одна из главных проблем, от которой страдают символьные интер­претаторы — проблема взрыва путей исполнения: количество путей исполнения программы в общем случае зависит экспоненциально от ее размера[1]. Один из подходов, направленных на решение этой пробле­мы — это композиционное символьное исполнение [6], которое позволяет переиспользовать уже проинтерпретированные участки кода во время символьного исполнения. В случае с динамическими типами объектов композиционность заключается в возможности получить корректный результат интерпретации кода, при условии того, что типы объектов могут быть конкретизированы, без повторного исполнения.
V# — это проект, направленный на создание неограничиваемого ве­рификатора для платформы .NET. Помимо огромной важности для са­мого проекта V#, эта задача может представлять интерес для акаде­мического сообщества. К примеру, существует довольно большое ко­личество работ, посвященных статическому анализу языка Java (одна из последних обзорных статей на эту тему является [16]). Существуют и работы на тему символьного исполнения в условиях неопределенности типа объектов, например, [10]. Стоит отметить также, что в наиболее известных state-of-art-интерпретаторах (таких как Java PathFinder [7] и Pex [21]), символьное исполнение кода со сложными типами поддер­жано в весьма ограниченном виде. В частности, не один из этих ин­струментов не поддерживает исполнение кода с открытыми типами в полном объёме, хотя возможность получить корректный результат символьной интерпретации кода с открытыми типами в сочетании с композициональностью позволяет сильно повысить эффективность ис­полнения.
Купить

В данной работе были выполнены следующие задачи.
• Спроектирована архитектура подсистемы, отвечающей за интер­претацию типов.
• Реализовано символьное исполнение функций с учетом открытых типов и полиморфизма. Неопределенность динамических типов выражена в символьных типах, на которые накладываются огра­ничения в виде символьных булевых термов. Поддержка исполне­ния кода с неопределенными типами реализована с учетом композициональности исполнения.
• Предложен и реализован алгоритм, который решает ситемы огра­ничений на открытые .NET типы. В частности, разработан и реа­лизован алгоритм, который сводит задачу определения выполни­мости набора ограничений на открытые типы платформы .NET к разрешимому фрагменту логики первого порядка.
• Подана статья на конференцию SEIM 2018, c последующей пуб­ликацией в CEUR (индексируется в базе данных SCOPUS).
• Проведено тестирование функциональности реализованной под­системы.
Купить