Зачем?

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

Зачем ещё один язык?

Rust, C и Zig проектировались в то время, когда дороже всего обходилось написание кода, и свой бюджет сложности они тратят на того, кто пишет. Сейчас всё иначе. Первый черновик модель выдаёт за секунды, а прочитать его, проверить и решить, можно ли ему доверять, по-прежнему стоит столько же, сколько всегда. kola тратит бюджет на этого второго человека: рецензента, аудитора, того, кто будет сопровождать код через год.

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

• Безопасная работа с памятью без GC и без borrow checker. Память живёт в регионах, а ссылка, в тип которой входит регион, не может его пережить. Подробнее — в главе Память: регионы и ссылки.

• Утечка — ошибка компиляции. Файл, сокет или транзакция — это ресурс, и ресурс обязан быть израсходован на каждом пути выполнения функции. См. Ресурсы и линейность.

• Доступ к миру виден в сигнатуре. Эффекты говорят, что функция делает, а капабилити — с чем. Функция, которой не передали сетевую капабилити, не может открыть сокет. Это свойство системы типов, а не договорённость в команде. См. Эффекты и капабилити.

• Контракты нельзя отключить. Контракт (req, ens) либо доказывается при компиляции и тогда ничего не стоит, либо проверяется во время выполнения. Релизного режима, который их выбрасывает, не существует. См. Контракты, трапы и тесты.

• Любой упавший тест воспроизводится по одному числу. Время, случайность и планирование потоков проходят через капабилити, и тестовый прогон подменяет их детерминированными симуляциями. Красный тест печатает своё зерно (seed), и по нему прогон повторяется в точности.

Почему не линтер для Rust? Потому что всё перечисленное — правила системы типов, которые действуют на каждой границе вызова, в том числе внутри библиотек, которые вы никогда не открывали. Линтер можно не запустить, договорённость можно нарушить, а сигнатуру kola обойти нельзя. И хотя язык проектировался с оглядкой на сгенерированный код, он небольшой, синтаксис у него близок к Rust, и писать на нём руками вполне приятно.

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

Каких ошибок в языке не бывает

У правила «никаких полномочий из воздуха» есть одно намеренное исключение, и встретится оно уже в первой программе: эффекту log капабилити не нужна. Любая функция может что-то сказать. Дыры здесь нет: приёмник журнала один раз выбирает тот, кто запускает процесс (kola --log, KOLA_LOG), и он работает только на запись. Программа не может ни выбрать, куда писать, ни прочитать написанное обратно, так что через журнал нельзя ни повлиять на ход выполнения, ни протащить полномочия. Вывод программы, то есть байты, которые будет разбирать другая программа, — это другой канал, и для него капабилити нужна: sys.stdout.write(&bytes).

Как это выглядит

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

enum Verdict { Clean, Suspicious }

pub fn scan[r](payload: &r [u8]) -> Verdict !{} {
    let mut zeros = 0;
    for i in 0..payload.len {
        if payload[i] == 0 { zeros = zeros + 1; }
    }
    if zeros * 4 > payload.len { Verdict::Suspicious } else { Verdict::Clean }
}

На главные вопросы рецензента сигнатура уже ответила. scan не получает ни одной капабилити и объявлена чистой. Даже если её тело перепишет злоумышленник или модель сгенерирует его с ошибкой, функция всё равно не сможет никуда отправить данные, выделить память или зависнуть. Проверять остаётся только саму логику.

А вот тот же код целиком, как программа. main получает все полномочия процесса и решает, сколько из них достанется каждой вызываемой функции. В этой программе не достаётся ничего ни одной из них:

use std::log;

enum Verdict { Clean, Suspicious }

pub fn scan[r](payload: &r [u8]) -> Verdict !{} {
    let mut zeros = 0;
    for i in 0..payload.len {
        if payload[i] == 0 { zeros = zeros + 1; }
    }
    if zeros * 4 > payload.len { Verdict::Suspicious } else { Verdict::Clean }
}

// Журнал — это эффект, а не капабилити: приёмник только на запись,
// и выбирает его тот, кто запустил процесс.
fn report(v: Verdict) !{log} {
    match v {
        Verdict::Clean => log::info("payload: clean"),
        Verdict::Suspicious => log::info("payload: suspicious"),
    }
}

fn main(sys: Sys) -> u8 !{io, block, alloc(heap), log} {
    region r {
        let good = alloc in r [1u8, 2u8, 3u8, 4u8];
        let bad  = alloc in r [0u8, 0u8, 7u8, 0u8];
        report(scan(good));
        report(scan(bad));
    }
    0
}

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

use std::log;

// Получает часы и больше ничего. Открыть сокет, прочитать файл
// или выделить память она не может: ей просто нечем.
fn stamp(clock: &Clock) -> u64 !{io} {
    clock.now()
}

fn main(sys: Sys) -> u8 !{io, log} {
    log::info(f"t = {stamp(&sys.clock)}");
    0
}

Так же распределяется и память:

fn main(mut sys: Sys) -> u8 !{io, block, alloc(heap)} {
    let small: Mem = sys.mem.split(1048576);  // отрезаем 1 МиБ от корневого бюджета
    region r from small {                     // арена этого региона берёт память из него
        let v: &r mut Vec[u64] = alloc in r mut Vec::new();
        v.push(1);
    }                                         // регион закрыт, память вернулась
    sys.mem.absorb(small);                    // возвращаем бюджет
    0
}

Здесь важны две детали. split и absorb изменяют корневой набор, поэтому main принимает mut sys; если забыть mut, компилятор об этом скажет. И Mem — одна из немногих капабилити, которые нельзя просто выбросить. Выброшенный маркер полномочия вроде Clock ничего не теряет, и среда выполнения его подбирает. Бюджет же — это количество, и его потеря была бы настоящей утечкой, поэтому линейность заставляет вернуть его на каждом пути.

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

Откуда взялась kola

Название расшифровывается как kore language. kola разрабатывает Kore Ltd для собственных системных проектов: гипервизора, файловой системы, базы данных и сервисов вокруг них. Нам нужен был безопасный, быстрый, проверяемый и небольшой язык, программы на котором имеют ясные и явно очерченные границы. Мы рады участию сообщества и просим только об одном: сохранять эту идею.