JetBrains Research — наука, меняющая мир

Семинар по моделированию памяти С программ

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

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

В докладе представлена работа, расширяющая область применимости эффективных методов моделирования памяти. Предложен новый метод моделирования операций с указателями для инструмента дедуктивной верификации на основе SMT-решателей, позволяющий поддерживать вложенные структуры и массивы, а также произвольные объединения и приведения типов указателей. Метод был реализован в инструменте Jessie. Модернизированная версия Jessie включена в цепочку инструментов для верификации модуля безопасности (LSM – Linux Security Module) ядра ОС Linux.

Докладчик: Михаил Мандрыкин, Александр Петренко, ИСП РАН, Москва

21.11.2016, 17:15, Мат-Мех, ауд. 3248.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28