eBPF Nədir və Niyə Vacibdir?

eBPF Linux nüvəsi daxilində kiçik proqramların təhlükəsiz şəkildə işlədilməsinə imkan verən güclü texnologiyadır. Adətən nüvəyə yeni funksiya əlavə etmək çox riskli və çətin işdir. eBPF isə şəbəkə paketlərini izləmək, sistem çağırışlarını təqib etmək, performansı ölçmək və ya təhlükəsizlik siyasəti tətbiq etmək kimi işlər üçün nüvəyə kiçik proqramlar yükləməyə imkan verir.

Bu gün eBPF bulud infrastrukturlarında, təhlükəsizlik monitorinq sistemlərində, şəbəkə performansının ölçülməsində və müşahidəolunma alətlərində geniş istifadə olunur. Buna görə eBPF proqramlarının təhlükəsizliyi yalnız tərtibatçıları deyil, server infrastrukturlarını, məlumat mərkəzlərini və təhlükəsizlik komandalarını da maraqlandırır.

Lakin eBPF proqramları adətən aşağı səviyyəli C kodu ilə yazılır. C dili güclü və sürətlidir; ancaq yaddaş təhlükəsizliyi, tip qarışıqlığı və səhvlərin yoxlanması kimi sahələrdə tərtibatçının üzərinə çox böyük məsuliyyət qoyur.

Linux eBPF Verifier Hər Şeyi Yoxlamırmı?

eBPF proqramları nüvəyə yüklənməzdən əvvəl Linux eBPF verifier tərəfindən yoxlanılır. Verifier proqramın sonsuz dövrə düşməməsini, müəyyən yaddaş təhlükəsizliyi qaydalarına əməl etməsini və nüvə daxilində qəbul edilə bilən şəkildə işləməsini yoxlayır.

Bu çox vacibdir; çünki nüvədə işləyəcək proqramın nəzarətsiz davranması bütün sistemə təsir edə bilər.

Lakin məqalənin vurğuladığı məqam budur:

Verifier mənbə kodu səviyyəsindəki bütün səhvləri aşkar etmək üçün nəzərdə tutulmayıb.

Verifier əsasən kompilyasiya olunmuş bytecode üzərində işləyir. Proqramçının mənbə kodunda nəyi nəzərdə tutduğunu, hansı struct sahəsini xaricə göndərmək istədiyini, hansı xəta qaytarışının yoxlanmalı olduğunu və ya hansı map sxeminin məntiqi baxımdan düzgün olduğunu hər zaman anlaya bilmir.

Buna görə bəzi səhvlər kompilyasiya oluna, verifier-dan keçə və icra zamanı səssiz şəkildə yanlış nəticə yarada bilər.

Məqalədə Hansı Səhv Sinifləri Müzakirə Olunur?

Tədqiqatçılar eBPF verifier-ın əhatə dairəsindən kənarda qala bilən altı səhv sinfindən bəhs edirlər.

Sadələşdirildikdə bunları belə izah etmək olar:

1. Başladılmamış verilənlərdən istifadə
Verilənlər strukturunun bəzi sahələri doldurulmadan istifadəçi məkanına göndərilə bilər. Bu halda yaddaşda qalan köhnə məlumatlar xaricə sıza bilər.

2. Köməkçi funksiyaların qaytarış dəyərlərinin yoxlanmaması
Bəzi eBPF köməkçi funksiyaları uğursuz ola bilər. Qaytarış dəyəri yoxlanmasa, proqram uğursuz oxumadan sonra belə məlumat göndərməyə davam edə bilər.

3. Buffer / ölçü uyğunsuzluğu
Tərtibatçı yalnız kiçik bir sahəni göndərmək istədiyi halda səhvən daha böyük struct ölçüsü verə bilər. Bu da əlavə məxfi sahələrin xaricə çıxmasına səbəb ola bilər.

4. Hook / context uyğunsuzluğu
Proqram müəyyən eBPF hook növü üçün yazılmış kimi göründüyü halda yanlış context strukturundan istifadə edə bilər. Bu, izlənən məlumatların səhv şərh olunmasına səbəb ola bilər.

