eBPF Nedir ve Neden Önemlidir?

eBPF, Linux çekirdeği içinde küçük programların güvenli biçimde çalıştırılmasını sağlayan güçlü bir teknolojidir. Normalde çekirdeğe yeni özellik eklemek çok riskli ve zor bir iştir. eBPF ise ağ paketlerini izlemek, sistem çağrılarını takip etmek, performans ölçümü yapmak veya güvenlik politikası uygulamak gibi işlerde çekirdeğe küçük programlar yüklemeye izin verir.

Bugün eBPF; bulut altyapılarında, güvenlik izleme sistemlerinde, ağ performansı ölçümlerinde ve gözlemlenebilirlik araçlarında yaygın şekilde kullanılıyor. Bu nedenle eBPF programlarının güvenliği yalnızca geliştiricileri değil, sunucu altyapılarını, veri merkezlerini ve güvenlik ekiplerini de ilgilendiriyor.

Fakat eBPF programları genellikle düşük seviyeli C koduyla yazılıyor. C dili güçlü ve hızlıdır; ancak bellek güvenliği, tür karışıklığı ve hata kontrolü gibi alanlarda geliştiriciye çok fazla sorumluluk bırakır.

Linux eBPF Verifier Her Şeyi Kontrol Etmiyor mu?

eBPF programları çekirdeğe yüklenmeden önce Linux eBPF verifier tarafından kontrol edilir. Verifier, programın sınırsız döngüye girmemesini, bazı bellek güvenliği kurallarına uymasını ve çekirdek içinde kabul edilebilir biçimde çalışmasını denetler.

Bu çok önemlidir; çünkü çekirdekte çalışacak bir programın kontrolsüz davranması tüm sistemi etkileyebilir.

Ancak makalenin vurguladığı nokta şudur:

Verifier, her kaynak kodu düzeyi hatayı yakalamak için tasarlanmamıştır.

Verifier daha çok derlenmiş bytecode üzerinden çalışır. Programcının kaynak kodda neyi amaçladığını, hangi struct alanını dışarı göndermek istediğini, hangi hata dönüşünün kontrol edilmesi gerektiğini veya hangi map şemasının mantıksal olarak doğru olduğunu her zaman anlayamaz.

Bu yüzden bazı hatalar derlenebilir, verifier’dan geçebilir ve çalışma zamanında sessizce yanlış sonuç üretebilir.

Makalede Hangi Hata Sınıfları Tartışılıyor?

Araştırmacılar, eBPF verifier’ın kapsamı dışında kalabilen altı hata sınıfından söz ediyor.

Bunlar sadeleştirildiğinde şöyle açıklanabilir:

1. Başlatılmamış veri kullanımı
Bir veri yapısının bazı alanları doldurulmadan kullanıcı alanına gönderilebilir. Bu durumda eski bellek artıkları dışarı sızabilir.

2. Yardımcı fonksiyon dönüşlerinin kontrol edilmemesi
Bazı eBPF yardımcı fonksiyonları başarısız olabilir. Eğer dönüş değeri kontrol edilmezse, program başarısız okuma sonrası bile veri göndermeye devam edebilir.

3. Buffer / boyut uyumsuzluğu
Geliştirici yalnızca küçük bir alanı göndermek isterken yanlışlıkla daha büyük struct boyutu verebilir. Bu da fazladan özel alanların dışarı çıkmasına neden olabilir.

4. Hook / context uyumsuzluğu
Program bir eBPF hook türü için yazılmış gibi görünürken yanlış context yapısını kullanabilir. Bu, izlenen verilerin yanlış yorumlanmasına yol açabilir.

5. Map türü veya şema karışıklığı
Bir map içinde beklenen veri tipiyle yazılan veya okunan veri tipi uyuşmayabilir.

6. İşaretli / işaretsiz sayı karışıklığı
Negatif hata kodları işaretsiz sayıya çevrilirse çok büyük pozitif değerler gibi görünebilir ve yanlış map anahtarları veya yanlış sonuçlar üretebilir.

Bu hata sınıflarının ortak noktası şudur: Program teknik olarak çalışabilir; fakat güvenlik veya doğruluk açısından yanlış davranabilir.

Neden Rust ve Aya?

