До конференции осталось — :::

Формальной верификации обзорчик: безопасная разработка за пределами рандомизированных тестов

19:35 - 20:15
30 мин
Defensive Track

Что поделать, чтобы писать безопасный софт помимо code review и серьезнейшего тестирования? Писать меньше кода и больше теорем! Посмотрим, как HTTPS сейчас защищают на уровне реализации. 

Все знают, что понять код, который не влезает в один экран сложно. Какое решение? Ограничить семантику для лучшей композиции; дать пользователям волшебство дешевого моделирования; выкрутить статический и динамический анализ до 11. 

Этот доклад — ураганный пробег по стэйт-оф-зэ-арт в формальной верификации, с кейсами верифицированной ОС (CertiKOS), HTTPS-компонентов, на которых работает большая часть веб (Project Everest), и ядра Linux (linux.git/*.tla; модели блокировок). Зачем? Чтобы мы писали лучший код, разумеется. С благодатию Computer Science.

Спикеры
Дмитрий «wldhx» Волков
Поделиться
Другие доклады
Hardware Zone
Разбираемся в видах Flash памяти
Web Village
Фантастические баги и где они обитают
Web Village
Приключения хакера на сайтах знакомств
Наверх