5. Map növü və ya sxem qarışıqlığı
Map daxilində gözlənilən verilən tipi ilə yazılan və ya oxunan verilən tipi uyğun gəlməyə bilər.

6. İşarəli / işarəsiz ədədlərin qarışdırılması
Mənfi xəta kodları işarəsiz ədədə çevrilərsə, çox böyük müsbət dəyərlər kimi görünə və yanlış map açarları və ya yanlış nəticələr yarada bilər.

Bu səhv siniflərinin ortaq cəhəti budur: Proqram texniki olaraq işləyə bilər; lakin təhlükəsizlik və ya düzgünlük baxımından səhv davrana bilər.

Niyə Rust və Aya?

Rust yaddaş təhlükəsizliyi və tip təhlükəsizliyi baxımından C ilə müqayisədə daha güclü qoruma təmin edən müasir sistem proqramlaşdırma dilidir. Rust dəyişənin istifadə olunmazdan əvvəl başladılıb-başladılmadığı, tiplərin uyğunluğu, xəta nəticəsinin nəzərdən qaçırılıb-qaçırılmadığı kimi bir çox məsələdə tərtibatçını kompilyasiya mərhələsində məcbur edir.

Aya isə eBPF proqramlarını Rust ilə yazmağa imkan verən ekosistemdir. C/libbpf əsaslı yanaşmaya alternativ olaraq daha tip təhlükəsiz və Rust-a uyğun interfeys təqdim edir.

Məqalədəki əsas fikir budur:

Köhnə C eBPF proqramlarını birbaşa əl ilə yenidən yazmaq çox zəhmətli ola bilər.
Böyük dil modelləri çevirməni sürətləndirə bilər.
Lakin çevirmə yalnız “kompilyasiya olunur” deyə etibarlı qəbul edilməməlidir.
Buna görə çevirmədən sonra güclü doğrulama lazımdır.

Heimdall Nədir?

Heimdall C ilə yazılmış eBPF proqramlarını Rust/Aya-ya avtomatik köçürmək üçün təklif olunan çoxmərhələli sistemdir.

Sistemin məqsədi yalnız C kodunu Rust koduna çevirmək deyil. Əsas hədəf çevrilmiş Rust proqramının:

• Kompilyasiya oluna bilməsi
• Kernel verifier-dan keçməsi
• Təhlükəsiz Aya istifadəsinə uyğun olması
• Orijinal C proqramı ilə müşahidə edilə bilən davranış baxımından ekvivalent olması
• Səhv aşkarlandıqda LLM-ə əks əlaqə verərək çevirməni düzəltməsidir

Buna görə Heimdall klassik “AI kodu çevirdi” yanaşmasından daha irəli model təqdim edir. Burada süni intellekt təkbaşına qərar vermir; kompilyator, verifier, statik analiz, simvolik icra və Z3 kimi alətlərlə yoxlanılır.

Şəkil 1 Nəyi İzah Edir?

Məqalədəki Şəkil 1 Heimdall-ın beşmərhələli emal xəttini göstərir.

1. Mərhələ: LLM çevirməsi
C/libbpf eBPF proqramı böyük dil modeli tərəfindən Rust/Aya koduna çevrilir.

2. Mərhələ: Kompilyasiya və kernel verifier yoxlaması
Rust kodu eBPF bytecode-a kompilyasiya olunur. Sonra Linux kernel verifier proqramı qəbul edib-etmədiyini yoxlayır.

3. Mərhələ: Statik təhlükəsizlik analizi
Çevirmə təhlükəsiz Aya istifadəsinə zidd nümunələr baxımından yoxlanılır. Məsələn, lazımsız unsafe istifadəsinin, yoxlanılmayan helper nəticələrinin və ya başladılmamış output buffer istifadəsinin qarşısı alınmağa çalışılır.

