Могут ли методы проверки программы предотвратить появление ошибок жанра Heartbleed?

На вопрос об ошибке Heartbleed Брюс Шнайер написал в своей «Крипто-грамме» от 15 апреля: «Катастрофический» - правильное слово. По шкале от 1 до 10 это 11 '. Несколько лет назад я читал, что ядро ​​определенной операционной системы строго проверено современной системой проверки программ. Следовательно, можно ли предотвратить появление ошибок в жанре Heartbleed с помощью современных методов проверки программ или это все же нереально или даже принципиально невозможно?

Чтобы ответить на ваш вопрос самым кратким образом - да, эта ошибка могла быть потенциально обнаружена официальными средствами проверки. Действительно, свойство «никогда не отправлять блок, размер которого больше размера отправленного звукового импульса», довольно просто формализовать в большинстве языков спецификаций (например, LTL).

Проблема (которая является обычной критикой формальных методов) заключается в том, что используемые вами спецификации написаны людьми. Действительно, формальные методы только сдвигают задачу поиска ошибок от поиска ошибок к определению, что это за ошибки. Это сложная задача.

Кроме того, формальная проверка программного обеспечения общеизвестно трудна из-за проблемы взрыва состояния. В этом случае это особенно актуально, так как много раз, чтобы избежать взрыва состояния, мы абстрагируем границы. Например, когда мы хотим сказать «за каждым запросом следует грант в пределах 100000 шагов», нам нужна очень длинная формула, поэтому мы абстрагируем ее до формулы «каждый запрос в конечном итоге сопровождается грантом».

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

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

Программы проверки коммерческих программ, такие как Klocwork или Coverity, возможно, смогли бы найти Heartbleed, поскольку это относительно простое «забыл сделать ошибку проверки границ», что является одной из основных проблем, для которых они предназначены для проверки. Но есть гораздо более простой способ: использовать непрозрачные абстрактные типы данных, которые хорошо протестированы на отсутствие переполнения буфера.

Для программирования на Си доступно множество абстрактных типов данных «безопасная строка». Тот, с кем я больше всего знаком, это Vstr . Автор, Джеймс Антилл, подробно обсудил, почему вам нужен строковый абстрактный тип данных с его собственными конструкторами / фабричными методами, а также список других строковых абстрактных типов данных для Си .

Если вы считаете «  метод проверки программ  » комбинацией проверки границ во время выполнения и фаззинга, то да, эта конкретная ошибка могла быть обнаружена .

Правильное размытие заставит печально известное теперь memcpy(bp, pl, payload);чтение через предел блока памяти, к которому plпринадлежит. Проверка границ во время выполнения может в принципе перехватить любой такой доступ, и на практике, в данном конкретном случае, даже отладочная версия, mallocкоторая заботится о проверке параметров, memcpyмогла бы выполнить работу (здесь нет необходимости связываться с MMU) , Проблема в том, что выполнение фаззин-тестов для каждого типа сетевых пакетов требует усилий.

Использование более узкого языка не просто перемещает целевые посты от правильной реализации к правильной спецификации. Трудно сделать что-то очень неправильное, но логически непротиворечивое; вот почему компиляторы ловят так много ошибок.

Арифметика указателей в том виде, в котором она обычно формулируется, не имеет смысла, поскольку система типов на самом деле не означает, что она должна означать. Вы можете полностью избежать этой проблемы, работая на языке сборки мусора (обычный подход, который заставляет вас также платить за абстракцию). Или вы можете более точно определить, какие типы указателей вы используете, так что компилятор может отклонить все, что является непоследовательным или просто не может быть доказано, что оно правильно написано. Это подход некоторых языков, таких как Rust.

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

• int * x; // Ложное утверждение. х существует и не указывает на int
• int * y = z; // только true, если доказано, что z указывает на int
• * (х + 3) = 5; // только true, если (x + 3) указывает на int в том же массиве, что и x
• int c = a / b; // только true, если b ненулевой, например: "nonzero int b = ...;"
• обнуляемый int * z = NULL; // nullable int * - это не то же самое, что int *
• int d = * z; // Ложное утверждение, потому что z обнуляется
• if (z! = NULL) {int * e = z; } // Хорошо, потому что z не нуль
• бесплатно (у); int w = * y; // Ложное утверждение, потому что y больше не существует в w