Rust, bellek güvenliği ve tür güvenliği konusunda C’ye göre daha güçlü korumalar sunan modern bir sistem programlama dilidir. Rust, bir değişken kullanılmadan önce başlatılmış mı, türler uyumlu mu, hata sonucu göz ardı ediliyor mu gibi birçok konuda geliştiriciyi derleme aşamasında zorlar.

Aya ise eBPF programlarını Rust ile yazmaya yarayan bir ekosistemdir. C/libbpf tabanlı yaklaşıma alternatif olarak daha tip güvenli ve Rust’a uygun bir yüzey sunar.

Makaledeki temel fikir şudur:

Eski C eBPF programlarını doğrudan elle yeniden yazmak çok zahmetli olabilir.
Büyük dil modelleri çeviriyi hızlandırabilir.
Ama çeviri yalnızca “derleniyor” diye güvenilir kabul edilmemelidir.
Bu yüzden çeviri sonrası güçlü doğrulama gerekir.

Heimdall Nedir?

Heimdall, C ile yazılmış eBPF programlarını Rust/Aya’ya otomatik taşımak için önerilen çok aşamalı bir sistemdir.

Sistemin amacı yalnızca C kodunu Rust koduna çevirmek değildir. Asıl hedef, çevrilen Rust programının:

• Derlenebilir olması
• Kernel verifier’dan geçmesi
• Güvenli Aya kullanımına uygun olması
• Orijinal C programıyla gözlenebilir davranış açısından eşdeğer olması
• Hata bulunduğunda LLM’ye geri bildirim vererek çeviriyi onarmasıdır

Bu nedenle Heimdall, klasik “AI kod çevirdi” yaklaşımından daha ileri bir model sunuyor. Burada yapay zekâ tek başına karar vermiyor; derleyici, verifier, statik analiz, sembolik yürütme ve Z3 gibi araçlarla denetleniyor.

Şekil 1 Ne Anlatıyor?

Makaledeki Şekil 1, Heimdall’ın beş aşamalı işlem hattını gösteriyor.

1. Aşama: LLM çevirisi
C/libbpf eBPF programı, büyük dil modeli tarafından Rust/Aya koduna çevrilir.

2. Aşama: Derleme ve kernel verifier kontrolü
Rust kodu eBPF bytecode’a derlenir. Ardından Linux kernel verifier bu programı kabul ediyor mu diye kontrol edilir.

3. Aşama: Statik güvenlik analizi
Çeviri, güvenli Aya kullanımına aykırı kalıplar açısından denetlenir. Örneğin gereksiz unsafe kullanımı, kontrol edilmeyen helper sonuçları veya başlatılmamış output buffer kullanımı engellenmeye çalışılır.

4. Aşama: Sembolik yürütme
Hem orijinal C’den gelen eBPF bytecode hem de Rust’tan gelen eBPF bytecode sembolik olarak çalıştırılır. Yani belirli test girdileriyle değil, tüm olası yolları temsil eden mantıksal formüllerle incelenir.

5. Aşama: Z3 ile eşdeğerlik kontrolü
Z3 çözücü, iki programın aynı koşullarda aynı gözlenebilir davranışı üretip üretmediğini kontrol eder. Eğer fark bulursa, bu karşı örnek LLM’ye geri verilir ve çeviri onarılır.

Bu akışın en önemli mesajı şudur:

Derlenebilir kod üretmek yeterli değildir; güvenli ve davranışı koruyan kod üretmek gerekir.

Şekil 2 Ne Gösteriyor?

Makaledeki Şekil 2, araştırmacıların eBPF bytecode için angr adlı sembolik yürütme aracına nasıl destek eklediğini gösteriyor.

eBPF programlarını sembolik olarak yürütmek kolay değildir. Çünkü bu programlar çekirdek context yapıları, map işlemleri, helper fonksiyonları ve farklı hook türleriyle çalışır.

Araştırmacılar bu nedenle angr içinde eBPF için beş katmanlı destek geliştirdiklerini anlatıyor:

• eBPF ELF yükleyici
• eBPF mimari tanımı
• eBPF instruction lifter
• eBPF helper modelleri
• Formül üretici

Bu teknik altyapı, C ve Rust sürümlerinin bytecode düzeyinde karşılaştırılmasını sağlıyor. Böylece C ve Rust kaynak dillerinin farklılıkları yerine, çekirdeğe gidecek gerçek eBPF davranışı karşılaştırılıyor.