4. Mərhələ: Simvolik icra
Həm orijinal C-dən gələn eBPF bytecode, həm də Rust-dan gələn eBPF bytecode simvolik şəkildə icra olunur. Yəni konkret test girişləri ilə deyil, bütün mümkün yolları təmsil edən məntiqi düsturlarla araşdırılır.

5. Mərhələ: Z3 ilə ekvivalentlik yoxlaması
Z3 həlledicisi iki proqramın eyni şərtlərdə eyni müşahidə edilə bilən davranışı yaradıb-yaratmadığını yoxlayır. Fərq tapsa, bu əks nümunə LLM-ə geri verilir və çevirmə düzəldilir.

Bu axının ən mühüm mesajı budur:

Kompilyasiya olunan kod yaratmaq kifayət deyil; təhlükəsiz və davranışı qoruyan kod yaratmaq lazımdır.

Şəkil 2 Nəyi Göstərir?

Məqalədəki Şəkil 2 tədqiqatçıların eBPF bytecode üçün angr adlı simvolik icra alətinə necə dəstək əlavə etdiyini göstərir.

eBPF proqramlarını simvolik şəkildə icra etmək asan deyil. Çünki bu proqramlar nüvə context strukturları, map əməliyyatları, helper funksiyaları və müxtəlif hook növləri ilə işləyir.

Tədqiqatçılar buna görə angr daxilində eBPF üçün beşqatlı dəstək hazırladıqlarını bildirirlər:

• eBPF ELF yükləyicisi
• eBPF arxitektura tərifi
• eBPF instruction lifter
• eBPF helper modelləri
• Düstur generatoru

Bu texniki infrastruktur C və Rust versiyalarının bytecode səviyyəsində müqayisəsini təmin edir. Beləliklə, C və Rust mənbə dillərinin fərqləri əvəzinə nüvəyə gedəcək real eBPF davranışı müqayisə olunur.

Düstur Nəyi İzah Edir? Proqram Ekvivalentliyi Necə Yoxlanılır?

Məqalənin mühüm riyazi ideyası budur:

eBPF proqramı girişləri qəbul edir, qaytarış dəyəri yaradır və map vəziyyətini dəyişə bilər.

Sadələşdirilmiş şəkildə:

Proqram = giriş + başlanğıc map vəziyyəti → qaytarış dəyəri + son map vəziyyəti

Heimdall C və Rust proqramlarının yalnız eyni qaytarış dəyəri verib-vermədiyinə baxmır. Eyni zamanda map yeniləmələri və xaricə göndərilən müşahidə edilə bilən nəticələr kimi yan təsirləri də nəzərə alır.

Ekvivalentlik yoxlaması bu suala endirilir:

C proqramı ilə Rust proqramının fərqli nəticə yarada bildiyi hər hansı giriş varmı?

Əgər Z3 belə giriş tapa bilmirsə, yəni əks nümunə yoxdursa, proqramlar ekvivalent qəbul edilir.

Bu, testdən daha güclü yanaşmadır. Çünki testlərdə yalnız seçilmiş nümunələr sınaqdan keçirilir. Simvolik doğrulamada isə mümkün qədər bütün davranış sahəsi məntiqi şəkildə araşdırılmağa çalışılır.

Niyə “Şərti Ekvivalentlik” İstifadə Olunur?

Burada çox mühüm və öyrədici bir məqam var.

Əgər C proqramında təhlükəsizlik boşluğu varsa və Rust çevirməsi bunu düzəldirsə, Rust proqramı bəzi hallarda C proqramından fərqli davranacaq. Əslində bu, arzu olunan fərqdir.

Məsələn, C proqramı helper uğursuz olsa belə köhnə məlumatı göndərə bilər. Rust çevirməsi isə xəta halında təhlükəsiz şəkildə çıxa bilər. Sərt ekvivalentlik yoxlaması bu halda “Rust fərqli davrandı” deyərək təhlükəsiz çevirməni rədd edə bilər.

Buna görə Heimdall “şərti ekvivalentlik” ideyasından istifadə edir.

Sadə mənası budur:

