Дефект, который справедливо считается «чумой» современного программирования преодолим. Предлагаем ознакомиться с переводом статьи Бертрана Мейера, французского учёного, создателя языка программирования Eiffel, приглашенного профессора и руководителя Лаборатории программной инженерии Университета Иннополис. Оригинал статьи опубликован в журнале Сommunications of the ACM.

Код имеет большое значение — об этом мы говорили в предыдущей статье. Языки программирования играют не менее важную роль. Несмотря на то, что Eiffel больше известен принципами Design by Contract («проектирование по контракту»), они являются лишь частью систематического проектирования, основная цель которого — помочь разработчикам реализовать максимум своих возможностей и устранить из кода источники сбоев и ошибок.

Говоря об источниках сбоев, стоит упомянуть разыменование нулевого указателя — дефект, который справедливо считается «чумой» современного программирования. Данный термин обозначает явление, которое происходит, когда вы делаете вызов x.f, означающий «применить компонент f (доступ к полю или операции) к объекту, на который ссылается x». Если ваша задача — определить значащие структуры данных, необходимо разрешить использование значения null, также известного как Nil или Void, как одного из возможных значений ссылочных переменных (например, для завершения связанных структур данных: поле «next» последнего элемента списка должно быть нулевым, чтобы указать, что следующий элемент отсутствует). Далее следует убедиться, что вызов x.f никогда не применяется к нулевому значению x, поскольку в этом случае отсутствует объект, к которому применяется f.

Эта проблема довольно актуальна для объектно-ориентированных языков, в которых вызовы вида x.f являются ключевым механизмом. Риск неопределённого поведения возникает при каждом использовании этого механизма (сколько миллиардов таких случаев уже произошло к тому моменту, как вы прочитаете эту статью?). Компиляторы для большинства языков программирования улавливают другие ошибки подобной природы — в частности, ошибки, связанные с типом объявления, например, когда переменной присваивается неверное значение. Тем не менее, компиляторы не могут предотвратить разыменование нулевого указателя.

Разыменование нулевого указателя — основная уязвимость, которая ставит под угрозу реализацию большинства современных программ. По мнению Тони Хоара, разыменование нулевого указателя — «ошибка на миллиард долларов». И это нисколько не преувеличение. Александр Когтенков в своей кандидатской диссертации исследовал дефекты, связанные с разыменованием нулевого указателя, основываясь на базе данных типичных уязвимостей и рисков (CVE), в которой содержится информация об Интернет-атаках. Результаты исследования представлены в графике, где отображается общее количество атак в год.



За числом атак стоят пугающие реальные случаи. Исходя из описания уязвимостей CVE-2016-9113: Разыменование указателя NULL в функции imagetobmp модуля convertbmp.c:980 OpenJPEG 2.1.2 image->comps[0].data не присваивает значение после иницализации (NULL). Резульетат — отказ в обслуживании.

Да, это случай со стандартом JPEG. Постарайтесь не думать об этом, загружая свои фото в сеть. Всего за один месяц (ноябрь 2016) в базе данных системы были зафиксированы уязвимости, связанные с разыменованием нулевого указателя, повлиявшие на продукты Gotha в ИТ-индустрии, начиная от Google и Microsoft («теоретически, кто угодно мог обрушить сервер, смастерив всего один «специальный» пакет данных») до Red Hat и Cisco. Компания NVIDIA прокомментировала это так: Продукты NVIDIA Quadro, NVS и Ge-Force, а также NVIDIA Windows GPU Display Driver R340 версии до 342.00 и R375 версии до 375.63 обнаружили уязвимость в драйвере (nvlddmkm.sys), где разыменование указателя NULL, вызванное вводом недопустимого пользователя, может привести к отказу в обслуживании или потенциальной эскалации привилегий.

Люди часто жалуются, что безопасность и Интернет — вещи несовместимые. Но что, если проблема не только в проектировании (Стек протоколов TCP/IP прекрасно функционирует), а в языках программирования, которые используются для написания средств реализации этих протоколов?