Formül Ne Anlatıyor? Program Eşdeğerliği Nasıl Kontrol Ediliyor?

Makalenin önemli matematiksel fikri şudur:

Bir eBPF programı, girdileri alır, bir dönüş değeri üretir ve map durumunu değiştirebilir.

Sadeleştirilmiş biçimde:

Program = girdi + başlangıç map durumu → dönüş değeri + son map durumu

Heimdall, C ve Rust programlarının yalnızca aynı dönüş değerini verip vermediğine bakmaz. Aynı zamanda map güncellemeleri ve dışarıya gönderilen gözlenebilir sonuçlar gibi yan etkileri de dikkate alır.

Eşdeğerlik kontrolü şu soruya indirgenir:

C programı ile Rust programının farklı sonuç üretebildiği herhangi bir girdi var mı?

Eğer Z3 böyle bir girdi bulamazsa, yani karşı örnek yoksa, programlar eşdeğer kabul edilir.

Bu, test etmekten daha güçlü bir yaklaşımdır. Çünkü testlerde yalnızca seçilmiş örnekler denenir. Sembolik doğrulamada ise mümkün olduğunca tüm davranış alanı mantıksal olarak incelenmeye çalışılır.

Neden “Koşullu Eşdeğerlik” Kullanılıyor?

Burada çok önemli ve öğretici bir nokta var.

Eğer C programında güvenlik açığı varsa ve Rust çevirisi bunu düzeltiyorsa, Rust programı bazı durumlarda C programından farklı davranacaktır. Bu aslında istenen bir farktır.

Örneğin C programı helper başarısız olsa bile eski veriyi gönderebilir. Rust çevirisi ise hata durumunda güvenli biçimde çıkabilir. Katı eşdeğerlik kontrolü bu durumda “Rust farklı davrandı” diyerek güvenli çeviriyi reddedebilir.

Bu yüzden Heimdall “koşullu eşdeğerlik” fikrini kullanıyor.

Sade anlamı şudur:

Rust programı, C programının güvenli kabul edilen yollarında aynı davranışı göstermelidir.
Ama C’deki güvenlik hatasının tetiklendiği yollarda Rust’ın daha güvenli davranmasına izin verilir.

Bu ayrım önemlidir. Çünkü amaç kötü davranışı birebir kopyalamak değil, doğru davranışı korurken hatalı davranışı güvenli hale getirmektir.

Değerlendirme Nasıl Yapılmış?

Çalışmada araştırmacılar 119 eBPF programı toplamış. Aya’nın desteklemediği bazı özellikler nedeniyle bunların 102’si geçerli çeviri ve doğrulama setine alınmış.

Makale üç çeviri yaklaşımını karşılaştırıyor:

Baseline:
LLM ajanına C kodu veriliyor ve Rust/Aya çevirisi yapması isteniyor. Derlenebilir sonuç üretmesi bekleniyor.

Heimdall Deterministic:
Beş aşamalı işlem hattı dış bir kontrolcü tarafından sırayla işletiliyor. LLM yalnızca geri bildirimle yeni aday çeviri üretiyor.

Heimdall Agentic:
Ajan, aynı Heimdall ilkelerini izliyor ama dosya okuma, arama yapma, bytecode inceleme ve yardımcı araç kullanma konusunda daha serbest davranıyor.

Bu ayrım önemli. Çünkü modern yazılım geliştirme ajanları yalnızca metin üretmez; dosya arar, komut çalıştırır, hata çıktısını okur ve yeniden dener. Makale, bu araç kullanımıyla gelen farkı da ölçüyor.

Sonuçlar Ne Gösteriyor?

Makaledeki en dikkat çekici sonuçlardan biri şudur:

Tüm 102 geçerli program üzerinde Heimdall Agentic, 96 program için formal olarak doğrulanmış eşdeğer Rust çevirisi üretmiştir. Bu oran yüzde 94,1 olarak raporlanıyor.

Kalan altı program için araştırmacılar bunları doğrudan gerçek çeviri hatası olarak değil, sembolik yürütme veya çözücü ölçeklenebilirliği sınırı olarak açıklıyor. Üç program kısmen doğrulanmış, üç program ise solver sınırlarını aştığı için doğrulanamamıştır.