Rust proqramı C proqramının təhlükəsiz qəbul edilən yollarında eyni davranışı göstərməlidir.
Lakin C-dəki təhlükəsizlik səhvinin işə düşdüyü yollarda Rust-ın daha təhlükəsiz davranmasına icazə verilir.

Bu fərq vacibdir. Çünki məqsəd pis davranışı olduğu kimi kopyalamaq deyil, düzgün davranışı qoruyarkən səhv davranışı təhlükəsiz hala gətirməkdir.

Qiymətləndirmə Necə Aparılıb?

Tədqiqatda tədqiqatçılar 119 eBPF proqramı toplayıblar. Aya-nın dəstəkləmədiyi bəzi xüsusiyyətlərə görə bunların 102-si etibarlı çevirmə və doğrulama dəstinə daxil edilib.

Məqalə üç çevirmə yanaşmasını müqayisə edir:

Baseline:
LLM agentinə C kodu verilir və Rust/Aya çevirməsi etməsi istənilir. Kompilyasiya oluna bilən nəticə yaratması gözlənilir.

Heimdall Deterministic:
Beşmərhələli emal xətti xarici nəzarətçi tərəfindən ardıcıllıqla işlədilir. LLM yalnız əks əlaqə əsasında yeni namizəd çevirmə yaradır.

Heimdall Agentic:
Agent eyni Heimdall prinsiplərinə əməl edir, lakin fayl oxuma, axtarış aparma, bytecode-u araşdırma və köməkçi alətlərdən istifadə məsələsində daha sərbəst davranır.

Bu fərq vacibdir. Çünki müasir proqram təminatı hazırlayan agentlər yalnız mətn yaratmır; fayl axtarır, əmr işlədir, xəta çıxışını oxuyur və yenidən sınaqdan keçirir. Məqalə alət istifadəsinin yaratdığı fərqi də ölçür.

Nəticələr Nəyi Göstərir?

Məqalədəki ən diqqətçəkən nəticələrdən biri budur:

Bütün 102 etibarlı proqram üzərində Heimdall Agentic 96 proqram üçün formal şəkildə doğrulanmış, ekvivalent Rust çevirməsi yaradıb. Bu göstərici 94,1 faiz kimi bildirilir.

Qalan altı proqram üçün tədqiqatçılar bunu birbaşa real çevirmə səhvi kimi deyil, simvolik icra və ya həlledicinin miqyaslana bilmə sərhədi kimi izah edirlər. Üç proqram qismən doğrulanıb, üç proqram isə solver sərhədlərini aşdığı üçün doğrulana bilməyib.

Benchmark cədvəli həmçinin yalnız kompilyasiyanın kifayət etmədiyini göstərir. Baseline üsullarının hamısı 51 proqramı kompilyasiya edə bilir; lakin təhlükəsizlik və ekvivalentlik yoxlamaları əlavə edildikdə tam uğurlu çevirmələrin sayı çox aşağı qalır.

Bu, proqram təminatı təhlükəsizliyi baxımından güclü bir dərs verir:

Kodun kompilyasiya olunması onun düzgün və təhlükəsiz olduğu demək deyil.

Hansı Təhlükəsizlik Boşluqları Aradan Qaldırılıb?

Məqalədəki verilənlər dəsti üzərində aparılan təhlildə Heimdall-ın müşahidə olunan üç səhv sinfini aradan qaldırdığı bildirilir:

• Başladılmamış vəziyyət: 10 nümunədən 10-u
• Yoxlanılmayan helper qaytarışları: 44 nümunədən 44-ü
• İşarəli / işarəsiz ədəd qarışıqlığı: 6 nümunədən 6-sı

Bu nəticələr Heimdall-ın yalnız çevirmə aləti deyil, eyni zamanda mənbə kodu səviyyəsində müəyyən təhlükəsizlik səhvlərini azaldan köçürmə xətti kimi hazırlandığını göstərir.

Lakin bu nəticələr bütün eBPF dünyası üçün ümumi zəmanət deyil. Bunlar yalnız məqalənin araşdırdığı və doğruladığı verilənlər dəsti üçün bildirilmiş nəticələrdir.

