Seminarium: Systemy Rozproszone
17 marca 2022 12:15, sala 4070, transmisja online
Karol Baryła, Cezary Bednarz



LinKRID: Weryfikowanie zliczania referencji w jądrze z użyciem frameworka KLEE do wykonania symbolicznego



Wykonanie symboliczne polega na wykonywaniu kodu gdzie zamiast niektórych danych wejściowych podstawiamy zmienne symboliczne. W efekcie otrzymujemy zbiór ograniczeń, które możemy następnie rozwiązać używając SMT solvera, by utrzymać dane wejściowe powodujące wykonanie danej ścieżki. Wykonanie symboliczne jest stosowane głównie do szukania błędów w oprogramowaniu i testowania go, ale także do deobfuskacji czy inżynierii wstecznej.

KLEE jest frameworkiem do dynamicznego wykonania symbolicznego, działającym na poziomie kodu bitowego LLVM.

W trakcie prezentacji pokażę proste przykłady użycia KLEE, oraz opowiem jak został zastosowany do weryfikacji zliczania referencji w jądrze - skutkując znalezieniem 118 błędów, w tym 87 nowych.

Zapraszam,
Karol Baryła



Bibliografia:





Rust for Linux



Język C od zawsze był jedynym dostępnym językiem używanym przy tworzeniu jądra Linuksa, a dodanie drugiego języka budziło w społeczności wiele kontrowersji. Rust, popularny wysokopoziomowy język, dopiero od niedawna okazał się słusznym kandydatem. Projekt Rust for Linux przez ostatnie kilka lat zbliżył się do tego celu i możliwe jest, że niedługo zostanie on włączony do jądra.

Opowiem o tym co osiągnął projekt Rust for Linux, oraz o argumentach za i przeciw używania tego typu języka w jądrze.

Zapraszam,
Cezary Bednarz



Bibliografia: