Программные продукты и системы

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

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

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

У систем типов императивных языков программирования нет подобных механизмов. Попытки создать императивные языки с мощными системами типов сталкиваются с необходимостью решения ряда вопросов, связанных с наличием изменяемого состояния. Одновременное обеспечение и высокоуровневых, и низкоуровневых свойств зачастую приводит к появлению большого количества аннотаций типов в коде, создает препятствия к его дальнейшему расширению и поддержке. В частности, язык программирования Rust способен проверять корректность заимствования ссылок. В данном языке сделан акцент на явном выражении отношений владения, несмотря на то, что внутри выражений языка проверка выполняется неявным образом. Необходимость в предоставлении дополнительных аннотаций не позволяет использовать преимущества данного языка для анализа существующих программ, написанных на языках, традиционно более подверженных ошибкам работы с памятью – С/C++.

Подробное описание дается в статье «Построение модели программного кода для обнаружения программных дефектов при помощи систем типов», авторы: Цветков Л.В., Спивак А.И. (Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики (Университет ИТМО)).