Benchmark tablosu ayrıca yalnızca derlemenin yeterli olmadığını gösteriyor. Baseline yöntemlerin tamamı 51 programı derleyebiliyor; fakat güvenlik ve eşdeğerlik kontrolleri eklendiğinde tam başarılı çeviri sayısı çok düşük kalıyor.

Bu, yazılım güvenliği açısından güçlü bir ders veriyor:

Kodun derlenmesi, kodun doğru ve güvenli olduğu anlamına gelmez.

Hangi Güvenlik Açıkları Kapatılmış?

Makaledeki veri seti üzerinde yapılan analizde Heimdall’ın üç gözlenen hata sınıfını kapattığı raporlanıyor:

• Başlatılmamış durum: 10 örnekten 10’u
• Kontrol edilmeyen helper dönüşleri: 44 örnekten 44’ü
• İşaretli / işaretsiz sayı karışıklığı: 6 örnekten 6’sı

Bu sonuçlar, Heimdall’ın yalnızca çeviri yapan bir araç değil, aynı zamanda belirli kaynak kodu düzeyi güvenlik hatalarını azaltan bir taşıma hattı olarak tasarlandığını gösteriyor.

Ancak bu sonuçlar tüm eBPF dünyası için genel garanti değildir. Sadece makalenin taradığı ve doğruladığı veri seti için raporlanan bulgulardır.

Runtime Denemeleri Ne Anlatıyor?

Araştırmacılar, formal olarak doğrulanan bazı Rust çevirilerinin çalışma zamanında da benzer davranıp davranmadığını kontrol etmek için 10 program üzerinde deney yapıyor.

C ve Rust sürümleri aynı kontrollü iş yükleri altında çalıştırılıyor. Tablo 5’te bu programların her biri için 100 denemede 100 başarılı geçiş raporlanıyor. Runtime overhead değerleri programdan programa değişiyor. Bazılarında Rust sürümü daha yavaş görünürken, bazı örneklerde daha hızlı veya yakın sonuçlar raporlanmış.

Bu bölümün sade mesajı şudur:

Formal doğrulama güçlü bir araçtır; ancak çalışma zamanı kontrolü de pratik davranışı görmek için değerlidir.

Araştırma Ne Söylüyor?

Çalışmanın ana mesajı birkaç noktada toplanabilir.

Birincisi, eBPF verifier çok değerli bir güvenlik katmanı olsa da tek başına kaynak kodu düzeyi tüm hataları yakalamaz.

İkincisi, Rust ve Aya gibi daha tip güvenli araçlar, eBPF programlarında bazı hata sınıflarını derleme veya API düzeyinde engelleyebilir.

Üçüncüsü, büyük dil modelleri eski C kodlarını Rust’a taşımada yararlı olabilir; fakat bu çeviriler yalnızca LLM çıktısına güvenilerek kabul edilmemelidir.

Dördüncüsü, sembolik yürütme ve Z3 tabanlı eşdeğerlik kontrolü, çevirinin gerçekten davranışı koruyup korumadığını daha güçlü biçimde denetleyebilir.

Beşincisi, güvenlik iyileştiren çeviriler için koşullu eşdeğerlik gibi dikkatli doğrulama tanımlarına ihtiyaç vardır. Çünkü güvenli Rust çevirisi, C’deki hatalı davranışı birebir kopyalamamalıdır.

Bu Neden Önemli?

Bu çalışma, yapay zekâ destekli yazılım dönüşümünün geleceği açısından önemli bir ders veriyor.

Eski sistem kodlarını modern ve daha güvenli dillere taşımak yazılım dünyasının büyük sorunlarından biridir. Finans, bulut, işletim sistemi, ağ altyapısı ve güvenlik araçlarında yıllarca birikmiş C kodu vardır. Bu kodları elle yeniden yazmak pahalı ve risklidir.

LLM’ler bu süreci hızlandırabilir. Ancak sistem düzeyi güvenlik kodlarında “AI çevirdi, derlendi, tamam” yaklaşımı tehlikeli olabilir. Çünkü küçük bir tür hatası, yanlış map güncellemesi veya eksik hata kontrolü ciddi sonuçlar doğurabilir.

