Безопасность: исчерпывающая защита против масштабируемых атак

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

Превратить поверхность в список

Более аккуратный код этот разрыв не закроет: рецензия не масштабируется так, как теперь масштабируется автоматический поиск уязвимостей. Главное решение kola в области безопасности — сделать значимую для безопасности поверхность программы конечной, перечислимой и машиночитаемой, чтобы защитник (человек или модель того же рода, что у атакующего) мог проверить её целиком, а не выборочно. Исчерпывающая защита побеждает масштабируемое нападение, только когда поверхность — это список, а не кодовая база. В kola она и есть список:

У небезопасной работы с памятью нет конструкции в исходном коде. Нет unsafe, нет FFI (foreign function interface — способа напрямую вызывать код на C), нет сырых указателей, нет extern и ассемблерных вставок. Вне проверок kola остаются только компилятор со средой выполнения и аппаратные ветки — символы на C или ассемблере, названные в предложении hw у функции стандартной библиотеки или пакета. Это множество перечислимо: kola audit выводит каждую ветку, kola test --native сверяет каждую с телом функции на kola, ветка ct fn дизассемблируется и отвергается, если в ней есть условный или косвенный переход, а --no-hw собирает программу без единой ветки.
Возможность дотянуться до мира — это строки бюджета в манифестах пакетов. Пакет объявляет, какие капабилити он может взять из корневого набора. kola audit завершается ошибкой, если код выходит за бюджет, а неизвестное имя капабилити — это ошибка, а не опечатка, которую молча пропустят. Пакет с [caps] allowed = [], которому ничего не передали, не может обратиться ни к сети, ни к файловой системе, ни к часам, и обеспечивает это система типов, а не политика.
Поведение — это ряды эффектов в публичных сигнатурах (Эффекты и капабилити). Сигнатуры модуля говорят, что он может делать; больше полномочиям или побочному эффекту спрятаться негде.
Доверие к входным данным — это пометка untrusted. Параметр, через который приходят байты из сети, файла, stdin или IPC, помечается untrusted, и ни один контракт не может от него зависеть. Почему — объясняет раздел ниже.
Компилятор знает каждое место, где во время выполнения может сработать трап. kola report checks показывает по функциям, что доказано при компиляции, а что ещё проверяется во время выполнения. kola report reachable обходит тот же список от точек входа программы через все модули и называет то, что обойти не удалось.
Происхождение случайности записано в типе. Значение, которое противник не должен угадать, имеет тип Entropy[[u8; N]] и при каждом вызове берётся у ОС. Конструктор, нужный для тестовых векторов, Entropy::of, kola audit отвергает на любом пути, который не начинается в test. kola report secrets находит константу времени компиляции, попадающую в позицию типа Secret, то есть учётные данные, вшитые в образ.

kola query attack-surface выдаёт всю поверхность единицы компиляции одним JSON-объектом, построенным из фактов самого компилятора, а не из текстового поиска. Туда входят все функции, которым передают капабилити (выданные капабилити, производные от них маркеры и линейные дескрипторы вроде &Conn или &Dir, прослеженные транзитивно через структуры, которые их содержат), все функции, которые принимают байты на вход, не имея полномочий, все значения-функции, пересекающие границу, все возвраты, выходящие за пределы региона, и все типы, несущие капабилити.

Такой список полезен, только если он полон, а утверждение о полноте, записанное прозой, никто не запускает. Поэтому это утверждение — тест: набор тестов компилятора синтезирует пробную функцию для каждого зарезервированного типа капабилити и дескриптора, запускает перечисление и проверяет, что каждая попала в нужный класс; отрицательные контрольные случаи не дают пройти тесту, если просто перечислить всё подряд. Новый тип капабилити либо попадает в поверхность, либо тест падает и называет его. Общий урок шире этого инструмента: там, где утверждение о безопасности важно, заставьте что-нибудь его исполнять.

Убрать сырьё

