Четверг, а значит время проектов от подписчиков! 🌝

Тем, кто пропустил, что такое четверговые проекты от подписчиков, можно прочитать тут - https://xn--r1a.website/tech_b0lt_Genona/4983

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

А для демонстрации сделано полноценное живое видео (происходит впервые в четверговой рубрике!), за что отдельное спасибо.

Слово автору @ejiek

---
git-plumber — read-only клиент для git'a, преследующий образовательные цели. Он показывает, как другие git клиенты меняют содержимое папки .git.

Это консольное приложение, как и сам git. Но с TUI в качестве основного интерфейса. Надеюсь, это поможет пользователям IDE и GitHub Desktop узнать, что гит родом из терминала перебороть его страх.

Лично мне приложение помогло понять:
- Насколько плохо хранить бинарные файлы в гите
- Почему гит отказывается добавлять в репу пустые папки
- Как спасти удалённый и не закомиченный файл
- Как именно гит хранит разницу между версиями файла

Оказывается, на уровне хранения git ничего не знает ни про строки, ни про текст. Иногда git хранит все версии целиком. А иногда сжимает, но не построчными diff'aми, а побайтовыми delta'ми. Мало того, дельты умеют всего две операции: скопировать и вставить. Этого достаточно! Например, чтобы описать удаление: «скопируй всё до, пропусти лишнее, скопируй всё после».

Приглашаю попробовать приложение самостоятельно. И поделиться обратной связью. Особенно если что-то сложно понять или нужны пояснения.

git-plumber ещё в ранней стадии разработки, но уже может быть полезен. Сейчас главная цель — проработать подачу материала и UX. И вооружить git-plumber'ом преподавателей, студентов и энтузиастов уже в этом учебном году.

⭐️ Прошу поддержать проект звездой на GitHub'e ⭐️
---

Тут темпоральную логику затащили в рантайм Linux (6.17.0-rc2) для верификации происходящего в ядре.

Extending run-time verification for the kernel
https://lwn.net/Articles/1030685/

[PATCH v11 00/21] RV: Linear temporal logic monitors for RT application
https://lwn.net/ml/all/cover.1751634289.git.namcao@linutronix.de/

Вообще, вокруг ядра есть куча всего и для статического анализа, и динамического, и тестирования, что бы оно становилось стабильней и лучше

Development tools for the kernel
https://docs.kernel.org/dev-tools/index.html

В посте идёт рассказ проблематики и причин появления утилиты rvgen. Это инструмент, который из DOT-описания Graphviz генерирует код на C, который, в свою очередь, представляет собой "скелет" для Runtime Verification Monitor'а (RVM). Но так же можно с помощью него получить логический монитор

$ rvgen monitor -c ltl -s pagefault.ltl -t per_task

В результате будет получено два файла:

- pagefault.h - файл с описанием автомата Бюхи
- pagefault.c - скелет RVM

Подробнее тут
https://docs.kernel.org/trace/rv/monitor_synthesis.html#rvgen

Собственно, в этом и состоит патч.

Но тут я хочу теперь больше сказать про то что такое LTL

LTL (Linear Temporal Logic) значит/переводится как логика линейного времени. Как понятно из названия это относительно простая сущность, которая позволяет описать и формализовать последовательность событий без ветвлений.

Давайте рассмотрим простейший пример - светофор.

Обычный режим его работы: Красный -> Жёлтый -> Зелёный

Описать это можно следующей формулой:
[](Красный -> (<> Зелёный && (!Зелёный U Жёлтый)))
,где
[] - всегда в будущем
<> - когда-нибудь
&& - логическое И
U - до тех пор (пока)

Соответственно, эту формулу можно "перевести" так: Всегда после Красного когда-нибудь в будущем будет Зелёный, после того как некоторое время был Жёлтый

Сварщик я не настоящий и подобные штуки это скорей моё хобби. Я когда-то игрался с LTL/CTL применительно к ping'у, было сложна 🌝

Вот, для понимания, пример из статьи применительно к ядру
https://lwn.net/Articles/1030831/

Если вы хотите узнать, что такое автомат Бюхи, модель Крипке и т.д., то в интернете много материала на эту тему. Я же оставлю на русскоязычные источники (если знаете хорошие, то кидайте в личку или комменты)

Проверка моделей. Видео и слайды лекций
http://wasp.iis.nsk.su/page5.html