Heimdall’ın önemi burada ortaya çıkıyor. Bu çalışma, AI kod çevirisinin ancak güçlü araçlarla denetlendiğinde güvenilir olabileceğini gösteren bir araştırma örneği sunuyor.

Yani gelecekte güvenli yazılım modernizasyonu, yalnızca yapay zekâ metin üretimiyle değil; derleyici, statik analiz, sembolik yürütme, solver ve karşı örnekli onarım döngülerinin birlikte kullanılmasıyla ilerleyebilir.

Dikkat Edilmesi Gereken Noktalar

Bu çalışma güçlü sonuçlar sunsa da bazı sınırlamalara sahiptir.

İlk olarak, çalışma preprinttir. Bulguların bağımsız akademik değerlendirme ve farklı sistemlerde tekrar edilmesi gerekir.

İkinci olarak, Heimdall’ın başarısı test edilen eBPF programları ve Aya’nın desteklediği özelliklerle sınırlıdır. Aya’nın desteklemediği bazı map türleri, USDT argümanları veya eski socket-filter talimatları kapsam dışı bırakılmıştır.

Üçüncü olarak, 96 programın doğrulanması çok güçlü bir sonuç olsa da kalan programlarda solver ve sembolik yürütme ölçeklenebilirliği sınırları görülmektedir. Bu, formal doğrulamanın pratikte hâlâ maliyetli olabileceğini gösterir.

Dördüncü olarak, Rust daha güvenli bir dil olsa da Rust eBPF programlarında tamamen unsafe olmadan çalışmak her zaman mümkün değildir. Makale de üretilen çevirilerde ortalama unsafe operasyonları bulunduğunu raporlamaktadır. Önemli olan bu unsafe bölgelerin daraltılması ve denetlenmesidir.

Beşinci olarak, makaledeki güvenlik bulguları belirli açık kaynak programlar ve test koşulları üzerinden raporlanmıştır. Bu bulgular genelleştirilirken dikkatli olunmalı, suçlayıcı veya kesin hükümlü dil kullanılmamalıdır.

Son olarak, formal eşdeğerlik belirli modellenmiş davranışlara dayanır. Model dışı kalan kernel davranışları, donanım etkileri veya desteklenmeyen yardımcı fonksiyonlar ayrıca değerlendirilmelidir.

Sonuç

Bu araştırma, yapay zekâ destekli kod dönüşümünün ciddi sistem yazılımlarında nasıl daha güvenli hale getirilebileceğini gösteren önemli bir örnek sunuyor.

Heimdall, eski C eBPF programlarını Rust/Aya’ya çevirmek için büyük dil modellerinden yararlanıyor; fakat çeviriyi yalnızca LLM’ye bırakmıyor. Derleme, kernel verifier, statik güvenlik politikası, sembolik yürütme ve Z3 tabanlı eşdeğerlik kontrolünü aynı hatta birleştiriyor.

Çalışmanın en önemli mesajı şudur:

Güvenli yazılım modernizasyonunda yapay zekâ hız sağlayabilir; fakat güven, doğrulama araçlarıyla kazanılır.

eBPF gibi çekirdek seviyesine yakın çalışan sistemlerde bu yaklaşım özellikle değerlidir. Çünkü burada küçük bir kaynak kodu hatası bile veri sızıntısı, yanlış güvenlik kararı veya sistem gözlemi hatası gibi sonuçlar doğurabilir.

Heimdall, bu sorunlara nihai çözüm değildir; ancak AI destekli çeviri ile formal doğrulamayı birleştiren güçlü bir araştırma yönünü temsil eder.

Kaynak ve Yöntem Notu

Bu içerik, Vishnu Asutosh Dasu, Monika Santra, Md Rafi Ur Rashid, Ashish Kumar, Saeid Tizpaz-Niari ve Gang Tan tarafından hazırlanan “Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust” başlıklı akademik çalışmadan yararlanılarak Verianla editoryal formatında özgün olarak hazırlanmıştır.

Çalışma arXiv üzerinde yayımlanmış preprint niteliğindedir. İçerik bilgilendirme ve eğitim amacı taşır. Siber güvenlik, Linux çekirdeği geliştirme, eBPF programlama, kurumsal sistem güvenliği veya profesyonel yazılım doğrulama danışmanlığı yerine geçmez.