Идеи и инсайты

Исследуем AI-first разработку, кодовые ограждения и архитектуру одноразовости.

abstract-interpretationstatic-analysismetainfer

Meta нашла 100 000 багов в production-коде статическим анализатором, который никогда не запускает программу

Infer от Meta использует abstract interpretation и bi-abduction для поиска null dereference, утечек памяти и race conditions, рассуждая о структуре кода, а не о его выполнении. Вот как это работает и как использовать в своей codebase.

Meta выпустила более 100 000 исправлений багов, пойманных статическим анализатором до того, как код дошёл до пользователя. Инструмент называется Infer, он open…
abstract-interpretationstatic-analysissafety-criticalaviation

Статический анализ не может доказать, что ваш самолёт не разобьётся. Но он может доказать кое-что более полезное.

Абстрактная интерпретация аппроксимирует сверху каждое возможное состояние программы. Если деление на ноль недостижимо в абстракции, оно недостижимо и в реальном коде. Вот как это работает и где даёт сбои.

Статический анализ не может доказать, что самолёт не разобьётся. Но он может доказать, что контур управления высотомером никогда не поделит на ноль, никогда не…
abstract-interpretationstatic-analysisruntime-errorsverification

Как доказать, что в вашем коде нет ошибок времени выполнения (и почему вы, скорее всего, бросите эту затею)

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

Ваш набор тестов проходит. Ваш type checker зелёный. Вы выкладываете в прод. Через два часа продакшен выдаёт на граничном случае, который никому не пришло в…
hardware-assisted-safetychericporting

Ваш код на C может работать на capability-оборудовании без полного rewrite

Гибридный ABI CHERI позволяет портировать код на C на capability-оборудование постепенно. Вот как компилировать, что ломается и как это исправить без rewrite всей codebase.

У вас есть codebase на C, которая слишком велика для rewrite на Rust и слишком критична, чтобы оставлять её уязвимой для переполнений буфера.…
hardware-assisted-safetycapability-hardwarecherisoftware-history

Hardware capability не провалился. Он пришёл на 40 лет раньше времени.

Безопасность памяти на уровне hardware была возможна с 1970-х. Вот почему архитектуры capability проигрывали плоским моделям памяти, и почему CHERI наконец меняет расклад.

Семьдесят процентов CVE — это баги memory safety. Buffer overflows, use-after-free, double frees. Тип уязвимостей, который позволяет атакующему перейти от…
hardware-assisted-safetysandboxingcwebassembly

Ваша зависимость на C может уронить весь процесс. WebAssembly может это остановить.

Контейнеры — это overkill для изоляции одной C-библиотеки. Скомпилируйте её в WebAssembly и запустите внутри WASI-sandbox для memory safety, capability-based доступа к файловой системе и crash containment без Docker.

Одиночный null pointer dereference внутри C-библиотеки может уронить всё приложение. Если эта библиотека парсит пользовательский ввод, декомпрессирует…
hardware-assisted-safetymemory-corruptionmobileasan

Ваш телефон уже оснащён аппаратным обеспечением, которое обнаруживает повреждение памяти

ARM Memory Tagging Extension и GWP-ASan делают возможным обнаружение проблем безопасности памяти в продакшене на современных мобильных устройствах. Вот как они работают и каковы компромиссы.

Ваш телефон может обнаруживать повреждение памяти в продакшене. Не с помощью полной инструментации, которую вы запускаете в CI, и не при каждом выделении…
hardware-assisted-safetybuffer-overflowmemory-safetycheri

Buffer Overflows Продолжают Происходить, Потому Что Мы Исправляем Их в Software

CHERI — это hardware-расширение, которое превращает каждый pointer в bounded capability. Вот как оно останавливает buffer overflows на уровне CPU, что это стоит и как попробовать его на реальном оборудовании.

Buffer overflows находятся в CWE Top 25 уже двадцать лет. У нас есть stack canaries, ASLR, DEP, control-flow integrity и memory-safe языки, но они всё равно…
cleanroom-correctnessllmformal-proofsautomation

LLM не могут доказать корректность вашего кода, но они могут написать шаблонный код, который это делает

Верификация по методологии Cleanroom требует генерации и разрядки обязательств доказательства. Вот как LLM автоматизируют аннотации и генерацию VC, чтобы вы могли сосредоточиться на самых сложных доказательствах.

Cleanroom-инжиниринг программного обеспечения требует, чтобы вы доказали корректность своего кода ещё до компиляции. Это звучит благородно, пока вы не…
cleanroom-correctnessprocessefficiencypragmatism

Cleanroom Даёт 0,1 Дефектов на KLOC. Полный Ритуал Для Этого Не Нужен.

Cleanroom software engineering снижает плотность дефектов в 100 раз, но полное внедрение требует отдельных команд тестирования и формальных доказательств. Вот прагматичное подмножество, которое улавливает большую часть выгоды без overhead.

Cleanroom software engineering даёт 0,1 дефекта на тысячу строк кода. Средний показатель по отрасли — от 10 до 50. Подвох в том, что полный Cleanroom требует…