Runtime Sınaqları Nəyi İzah Edir?

Tədqiqatçılar formal şəkildə doğrulanmış bəzi Rust çevirmələrinin icra zamanı da oxşar davranıb-davranmadığını yoxlamaq üçün 10 proqram üzərində təcrübə aparırlar.

C və Rust versiyaları eyni nəzarət olunan iş yükləri altında işlədilir. Cədvəl 5-də bu proqramların hər biri üçün 100 sınaqdan 100 uğurlu keçid bildirilir. Runtime overhead dəyərləri proqramdan proqrama dəyişir. Bəzilərində Rust versiyası daha yavaş görünür, bəzi nümunələrdə isə daha sürətli və ya yaxın nəticələr bildirilir.

Bu hissənin sadə mesajı budur:

Formal doğrulama güclü alətdir; lakin icra zamanı yoxlama da praktik davranışı görmək üçün dəyərlidir.

Tədqiqat Nə Deyir?

Tədqiqatın əsas mesajını bir neçə məqamda toplamaq olar.

Birincisi, eBPF verifier çox dəyərli təhlükəsizlik qatı olsa da, təkbaşına mənbə kodu səviyyəsində bütün səhvləri aşkar etmir.

İkincisi, Rust və Aya kimi daha tip təhlükəsiz alətlər eBPF proqramlarında bəzi səhv siniflərinin kompilyasiya və ya API səviyyəsində qarşısını ala bilər.

Üçüncüsü, böyük dil modelləri köhnə C kodlarını Rust-a köçürməkdə faydalı ola bilər; lakin bu çevirmələr yalnız LLM çıxışına etibar edilərək qəbul edilməməlidir.

Dördüncüsü, simvolik icra və Z3 əsaslı ekvivalentlik yoxlaması çevirmənin həqiqətən davranışı qoruyub-qorumadığını daha güclü şəkildə yoxlaya bilər.

Beşincisi, təhlükəsizliyi yaxşılaşdıran çevirmələr üçün şərti ekvivalentlik kimi diqqətli doğrulama təriflərinə ehtiyac var. Çünki təhlükəsiz Rust çevirməsi C-dəki səhv davranışı olduğu kimi kopyalamamalıdır.

Bu Niyə Vacibdir?

Bu tədqiqat süni intellekt dəstəkli proqram təminatı çevrilməsinin gələcəyi baxımından mühüm dərs verir.

Köhnə sistem kodlarını müasir və daha təhlükəsiz dillərə köçürmək proqram təminatı dünyasının böyük problemlərindən biridir. Maliyyə, bulud, əməliyyat sistemi, şəbəkə infrastrukturu və təhlükəsizlik alətlərində illərlə yığılmış C kodu var. Bu kodları əl ilə yenidən yazmaq bahalı və risklidir.

LLM-lər bu prosesi sürətləndirə bilər. Lakin sistem səviyyəli təhlükəsizlik kodlarında “AI çevirdi, kompilyasiya olundu, bitdi” yanaşması təhlükəli ola bilər. Çünki kiçik tip səhvi, yanlış map yeniləməsi və ya natamam xəta yoxlaması ciddi nəticələr doğura bilər.

Heimdall-ın əhəmiyyəti burada ortaya çıxır. Bu tədqiqat AI kod çevirməsinin yalnız güclü alətlərlə yoxlanıldıqda etibarlı ola biləcəyini göstərən araşdırma nümunəsi təqdim edir.

Yəni gələcəkdə təhlükəsiz proqram təminatı modernləşdirilməsi yalnız süni intellektin mətn yaratması ilə deyil; kompilyator, statik analiz, simvolik icra, solver və əks nümunə əsasında düzəliş dövrlərinin birlikdə istifadəsi ilə irəliləyə bilər.

Diqqət Edilməli Məqamlar

Bu tədqiqat güclü nəticələr təqdim etsə də, bəzi məhdudiyyətləri var.

