Как сварщик из Питера за 4 месяца написал ОС с математическими доказательствами (и чуть не убил ноутбук)
Привет, Пикабу. Я давно вас читаю, а сейчас решил написать. Мне 38 лет, я работаю сварщиком в Санкт-Петербурге. Профильного IT-образования у меня нет. В июне этого года я купил ноутбук, поставил Linux и начал разбираться, как всё устроено внутри.
Первый месяц я вообще не писал код. Только учился. Два-три часа каждый вечер после работы, по плану, который сам себе составил. Терминал, сети, маска подсети, TCP-рукопожатие, HTTP, SSH. Читал статьи, смотрел YouTube, листал TikTok. Брал отовсюду, где было понятно. Жена сначала думала, что я просто залипаю в телефоне, но потом привыкла.
Про курсы и вуз думал. Посмотрел, что там дают, и понял, что не подходит. Не потому что плохо. А потому что информация устаревает быстрее, чем её успеваешь выучить. Пока учишь один фреймворк, выходит другой. Пока сдаёшь диплом, технология уже не та. Мне нужно было другое. Разобраться в основах и дальше идти самому, беря то, что нужно сейчас.
Где-то в процессе появилась мысль, что можно что-то создать. Приложение - не то. Игра - не то. Операционная система - почему бы и да. К концу июля у меня было около 160 модулей. И я понял, что не знаю, как их связать вместе. Структура плоская, переделать на ходу почти невозможно. Тогда я начал работать с ИИ-агентом.
Относился к нему двояко. С одной стороны, как к наставнику. Перед важными шагами я не приказывал, а советовался. На что повлияет изменение, какие есть альтернативы, что сломается, если пойти этим путём. У агента есть режим рассуждений, и я видел ход его мыслей. Иногда понимал, что он пошёл не туда, тормозил, направлял. А иногда видел подход, до которого сам бы не додумался. Так учиться оказалось быстрее, чем просто читать документацию.
С другой стороны, без слепой веры на слово. Если что-то выглядело сомнительно, я перепроверял. Сверял с документацией, с исходниками. Иногда агент ошибался, и это было нормально. Ошибки он не скрывал, а признавал. Это тоже часть работы. Не верить, а проверять.
Пик пришёлся на 8-18 августа. 8950 запросов, почти 3 миллиарда токенов, 37 долларов. Тогда же начались первые тесты на железе. И первая страница, открытая со смартфона 15 августа. Система ожила. Стало страшновато. До этого момента я считал это чуть более чем баловством.
Вот так выглядела страница, которую отдала моя ОС на обычный телефон по Wi-Fi. Дизайн, конечно, на уровне 90-х, но работает же!
Проект называется Schild TCB. Если совсем просто, это система, в которой ядро (самая главная и важная часть) написано так, чтобы его можно было проверить математически. То есть не просто прогнать тесты, а доказать, что оно работает правильно при любых входных данных.
Сначала я думал, что хватит одного образа. Но потом понял, что их нужно два. Первый написан с нуля полностью, там мой загрузчик, мои драйверы, мой сетевой стек. Он отвечает на вопрос, а работает ли это вообще. Второй образ стоит на микроядре seL4. Это ядро писал не я, его уже проверили до меня. А мой вклад - это то, что поверх. Задача на языке Ada и изолированные процессы. Этот образ отвечает на вопрос, а доказано ли это.
Почему я выбрал Ada. Честно скажу, не помню откуда я про него узнал. Наверное, в детстве что-то слышал. А ещё в Ada есть подмножество SPARK, где к коду можно добавлять контракты. И специальная программа-доказатель проверяет, что код ведёт себя ровно так, как записано. Звучит скучно, но на деле это как сварка. Только вместо шва — математическое доказательство, а вместо электрода — gnatprove.
И это не просто красивые слова. Был у меня один случай. Я задал права на страницы памяти как только для чтения. А в раскладке микроядра биты прав лежат иначе. В итоге моя страница только для чтения на самом деле стала только для записи, а такие страницы процессор не поддерживает, и ядро молча закрывало к ним доступ вообще. Тесты этого не ловили, потому что код просто не читал эти страницы. А вот доказатель поймал. Когда я начал проверять контракты, он показал, что математика не сходится с реальностью. Я пошёл разбираться, нашёл причину и исправил в одну строчку. Для меня это был главный результат всей работы. Тесты не нашли, а математика нашла. Вот это поворот, да?
Тот самый момент, когда доказатель говорит, что все сходится. Ноль ошибок. Для меня это выглядело как магия
Ещё была эпопея с изоляцией. Драйвер сети внутри ядра - это ошибка, которая роняет всю систему. Я вынес драйвер в отдельный процесс. Теперь, если он падает, падает только он, а ядро живёт дальше. Как в жизни: если у тебя сломалась розетка, это не значит, что нужно сносить весь дом.
Самое сложное в работе было даже не писать код. Самое сложное было отлаживать это на ноутбуке без COM-порта и UART. Второго компьютера для логов у меня нет. Поэтому я загружался с флешки, смотрел на экран, а потом грузился в Linux и описывал симптомы. Когда логи перестали писаться даже в файл, в ход пошли светодиоды клавиатуры. Num Lock и Caps Lock работали как индикация этапов загрузки. Горит Caps - код дошёл до такого-то места. Не горит - упал раньше. Жена спрашивала, чего это я так внимательно смотрю на клавиатуру. А я просто ждал, пока лампочка скажет мне, что система не упала.
Сейчас у меня работают два образа. Сеть и хранилище изолированы. TCP работает на реальном ноутбуке, страница открывается со смартфона. 108 модулей ядра доказаны на 4 уровне строгости SPARK. И я не считаю, что я такой умный. Просто всё, что не удавалось доказать, я либо переписывал, либо выносил из доказанного множества и честно помечал как таковое.
Где я застрял. Честно, потому что отчёт из одних побед никому не нужен. Главная проблема - это IOMMU, устройство для защиты памяти от прямого доступа извне. Без него скомпрометированная сетевая карта теоретически может писать в любую память, включая память ядра. Я собрал ядро с поддержкой IOMMU, но там всплыл баг в самом ядре seL4, который я не могу починить, потому что это чужой код. Так что сейчас это в подвешенном состоянии. Как говорится, хочешь сделать хорошо — сделай сам. А тут не могу. Печалька.
За всеми этими цифрами стоят три месяца по вечерам и выходным, ноутбук, флешка и любопытство. Если кто-то прочитал это и решил, что тоже хочет разобраться в чём-то сложном, значит, я написал не зря.
Ссылка на репозиторий: https://github.com/Nik0laic4/SchildTCB
А если кому-то интересны технические детали, вот моя статья на Хабре: https://habr.com/ru/articles/1095314/
Отвечу на вопросы, если они будут. Только не спрашивайте, как я спаял материнскую плату. Я её не паял. Я сварщик, а не волшебник.