ISSN 0236-235X (P)
ISSN 2311-2735 (E)

Публикационная активность

(сведения по итогам 2017 г.)
2-летний импакт-фактор РИНЦ: 0,500
2-летний импакт-фактор РИНЦ без самоцитирования: 0,405
Двухлетний импакт-фактор РИНЦ с учетом цитирования из всех
источников: 0,817
5-летний импакт-фактор РИНЦ: 0,319
5-летний импакт-фактор РИНЦ без самоцитирования: 0,264
Суммарное число цитирований журнала в РИНЦ: 6012
Пятилетний индекс Херфиндаля по цитирующим журналам: 404
Индекс Херфиндаля по организациям авторов: 338
Десятилетний индекс Хирша: 17
Место в общем рейтинге SCIENCE INDEX за 2017 год: 527
Место в рейтинге SCIENCE INDEX за 2017 год по тематике "Автоматика. Вычислительная техника": 16

Больше данных по публикационной активности нашего журнале за 2008-2017 гг. на сайте РИНЦ

Вход


Забыли пароль? / Регистрация

Добавить в закладки

Следующий номер на сайте

4
Ожидается:
16 Декабря 2018

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

14.06.2018

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

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

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

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

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