Birincisi, tədqiqat preprintdir. Nəticələrin müstəqil akademik qiymətləndirmədə və müxtəlif sistemlərdə təkrar yoxlanması lazımdır.

İkincisi, Heimdall-ın uğuru sınaqdan keçirilən eBPF proqramları və Aya-nın dəstəklədiyi xüsusiyyətlərlə məhdudlaşır. Aya-nın dəstəkləmədiyi bəzi map növləri, USDT arqumentləri və ya köhnə socket-filter təlimatları əhatə dairəsindən çıxarılıb.

Üçüncüsü, 96 proqramın doğrulanması çox güclü nəticə olsa da, qalan proqramlarda solver və simvolik icranın miqyaslana bilmə sərhədləri görünür. Bu, formal doğrulamanın praktikada hələ də xərc tələb edə biləcəyini göstərir.

Dördüncüsü, Rust daha təhlükəsiz dil olsa da, Rust eBPF proqramlarında tamamilə unsafe olmadan işləmək hər zaman mümkün deyil. Məqalədə də yaradılmış çevirmələrdə orta hesabla unsafe əməliyyatların olduğu bildirilir. Əsas məsələ bu unsafe sahələrin daraldılması və nəzarətdə saxlanmasıdır.

Beşincisi, məqalədəki təhlükəsizlik nəticələri müəyyən açıq mənbəli proqramlar və test şərtləri əsasında bildirilib. Bu nəticələri ümumiləşdirərkən ehtiyatlı olmaq, ittihamedici və ya qəti hökm verən dildən qaçmaq lazımdır.

Nəhayət, formal ekvivalentlik müəyyən modelləşdirilmiş davranışlara əsaslanır. Modeldən kənarda qalan kernel davranışları, aparat təsirləri və ya dəstəklənməyən köməkçi funksiyalar ayrıca qiymətləndirilməlidir.

Nəticə

Bu tədqiqat süni intellekt dəstəkli kod çevrilməsinin ciddi sistem proqram təminatında necə daha təhlükəsiz hala gətirilə biləcəyini göstərən mühüm nümunə təqdim edir.

Heimdall köhnə C eBPF proqramlarını Rust/Aya-ya çevirmək üçün böyük dil modellərindən istifadə edir; lakin çevirməni yalnız LLM-in öhdəsinə buraxmır. Kompilyasiya, kernel verifier, statik təhlükəsizlik siyasəti, simvolik icra və Z3 əsaslı ekvivalentlik yoxlamasını eyni xəttdə birləşdirir.

Tədqiqatın ən mühüm mesajı budur:

Təhlükəsiz proqram təminatı modernləşdirilməsində süni intellekt sürət verə bilər; lakin etibar doğrulama alətləri ilə qazanılır.

eBPF kimi nüvə səviyyəsinə yaxın işləyən sistemlərdə bu yanaşma xüsusilə dəyərlidir. Çünki burada mənbə kodundakı kiçik səhv belə məlumat sızması, yanlış təhlükəsizlik qərarı və ya sistem müşahidəsi xətası kimi nəticələr doğura bilər.

Heimdall bu problemlərin son həlli deyil; lakin AI dəstəkli çevirmə ilə formal doğrulamanı birləşdirən güclü tədqiqat istiqamətini təmsil edir.

Mənbə və Metod Qeydi

Bu məzmun Vishnu Asutosh Dasu, Monika Santra, Md Rafi Ur Rashid, Ashish Kumar, Saeid Tizpaz-Niari və Gang Tan tərəfindən hazırlanmış “Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust” adlı akademik tədqiqatdan istifadə edilərək Verianla redaksiya formatında orijinal şəkildə hazırlanıb.

Tədqiqat arXiv-də yayımlanmış preprint xarakterlidir. Məzmun məlumatlandırma və təhsil məqsədi daşıyır. Kibertəhlükəsizlik, Linux nüvəsinin hazırlanması, eBPF proqramlaşdırması, korporativ sistem təhlükəsizliyi və ya peşəkar proqram təminatı doğrulaması üzrə məsləhətin yerini tutmur.