Математические методы верификации схем и программ
https://mk.cs.msu.ru/index.php/%D0%9C%D0%B0%D1%82%D0%B5%D0%BC%D0%B0%D1%82%D0%B8%D1%87%D0%B5%D1%81%D0%BA%D0%B8%D0%B5_%D0%BC%D0%B5%D1%82%D0%BE%D0%B4%D1%8B_%D0%B2%D0%B5%D1%80%D0%B8%D1%84%D0%B8%D0%BA%D0%B0%D1%86%D0%B8%D0%B8_%D1%81%D1%85%D0%B5%D0%BC_%D0%B8_%D0%BF%D1%80%D0%BE%D0%B3%D1%80%D0%B0%D0%BC%D0%BC

Софт с которым можно поиграться

- https://uppaal.org/
Презентация с UPPAAL https://asvk.cs.msu.ru/~dimawolf/SoftwareReliability/Lection05.pdf

- https://spinroot.com/
Две лекции со SPIN https://www.lektorium.tv/course/22862

Об IOCCC (International Obfuscated C Code Contest) я писал в январе
https://xn--r1a.website/tech_b0lt_Genona/4922

И вот недавно подвели итоги

Winning Entries of 2024 - The 28th IOCCC
https://www.ioccc.org/2024/index.html#2024

Объявлены победители 28 конкурса по написанию запутанного кода на языке Си
https://www.opennet.ru/opennews/art.shtml?num=63668

Участвующие в конкурсе работы, с одной стороны, должны препятствовать анализу кода и пониманию сути решаемой задачи, но, с другой стороны, код должен быть интересен и чем-то примечателен (работы могут быть необычно оформлены или выделять неожиданные стороны языка Си). Размер исходного кода программы не должен превышать 4096 байт, а программа должна собираться и выполнять осмысленное действие

Больше всего меня впечатлили три работы

1. Виртуальная машина, способная запускать Doom 1/2 на современных ПК от Ильи Курдюкова из "Базальт СПО"
https://www.ioccc.org/2024/kurdyukov3/index.html
https://github.com/ioccc-src/winner/blob/master/2024/kurdyukov3/prog.c

Разбор его работы от жюри
2024/kurdyukov3 - Prize in virtual quietus
https://www.youtube.com/watch?v=iaXMwqR93iE

2. Эмулятор CPU Intel 4004 от Николаса Карлини (Nicholas Carlini) из "Anthropic"
https://www.ioccc.org/2024/carlini/index.html
https://github.com/ioccc-src/winner/blob/master/2024/carlini/prog.c

Разбор его работы от жюри
2024/carlini - Prize in perfect timing
https://www.youtube.com/watch?v=r6wUZUaaJBY

Пост с разбором от самого автора
Gate-level emulation of an Intel 4004 in 4004 bytes of C
https://nicholas.carlini.com/writing/2025/ioccc-intel-4004-in-4004-bytes-c.html

3. Эмулятор CPU OpenRISC, способный запустить Linux от Себастиана Маке (Sebastian Macke) из "QAware"
https://www.ioccc.org/2024/macke/index.html
https://github.com/ioccc-src/winner/blob/master/2024/macke/prog.c

Разбор его работы от жюри
2024/macke - Prize in imitative rebooting
https://www.youtube.com/watch?v=jeQFI_8kGA4

Репа со всеми победителями за все года
https://github.com/ioccc-src/winner

Полная трансляция разбора работ
IOCCC28 Winning Entries | IOCCC Awards Presentation and Source Code Reveal
https://www.youtube.com/watch?v=UDzGwTalVAc