Что касается языка программирования Eiffel, мы решили, что пора решить эту проблему. Ранее мы устранили небезопасные преобразования типа с помощью системы типов, избавились от ошибок управления памятью с помощью сборки мусора, от дефектов data race — с помощью механизма SCOOP. Пришло время решить проблему разыменования нулевых указателей. Теперь в Eiffel нет проблемы небезопасных вызовов – разыменование нулевого указателя здесь в принципе невозможно. Принимая вашу программу, компилятор гарантирует, что при каждом исполнении вызова x.f, переменная x будет ссылаться на конкретный объект, который реально существует.

Как нам это удалось? В этой статье мы не станем подробно описывать, как предотвратить разыменование нулевых указателей, ограничившись ссылкой на ресурс с документацией. Отметим также, что механизм постоянно совершенствуется. В настоящей статье мы расскажем об основных идеях. Оригинальная статья по данной теме стала основным докладом на Европейской конференции по объектно-ориентированному программированию (ECOOP) в 2005 году. Несколько лет спустя, пересматривая исходное решение в одной из статей, я писал: «На разработку, усовершенствование и описание технологии void safety, основанной на механизме защиты от разыменования нулевых указателей, ушло несколько недель. Инженерная работа заняла четыре года».

Это звучало оптимистично. Семь лет спустя «инженерные работы» продолжались. И дело не в защите нулевых указателей от разыменования — механизм изначально был достаточно обоснован теоретически. Целью затянувшейся доработки концепции было облегчить работу программистов. Любой механизм, лишённый багов, например, статическая типизация, обеспечивает надёжную защиту и безопасность, по следующей формуле: «запретить вредоносные схемы (иначе дефектов не избежать), сохранив полезные (иначе избавиться от дефектов было бы слишком просто — достаточно удалить все программы!), при этом не меняя принцип их работы». Так называемые «инженерные работы» включают подробный статический анализ, благодаря которому компилятор принимает безопасные типы, которые были бы отвергнуты более упрощённым решением.
На практике, сложность оптимизации решений по защите от разыменования нулевых указателей в большей степени связана с инициализацией объектов. Детали механизма можно постоянно совершенствовать, но сама идея проста: механизм основывается на объявлении типов и статическом анализе.

Система защиты от разыменования нулевых указателей разграничивает «прикрепленные» (attached) и «открепляемые» (detachable) типы. Если вы типизируете переменную р1 конкретным типом (например, PERSON), она никогда не будет нулевой — её значение всегда будет ссылкой на объект данного типа, т.е. переменная р1 является «прикреплённой». Это по умолчанию. Если вы хотите, чтобы переменная р2 приняла нулевое значение, обозначьте её как «открепляемую» — detachable PERSON. Простые механизмы компиляции поддерживают это разграничение: можно присвоить р1 в р2, но не наоборот. Таким образом, «прикреплённое» выражение является верным: во время выполнения программы значение р1 всегда будет ненулевым. Компилятор формально гарантирует это.

При статическом анализе таких гарантий гораздо больше, причём это не требует каких-то усилий со стороны программистов, если код безопасен. Например, если фрагмент кода выглядит так:
if p2 /= Void then p2.f end, мы знаем, что всё в порядке (при определённых условиях. В многопоточном программировании, например, важно, чтобы параллельный поток не обнулил переменную р2 в промежуток между ее проверкой и применением f. Это предусмотрено правилами).

Разумеется, реальное определение механизма не гарантирует, что компилятор распознает безопасные случаи и отклонит небезопасные. Мы не можем просто доверить безопасность программы программному инструменту (даже таким инструментам с открытым исходным кодом, как компиляторы Eiffel). Кроме того, есть нечто большее, чем просто компилятор. Определение void safety использует ряд простых и понятных правил, известных как сертифицированные шаблоны прикрепления (CAPs), которые компиляторы должны соблюдать. Предыдущий пример иллюстрирует один из таких сертифицированных шаблонов. Формальная модель, подкрепленная механизированными доказательствами (с помощью инструмента Isabelle/HOL), даёт весомые доказательства обоснованности этих правил, включая деликатные вопросы, связанные с инициализацией.

Технология void safety существует уже несколько лет, и те, кто её использовал, не хотят возвращаться к прежним методам безопасности нулевых указателей. Создание безопасного кода быстро становится привычным делом.

А вы уверены, что ваш код защищён от разыменования нулевых указателей?

https://habrahabr.ru/post/333622/