В этом мире указатели не могут быть нулевыми. Разыменования NullPointer не существует, и указатели не нужно нигде проверять на нулевое значение. Вместо этого «nullable int *» - это другой тип, значение которого может быть извлечено либо в ноль, либо в указатель. Это означает, что в тот момент, когда начинается ненулевое предположение, вы либо регистрируете свое исключение, либо переходите к нулевой ветви.

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

Кроме того, если у вас не будет указателя, который не инициализирован, у вас не будет указателей на неинициализированную память. Если у вас есть указатель на освобожденную память, то он должен быть отклонен компилятором. В Rust существуют разные типы указателей, чтобы можно было ожидать таких доказательств. Существуют исключительно собственные указатели (то есть: без псевдонимов), указатели на глубоко неизменяемые структуры. Тип хранилища по умолчанию является неизменным и т. Д.

Существует также проблема применения фактической четко определенной грамматики для протоколов (которая включает элементы интерфейса), чтобы ограничить область входной поверхности в точности тем, что ожидается. Суть «правильности» в следующем: 1) избавиться от всех неопределенных состояний 2) обеспечить логическую согласованность . Сложность попадания во многом связана с использованием крайне плохого инструмента (с точки зрения правильности).

Именно поэтому две худшие практики - это глобальные переменные и переходы. Эти вещи мешают помещать пре / пост / инвариантные условия вокруг чего-либо. Это также, почему типы так эффективны. По мере того, как типы становятся сильнее (в конечном счете, используя зависимые типы, чтобы принять во внимание фактическое значение), они становятся сами по себе конструктивными доказательствами правильности; несогласованные программы не скомпилируются.

Имейте в виду, что это не просто глупые ошибки. Речь идет также о защите базы кода от умных проникновений. Будут случаи, когда вам придется отклонить отправку без убедительного сгенерированного машиной доказательства важных свойств, таких как «следует формально указанному протоколу».

Инструменты статического анализа, такие как Coverity, действительно могут обнаружить HeartBleed и подобные дефекты. Полное раскрытие: я основал Coverity.

Посмотрите мой пост в блоге о нашем исследовании HeartBleed и о том, как наш анализ был улучшен для его обнаружения:

http://security.coverity.com/blog/2014/Apr/on-detecting-heartbleed-with-static-analysis.html

Автоматическая / формальная проверка программного обеспечения полезна и может помочь в некоторых случаях, но, как отмечали другие, это не серебряная пуля. Можно отметить, что OpenSSL уязвим в том смысле, что его открытый исходный код и в то же время широко используется в промышленности и в отрасли, широко используется и не требует тщательной проверки перед выпуском (возникает вопрос, есть ли в проекте даже платные разработчики). дефект был обнаружен в основном после проверки кода, а код был, по-видимому, проверен перед выпуском (обратите внимание, что, вероятно, нет способа отследить, кто проводил внутреннюю проверку кода). «обучающий момент» с сердечным кровотечением (среди многих других) - это, в основном, лучший обзор кода, в идеале перед выпуском особенно чувствительного кода, возможно, лучше отслеживаемого. возможно, OpenSSL теперь подвергнется более тщательной проверке.

больше bkg от СМИ, детализирующего его происхождение:

• Heartbleed был несчастным случаем: разработчик признался в том, что он вызвал ошибку кодирования, и признает, что ее эффект «явно серьезный». «Немецкий разработчик доктор Робин Сеггельманн признался, что написал код. Затем он был проверен другими участниками и добавлен в программное обеспечение OpenSSL»

• Как Codenomicon нашел ошибку с кровоточащей кровью, которая теперь мучает Интернет «Руководитель охранной фирмы объясняет, как был обнаружен недостаток, насколько велик риск и что люди могут с этим поделать».

• 3 больших урока, которые можно извлечь из Heartbleed: «Разрушительная уязвимость OpenSSL доказывает важность оркестровки центра обработки данных, мудрость использования старых версий и необходимость возвращаться к проекту OpenSSL»