Есть такой стартап Antithesis, который сделан выходцами из Apple, которые пилили FoundationDB (https://github.com/apple/foundationdb/) и занимается он созданием платформы для тестирования ПО - https://antithesis.com/product/what_is_antithesis/

Автоматическое тестирование ускорило разработку в 50 раз. Сказка от создателей FoundationDB
https://habr.com/ru/companies/ruvds/articles/800009/

И у них есть серия постов про их ИИ, который создан с одной целью - проходить игры с NES.

> The Antithesis autonomous testing platform can beat dozens of games, including some very complex ones that as far as we know have never before been completed by an autonomous system

Antithesis announces Artificial General 8-bit Intelligence (AG8I)
https://antithesis.com/blog/ag8bi/

How Antithesis finds bugs (with help from the Super Mario Bros.)
https://antithesis.com/blog/sdtalk/

Solving Zelda with the Antithesis SDK
https://antithesis.com/blog/zelda/

Crushing Castlevania with Antithesis
https://antithesis.com/blog/castlevania/

Depth is all you need: how Antithesis crushes Gradius
https://antithesis.com/blog/2025/gradius/

Optimizing our way through Metroid
https://antithesis.com/blog/2025/metroid/

Планируются ещё Contra, Kirby’s Adventure, Arkanoid, Tetris, Ice Climber

В посте про Metroid они поясняют зачем они это делают

> The honest truth, the underlying reality beneath the hype, is that this is actually how we figured this stuff out. None of us were fuzzing or PBT experts coming into this business, and if we were that wouldn’t have helped anyway, because our ambitions quickly went way beyond the state of the art in those fields. So we started asking questions like: “why can’t you beat The Legend of Zelda with a fuzzer,” and pixel by grueling pixel we learned enough to build the Antithesis platform.

В целом это правда похоже на специфичный fuzzing

> But our system doesn’t have to act like a linear agent. The rest of the platform around it is a mechanism for giving an arbitrary program save slots that can be written to and reloaded at arbitrary points. This translates a one-shot problem into a problem on which incremental progress is possible. We’re not sure if there’s a term for such an agent, but internally, we refer to this as “tree fuzzing,” and it enables our system to effectively test complex programs with a comparatively minimal understanding of their internal workings.

https://antithesis.com/blog/2025/gradius/#seeing-like-a-fuzzer

Запускают всё в специальном окружении, которое позволяет ловить и воспроизводить ошибки

So you think you want to write a deterministic hypervisor?
https://antithesis.com/blog/deterministic_hypervisor/

Я прикрепил к посту их трейлер и пару докладов, которые позволяют погрузиться в тему.

В общем с удовольствием прочитал всю серию и жду новые посты, тем кто интересуется рекомендую.

Русский след в истории логотипа PostgreSQL
https://habr.com/ru/companies/postgrespro/articles/905612/

Готовый эскиз сайта с логотипом Дмитрий выложил на своём персональном сайте devnull.wplus.net (что подчеркивало неформальность) и отправил ссылку в нашу рассылку. И это не просто воспоминания: сохранилось его письмо в список рассылки pgsql-hackers от 12 апреля 1999 года. В нем, отвечая в рамках дискуссии "RE: [HACKERS] PostgreSQL Webpage", Дмитрий писал: "I was commited to show how postgres webpage should looks by my opinion. See http://devnull.wplus.net/pub/postgres/" («Я решил показать, как, по моему мнению, должна выглядеть веб-страница postgres. Смотрите...»). Так что факт задокументирован: именно тогда, в апреле 1999-го, эскиз был представлен сообществу.
. . .
Юридически авторство и права на использование «русского слоника» оставались в «серой зоне». Я решил исправить эту ситуацию и обратился к Дмитрию Самерсову с просьбой формально передать права на оригинальный дизайн сообществу. Поскольку разработка логотипа была частной инициативой Дмитрия и его студии, а не какой-то организации, процедура передачи прав была простой.

Дмитрий, не имевший никаких претензий на логотип, согласился. С присущим ему юмором он вспоминает: «Если просят сделать какую-то странную фигню, то эту странную фигню надо сделать со всей тщательностью и вниманием». В марте 2025 года Дмитрий Самерсов официально передал права на дизайн «слоника» под лицензией Creative Commons всему сообществу PostgreSQL.

Сегодня на официальной вики PostgreSQL закреплено: «The PostgreSQL elephant logo “Slonik” is a copyrighted design...» История приобрела логическое завершение.

Что чувствует Дмитрий Самерсов, стоя у истоков символа, известного миллионам? «С одной стороны, приятно, что есть что-то, что останется после меня, кроме детей. С другой стороны, немножко забавно, что из всего сделанного в этой жизни наиболее ярким ощущением остался такой случайный логотип slonik.gif».

Пост об этом же от Олега Бартунова из 2016 года
О логотипе PostgreSQL
https://obartunov.livejournal.com/186860.html

Небольшой доклад Олега (прикрепил тоже к посту)
История логотипа Slonik
https://www.youtube.com/watch?v=nqeyAs0YOHQ

Слайды положу в комментарии

Я с Дмитрием знаком лично. Он замечательный человек и собеседник.

Персональный сайт - https://www.samersoff.net/mz/
Канал - @softrainbbs

Ребяты из Vulners запилили плагин для Chrome, который подсвечивает сами CVE на странице, показывает дополнительную информацию в попапе и по клику кидает на страницу с описанием уязвимости на https://vulners.com/

Оригинальное сообщение тут
https://xn--r1a.website/VulnersChat/15840

Архив есть в оригинальном сообщении + положу его в комментарии

Установка

1. Распакуйте ZIP
2. Откройте chrome://extensions/ → включите Developer mode
3. Нажмите Load unpacked и выберите папку с расширением

Я работаю с БДУ ФСТЭК в отдельном браузере и удобно, когда есть подсветка на странице по CVE с дополнительной информацией 🌝

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