Классы ошибок, которые автоматические охотники собирают в C, на kola не выразить: use-after-free (обращение к памяти после её освобождения), выход за границы (чтение или запись за концом буфера), двойное освобождение (повторное освобождение той же памяти) и тихое переполнение целых. В kola нет неопределённого поведения — так в C называют операцию, результат которой язык не задаёт, а компилятор вправе считать, что она никогда не происходит (см. таблицу на странице Зачем kola?). Особенно это важно для сгенерированного кода. «Правдоподобно, но чуть-чуть неверно» — естественный способ ошибаться для статистического генератора, и в C такие ошибки становятся материалом для эксплойтов. В kola они становятся детерминированным трапом: ошибка, которая могла бы дать удалённое выполнение кода, превращается в громкую остановку.

Насколько громкую, определяет блок domain. Трап внутри него сносит регион этого блока и запускает его ветку recover вместо того, чтобы убить процесс, так что враждебный запрос погибает, а сервер продолжает работать. Восстановление превращает «умер процесс» в «умер запрос, и кому-то предстоит это исправить». Трап всё равно остаётся ошибкой, и kola audit учитывает каждый домен, чтобы пути отказа нельзя было тихо замазать.

Повышать полномочия тоже не за счёт чего: полномочий «из воздуха» нет. Парсер с типом fn scan[r](p: &r [u8]) -> Verdict !{} не может никуда отправить то, что разбирает, даже если его тело написано со злым умыслом: у него нет ни одной капабилити, а ряд эффектов доказывает, что он чистый. Отсюда и рабочая дисциплина для недоверенного ввода. Код, обрабатывающий байты, прочитанные через капабилити, остаётся чистой обработкой данных без эффектов вплоть до того места, где ввод проверен. Так написан протокольный код стандартной библиотеки.

Контракт — это обещание вызывающему, а у байтов из сети вызывающего нет

Самая поучительная дыра из закрытых в kola нашлась в её собственной стандартной библиотеке, и это была не ошибка работы с памятью. У транспортной функции было обычное предусловие req packet.len >= 32, где packet — полезная нагрузка UDP прямо из сети. Специально составленный 20-байтный пакет вызывал трап, а в freestanding-сборке (работающей без операционной системы, как прошивка маршрутизатора) трап останавливает весь маршрутизатор. Получался удалённый отказ в обслуживании, доступный ещё до всякой аутентификации, с одного пакета. При этом каждая гарантия работала как задумано: контракты соблюдаются, а нарушенный контракт и должен останавливать программу.

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

pub fn parse(untrusted pkt: &[u8]) -> u16 !{}
    req pkt.len >= 4
{
    0
}

Компилятор отвечает error[card §8]: `req` depends on untrusted input `pkt` и предлагает проверять во время выполнения и возвращать Result или Option. Тогда проверка длины становится обычным кодом и заодно даёт пруверу нужный ему факт:

use std::encoding::bytes;

enum Frame { Ping, Data(u16) }

pub fn parse(untrusted pkt: &[u8]) -> Option[Frame] !{} {
    if pkt.len < 4 { return None; }
    let kind = bytes::rd16(pkt, 0);
    let len = bytes::rd16(pkt, 2);
    if kind == 1 { return Some(Frame::Ping); }
    if kind == 2 && widen[usize](len) + 4 == pkt.len { return Some(Frame::Data(len)); }
    None
}

test short_packet_is_refused_not_trapped {
    assert parse(&b"\x00\x01") == None;
    assert parse(&b"\x00\x01\x00\x00") == Some(Frame::Ping);
}

kola report checks для этого файла показывает оба предусловия rd16 доказанными в местах вызова. На глаз этот класс ошибок трудно заметить потому, что опасное условие обычно стоит рядом с законным в том же предложении: настоящее обязательство вызывающего и длина, которой управляет атакующий, в одной строке req. kola report tainted-reqs находит кандидатов в существующем коде. Отказ из-за untrusted в kola check касается только функции, на которой стоит пометка; контракт на три вызова глубже, где-нибудь в кодеке, виден kola report reachable, который обходит замыкание от точек входа.

Вместе с Secret[T] (данные, которые нельзя раскрыть) и ct fn (код, время работы которого не должно ничего раскрывать) untrusted замыкает ось доверия к данным, выраженную в типах и проверяемую компилятором.

Удержать то, что вы не контролируете

Зависимость получает только те капабилити, которые её API действительно передали, а бюджет в её манифесте соблюдает компилятор, причём по принципу «запрещено всё, что не разрешено»: нет раздела с бюджетом — не разрешено ничего. Аудит опирается на факты чекера об эффектах, а не на текстовый поиск.

