Speaker
Mr
Daniil Maximov
(MIPT)
Description
Технология eBPF - активно развиваемая часть операционной системы ядра Linux, позволяющая вставлять и запускать заверенный верификатором пользовательский код в модулях ядра. Однако, как и с большим количеством другого системного ПО, эта подсистема не относится к доверенной кодовой базе Linux и в ней регулярно находятся уязвимости и ошибки. Эта работа посвящена изучению возможности применения property-based подхода в тестировании eBPF. Была построена модель подмножества eBPF на языке программирования Idris2, с помощью которой построен генератор случайных eBPF программ и проведено соответствующее тестирование официальной реализации eBPF.
Primary author
Mr
Daniil Maximov
(MIPT)
