Cloudflare выложили разбор вчерашнего инцидента

Cloudflare outage on December 5, 2025
https://blog.cloudflare.com/5-december-2025-outage/

Попробую кратко описать чо там у них случилось, если где-то неправильно понял, то поправьте в комментариях

Как и писал CTO (https://news.1rj.ru/str/tech_b0lt_Genona/5926), они катили изменения для того, что бы закрыть свежую и нашумевшую уязвимость React'а (https://news.1rj.ru/str/tech_b0lt_Genona/5918, https://news.1rj.ru/str/tech_b0lt_Genona/5923)

Для этого они провели два действия:

- Они обнаружили что балалайка, котрая тестирует их WAF, не поддерживает нужный размер буфера тела HTTP-запроса, поэтому они её отключили (нужен был 1 MB, а умела только 128 KB)

- Выкатили практически моментально на все сервера изменения. Если я понял правильно, то они так настроили/сделали систему конфигурации после прошлого отвала - https://news.1rj.ru/str/tech_b0lt_Genona/5885

Как и в прошлый раз, сейчас тоже упоминаются две реализации их прокси - FL1 (старая, я не помню на чём, но там есть Lua) и FL2 (новая на Rust)

FL1 стало плохо после отключения балалайки, которая тестировала WAF и его правила, и начала "пятисотить". Происходило это из-за того, что поломался кусок, который отвечал за правила (Lua часть)

[lua] Failed to run module rulesets callback late_routing: /usr/local/nginx-fl/lua/modules/init.lua:314: attempt to index field 'execute' (a nil value)

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

> Customers that have their web assets served by our older FL1 proxy AND had the Cloudflare Managed Ruleset deployed were impacted

> Customers that did not have the configuration above applied were not impacted. Customer traffic served by our China network was also not impacted.

Когда CF увидели, что всё посыпалось, то вообще должна была отработать система "отката". Но что-то пошло не так 🌝

Правила, когда отрабатывают, то выполняются определённые действия (в том числе и к трафику)

> Typical actions are “block”, “log”, or “skip”. Another type of action is “execute”, which is used to trigger evaluation of another ruleset.

Но как выяснилось они никогда не откатывали аварийно правила с типом execute и при откате сломавшего всё нового правила возникла ошибка в логике

if rule_result.action == "execute" then
  rule_result.execute.results = ruleset_results[tonumber(rule_result.execute.results_index)]
end

> This code expects that, if the ruleset has action=”execute”, the “rule_result.execute” object will exist. However, because the rule had been skipped, the rule_result.execute object did not exist, and Lua returned an error due to attempting to look up a value in a nil value.

В FL2 проблемы не существовало такой, потому что, цитирую

> This is a straightforward error in the code, which had existed undetected for many years. This type of code error is prevented by languages with strong type systems.

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

Короче, растпобеда случилась 🗿

#prog #c #article #abnormalprogramming

Серия из трёх (на текущий момент) статей о странностях C

Weekend projects: getting silly with C
Getting silly with C, part (void*)2
Getting silly with C, part ~(~1<<1)

Наверное, мои самый любимые примеры кода из статей — это многострочный комментарий:

#include <stdio.h>

int main() {
  puts("Hello world");
  asm("/*");
  /* Nested comment */
  for (int i = 0; i < 10; i++) puts("I LIKE PANCAKES!");
  asm("*/");
  puts("Goodbye world");
}

и абьюз type punning-а на сигнатуре main для доставания "Главного ответа о вселенной, смысле жизни и всего такого" из воздуха:

#include <stdio.h>

int main(int i) {

  do do do do "baby shark!";

  while (++i % 2);
  while (i == 2);
  while (i % 3); 
  while (i % 7);

  printf("The answer is %d.\n", i);

}

Для интересующихся, как это работает:

main, вообще говоря, в C либо не принимает аргументов, либо принимает два: argc и argv. GCC даже указывает на это при компиляции с -Wall. В данной программе main имеет некорректную сигнатуру, но в силу того, как распределяются регистры для целевого ABI, первый аргумент для int main(int, char**) и int main(int) попадают в один и тот же регистр. Иными словами, при запуске этой программы в i попадает значение argc, и так как на godbolt по умолчанию программе никаких аргументов не прокидывается, i имеет значение 1 (первым аргументом OS передаёт название программы — так, например, работает busybox, который в одном бинарнике скрывает несколько программ и по этому аргументу выбирает, какую звать).

Форматирование кода скрывает тот факт, что в программе содержатся четыре вложенных друг в друга do-while цикла (это можно проявить, если отформатировать код). Для того, чтобы циклы завершились, нужно, чтобы после выхода из циклов i было:

* кратно 2
* не равно 2
* кратно 3
* кратно 7

i начинает с 1 (точнее, 2 из-за преинкремента на первой итерации), наименьшим общим кратным 2, 3 и 7 является число 42, поэтому именно это значение принимает i и оно в итоге выходит на печать.

Так как 2 не кратно ни 3, ни 7, условие "не равно 2" избыточно. И действительно, если убрать один из do и второй while, то результат будет тот же.

Тот факт, что в i попадает именно значение argc, можно подтвердить, если добавить на gobolt окно с исполнением и докинуть аргументов командной строки для программы. Если туда вписать 41 значение, то argc будет равно 42, на первой итерации i станет равным 43 и потому программа выдаст следующее число, кратное 2, 3 и 7: The answer is 84.

#prog #meme

Source

Reject Maya/3ds Max

Ну и срань

Хабр в плюсе, Яндекс в плюсе, а вот читатели получают здоровенный неотключаемый баннер к каждому сниппету кода, который ещё и требует логина в аккаунт Яндекса и (по отзывам) работает крайне паршиво.

Если используете uBlock, то в комментариях подсказали фильтр для того, чтобы убрать:

habr.com##.code-explainer

#prog #suckassstory

🎆 🎭 TROBBIO! 🎭 🎇

РИА Новости накануне зимней сессии предупреждает: ДУМАТЬ ВРЕДНО !

Длительная умственная нагрузка может привести к развитию гипертонии, аритмии и ишемии сердца.

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

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

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

https://ria.ru/20251209/vrach-2060710660.html

#prog #article

Afternoon project: JPEG DCT text lossifizer

Чел сделал штуку (веб-приложение), которая применяет к тексту процесс, аналогичный сжатию с потерями в JPEG: разбирает текст как семпл на частоты, огрубляет их и собирает обратно.

Пара моментов:

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

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

Dear colleagues,

At AWS re:Invent 2025 in Las Vegas, we announced the AWS Nitro Isolation Engine [1, 2, 3], a formally verified enhancement to the AWS Nitro System that enforces isolation between virtual machines hosted on AWS's new Graviton5-based EC2 instances.

Nitro Isolation Engine represents a significant deployment of mechanized proof in production infrastructure, and we therefore wanted to bring this to the attention of the formal methods and programming languages communities. This work builds directly on decades of advances in interactive theorem proving, program verification, and programming languages theory, alongside landmark projects—such as, seL4 [4], CertiKOS [5], SeKVM [6], and many others—that were inspirations for this work.

What is Nitro Isolation Engine?
Nitro Isolation Engine is a small, trusted computing base written in Rust that sits beneath the AWS Nitro Hypervisor, providing a security isolation boundary between the hypervisor and guest virtual machines, and between co-tenanted guest virtual machines. The Nitro Isolation Engine controls the critical hardware features required for isolating customer workloads, primarily control of Stage Two translation tables.

The verification effort
Nitro Isolation Engine was designed with verification in mind from the first line of code. Nitro Isolation Engine is subject to AWS’s existing rigorous engineering practices, including the deployment of property-based-testing and lightweight formal methods, for example the Kani bounded model checker for Rust [7].

Building atop this foundation, we have specified and verified the correctness of Nitro Isolation Engine in Isabelle/HOL [8]. Our model and proofs consist of around 260,000 lines of machine-checked models and proofs. Specifically, we have proved:

Functional correctness: Nitro Isolation Engine behaves as specified for all operations: virtual machine creation, memory mapping, instruction and data abort handling, and so on. As corollaries of our total verification style, we have also proven memory-safety, termination, and absence of runtime errors, providing our modelling assumptions are accurate.
Confidentiality: We prove a noninterference-style property demonstrating the confidentiality of guest virtual machine states, formalized as indistinguishability preservation up-to permitted flows of declassified information out of a guest.
Integrity: The integrity of guest virtual machine state is formalized as a safety property, showing that the private state of one virtual machine is unaffected by operations modifying another distinct virtual machine.
In addition, we have applied Iris [9] and Verus [10] to prove the correctness of the Nitro Isolation Engine’s concurrency primitives, including ticket locks, mutexes, and rendezvous barriers.

For functional verification, we defined μRust, a restricted subset of Rust expressive enough to write Nitro Isolation Engine but amenable to formal reasoning and embedded its semantics into Isabelle/HOL. Specifications are written in separation logic, and proofs proceed via weakest precondition calculus with custom automation. We have made our verification infrastructure open source as the AutoCorrode library [11] for Isabelle/HOL, which may be of independent interest.

Regards,
Automated Reasoning Group, AWS

[1]: https://www.aboutamazon.com/news/aws/aws-graviton-5-cpu-amazon-ec2
[2] : https://www.youtube.com/watch?v=3Gt-30Fm38U https://www.youtube.com/watch?v=3Gt-30Fm38U
[3]: https://www.youtube.com/watch?v=b0P55gHhG4g
[4]: https://sel4.systems/
[5]: https://flint.cs.yale.edu/certikos/
[6]: https://www.usenix.org/conference/usenixsecurity21/presentation/li-shih-wei
[7]: https://github.com/model-checking/kani
[8]: https://isabelle.in.tum.de/
[9]: https://iris-project.org/
[10]: https://github.com/verus-lang/verus
[11]: https://github.com/awslabs/AutoCorrode