Бюджет нужно читать точно. allowed говорит, что пакет может взять из корневого набора. Полномочия, которые пакет получает как обычный параметр, принадлежат вызывающему, поэтому аудит печатает их отдельно, в строке reaches:: линейные дескрипторы, выданные маркеры каталогов и окон и ссылки на функции, в ряде эффектов которых есть io или block. Бюджет — это то, что пакет может создать сам; строка reaches: — то, что ему доверили. Рецензенту нужно и то и другое. Sys в бюджете выдаёт только Sys, а не всё, что в нём содержится. На практике это значит, что обновление зависимости, которой вдруг понадобилась сеть, ломает сборку, пока манифест верхнего уровня этого не разрешит, а вся рецензия сводится к диффу в одну строку. До компиляции пакеты — это инертные данные; скриптов, выполняемых при установке, нет.

Получение кода — отдельный вопрос. kola pack push подписывает пакет, реестр хранит и отдаёт подпись, а kola pack fetch проверяет её и при первом использовании закрепляет ключ издателя за именем пакета: первый увиденный ключ запоминается, и следующий релиз, подписанный другим ключом, отвергается. Якорь доверия — издатель, реестр же лишь транспорт. Неподписанный пакет из реестра по https — безусловная ошибка; явный обход — --allow-unsigned. kola security check <packdir> сверяет каждую зависимость и то, во что она разрешилась, с опубликованными в реестре уведомлениями об уязвимостях. Всё о пакетах — на странице Пакеты.

Любой сбой воспроизводится

Весь недетерминизм (время, случайность, порядок ввода-вывода, планирование потоков) проходит через капабилити, поэтому трап, значимый для безопасности, бит в бит воспроизводится по зерну под kola test --sim --seed N. Успешная атака сводится к зерну и входным данным и становится регрессионным тестом.

Утверждения атакуют нарочно

Модель безопасности фальсифицируема, и местами её действительно опровергали, причём намеренно. В раундах состязательной проверки модели ставится задача сломать гарантии. Первый раунд нашёл нарушения безопасности памяти, существовавшие только в нативном бэкенде, когда интерпретатор корректно срабатывал трапом, а также пробелы в обработке капабилити и в аудите; один из следующих раундов, уже на исправленном коде, нашёл дыры в самом чекере. Каждую находку исправили вместе с регрессионным тестом, который без исправления падает. Структурный урок стал архитектурой: решение снять проверку теперь принимается ровно в одном месте, в верифицированном IR, и каждый бэкенд берёт его оттуда, так что два бэкенда не могут разойтись в том, какие проверки убраны (IR-0). Пройденный раунд покрывает только те атаки, которые были опробованы, поэтому раунды продолжаются.

Эту практику поддерживают два рабочих правила. Дефект не считается исправленным, пока нет теста, который падает при откате исправления. А проверка, которая пропускает сама себя или сообщает об успехе того, чего не запускала, считается хуже, чем отсутствие проверки: она забирает то внимание, которое заметило бы пробел.

От чего язык защитить не может

Неверные спецификации. Если контракт неверно моделирует протокол или железо, каждое построенное на нём доказательство уверенно ошибается. Смягчают это методами: независимыми эталонами, опубликованными тестовыми векторами, перекрёстным тестированием.
Дефекты на обеих сторонах сравнения. Сравнение двух исполнителей не найдёт общую для них ошибку, а симулированный тест не может подтвердить утверждение о настоящем сокете или настоящем железе.
Побочные каналы, кроме времени. Побочный канал выдаёт секрет не через вывод программы, а через что-то другое, например через время работы или потребляемую чипом мощность. Время для криптографии закрывает проверяемое компилятором подмножество с константным временем (Константное время). Утечки через спекулятивное выполнение процессора (работу, которую он делает наперёд, а потом отбрасывает) и через энергопотребление в эту модель не входят.
Враждебные издатели. Бюджеты удерживают враждебный пакет, но не делают так, чтобы его не было. Кто публикует пакеты — социальная проблема; закрепление ключа издателя делает её видимой, но не решает.
Продвижение. Все проверки касаются трапов. Цикл, который никогда не продвигается, проходит kola report checks и зависает во время выполнения, и атакующий, управляющий входом, может суметь это устроить.