eBPF деген эмне жана эмне үчүн маанилүү?

eBPF — Linux өзөгүнүн ичинде чакан программаларды коопсуз иштетүүгө мүмкүндүк берген кубаттуу технология. Адатта өзөккө жаңы мүмкүнчүлүк кошуу өтө тобокелдүү жана татаал иш. Ал эми eBPF тармак пакеттерин көзөмөлдөө, системалык чакырууларды байкоо, өндүрүмдүүлүктү өлчөө же коопсуздук саясатын колдонуу сыяктуу иштер үчүн өзөккө чакан программаларды жүктөөгө мүмкүндүк берет.

Бүгүнкү күндө eBPF булут инфраструктураларында, коопсуздукту көзөмөлдөө системаларында, тармак өндүрүмдүүлүгүн өлчөөдө жана байкоочулук куралдарында кеңири колдонулат. Ошондуктан eBPF программаларынын коопсуздугу иштеп чыгуучуларды гана эмес, сервердик инфраструктураларды, маалымат борборлорун жана коопсуздук командаларын да кызыктырат.

Бирок eBPF программалары адатта төмөн деңгээлдеги C коду менен жазылат. C тили күчтүү жана ылдам; бирок эс тутум коопсуздугу, типтердин аралашуусу жана каталарды текшерүү сыяктуу тармактарда иштеп чыгуучуга өтө чоң жоопкерчилик жүктөйт.

Linux eBPF Verifier баарын текшербейби?

eBPF программалары өзөккө жүктөлөрдөн мурда Linux eBPF verifier тарабынан текшерилет. Verifier программанын чексиз циклге кирбешин, айрым эс тутум коопсуздугу эрежелерине ылайык болушун жана өзөктүн ичинде кабыл алынуучу түрдө иштешин көзөмөлдөйт.

Бул абдан маанилүү; анткени өзөктө иштей турган программанын көзөмөлсүз жүрүм-туруму бүтүндөй системага таасир этиши мүмкүн.

Бирок макала баса белгилеген жагдай мындай:

Verifier баштапкы код деңгээлиндеги ар бир катаны кармоо үчүн иштелип чыккан эмес.

Verifier негизинен компиляцияланган bytecode үстүндө иштейт. Программист баштапкы коддо эмнени көздөгөнүн, кайсы struct талаасын тышка жөнөткүсү келгенин, кайсы ката кайтарымы текшерилиши керектигин же кайсы map схемасы логикалык жактан туура экенин ал дайыма эле түшүнө албайт.

Ошондуктан айрым каталар компиляцияланышы, verifier текшерүүсүнөн өтүшү жана иштөө маалында үн-сөзсүз туура эмес натыйжа чыгарышы мүмкүн.

Макалада кайсы ката класстары талкууланат?

Изилдөөчүлөр eBPF verifier камтыбай калышы мүмкүн болгон алты ката классын белгилешет.

Аларды жөнөкөйлөштүрүп төмөнкүдөй түшүндүрүүгө болот:

1. Инициализацияланбаган маалыматты колдонуу
Маалымат түзүмүнүн айрым талаалары толтурулбай туруп колдонуучу мейкиндигине жөнөтүлүшү мүмкүн. Мындай учурда эс тутумдагы эски калдыктар сыртка чыгып кетиши мүмкүн.

2. Helper функцияларынын кайтарым маанилерин текшербөө
Айрым eBPF helper функциялары ишке ашпай калышы мүмкүн. Эгер кайтарым маани текшерилбесе, программа ийгиликсиз окуудан кийин да маалымат жөнөтүүнү уланта бериши мүмкүн.

3. Buffer / өлчөм дал келбестиги
Иштеп чыгуучу чакан гана талааны жөнөткүсү келип туруп, жаңылыштык менен чоңураак struct өлчөмүн бериши мүмкүн. Бул кошумча купуя талаалардын да сыртка чыгышына алып келиши мүмкүн.

4. Hook / context дал келбестиги
Программа белгилүү бир eBPF hook түрү үчүн жазылгандай көрүнүп туруп, туура эмес context түзүмүн колдонушу мүмкүн. Бул байкалган маалыматтын туура эмес чечмеленишине алып келиши мүмкүн.

5. Map түрү же схемасынын аралашуусу
Map ичинде күтүлгөн маалымат түрү менен жазылган же окулган маалымат түрү бири-бирине дал келбей калышы мүмкүн.

6. Белгилүү / белгисиз сан түрлөрүнүн аралашуусу
Терс ката коддору белгисиз сан түрүнө айлантылса, алар өтө чоң оң маанилер сыяктуу көрүнүп, туура эмес map ачкычтарын же туура эмес натыйжаларды чыгарышы мүмкүн.

Бул ката класстарынын жалпы өзгөчөлүгү мындай: программа техникалык жактан иштеши мүмкүн, бирок коопсуздук же тууралык жагынан туура эмес жүрүм-турум көрсөтүшү мүмкүн.

Эмне үчүн Rust жана Aya?

Rust — эс тутум коопсуздугу жана тип коопсуздугу боюнча Cге караганда күчтүүрөөк коргоолорду сунуш кылган заманбап системалык программалоо тили. Rust өзгөрмө колдонулардан мурун инициализацияланганбы, типтер шайкешпи, ката натыйжасы көз жаздымда калтырылып жатабы деген сыяктуу көп маселеде иштеп чыгуучуну компиляция баскычында мажбурлайт.

Aya — eBPF программаларын Rust менен жазууга арналган экосистема. Ал C/libbpf негизиндеги ыкмага альтернатива катары тип коопсуздугу жогору жана Rustка ылайыктуу интерфейс сунуш кылат.

Макаладагы негизги ой мындай:

Эски C eBPF программаларын кол менен түздөн-түз кайра жазуу өтө көп эмгекти талап кылышы мүмкүн.
Чоң тил моделдери которууну тездетиши мүмкүн.
Бирок котормо «компиляцияланат» дегени үчүн эле ишенимдүү деп кабыл алынбашы керек.
Ошондуктан которуудан кийин күчтүү текшерүү талап кылынат.

Heimdall деген эмне?

Heimdall — C тилинде жазылган eBPF программаларын Rust/Ayaга автоматтык көчүрүү үчүн сунушталган көп баскычтуу система.

Системанын максаты C кодун Rust кодуна гана которуу эмес. Негизги максат — которулган Rust программасынын:

• Компиляциялана алышы
• Kernel verifier текшерүүсүнөн өтүшү
• Коопсуз Aya колдонуу эрежелерине ылайык болушу
• Түпнуска C программасына байкалуучу жүрүм-турум жагынан эквиваленттүү болушу
• Ката табылганда LLMге кайра байланыш берип, котормону оңдошу

Ошондуктан Heimdall классикалык «AI кодду которду» ыкмасынан алдыга кеткен модель сунуш кылат. Бул жерде жасалма интеллект жалгыз чечим кабыл албайт; ал компилятор, verifier, статикалык талдоо, символдук аткаруу жана Z3 сыяктуу куралдар менен текшерилет.

1-сүрөт эмнени түшүндүрөт?

Макаладагы 1-сүрөт Heimdallдын беш баскычтуу иштетүү конвейерин көрсөтөт.

1. Баскыч: LLM котормосу
C/libbpf eBPF программасы чоң тил модели тарабынан Rust/Aya кодуна которулат.

2. Баскыч: Компиляция жана kernel verifier текшерүүсү
Rust коду eBPF bytecodeго компиляцияланат. Андан соң Linux kernel verifier бул программаны кабыл алабы же жокпу текшерилет.

3. Баскыч: Статикалык коопсуздук талдоосу
Котормо коопсуз Aya колдонууга каршы келген үлгүлөр боюнча текшерилет. Мисалы, керексиз unsafe колдонуу, текшерилбеген helper натыйжалары же инициализацияланбаган output buffer колдонуу болтурбоого аракет кылынат.

4. Баскыч: Символдук аткаруу
Түпнуска Cден алынган eBPF bytecode да, Rustтан алынган eBPF bytecode да символдук түрдө аткарылат. Башкача айтканда, белгилүү тесттик киргизүүлөр менен эмес, бардык мүмкүн болгон жолдорду көрсөткөн логикалык формулалар аркылуу талданат.

5. Баскыч: Z3 менен эквиваленттүүлүктү текшерүү
Z3 чечүүчүсү эки программанын бирдей шарттарда бирдей байкалуучу жүрүм-турум чыгарарын же чыгарбасын текшерет. Эгер айырма тапса, бул каршы мисал LLMге кайра берилет жана котормо оңдолот.

Бул агымдын эң маанилүү билдирүүсү мындай:

Компиляциялана турган код чыгаруу жетишсиз; коопсуз жана жүрүм-турумду сактаган код чыгаруу керек.

2-сүрөт эмнени көрсөтөт?

Макаладагы 2-сүрөт изилдөөчүлөрдүн eBPF bytecode үчүн angr аттуу символдук аткаруу куралына кантип колдоо кошконун көрсөтөт.

eBPF программаларын символдук түрдө аткаруу оңой эмес. Анткени бул программалар өзөктүн context түзүмдөрү, map операциялары, helper функциялары жана ар түрдүү hook түрлөрү менен иштейт.

Ошондуктан изилдөөчүлөр angr ичинде eBPF үчүн беш катмарлуу колдоо иштеп чыкканын түшүндүрүшөт:

• eBPF ELF жүктөгүчү
• eBPF архитектурасынын аныктамасы
• eBPF instruction lifter
• eBPF helper моделдери
• Формула генератору

Бул техникалык инфраструктура C жана Rust версияларын bytecode деңгээлинде салыштырууга мүмкүндүк берет. Ошентип, C жана Rust баштапкы тилдеринин айырмачылыктарынын ордуна өзөккө бара турган чыныгы eBPF жүрүм-туруму салыштырылат.

Формула эмнени түшүндүрөт? Программанын эквиваленттүүлүгү кантип текшерилет?

Макаланын маанилүү математикалык идеясы мындай:

eBPF программасы киргизүүлөрдү алат, кайтарым маани чыгарат жана map абалын өзгөртө алат.

Жөнөкөйлөштүрүлгөн түрдө:

Программа = киргизүү + баштапкы map абалы → кайтарым маани + акыркы map абалы

Heimdall C жана Rust программалары бирдей кайтарым маани берип-бербегенин гана карабайт. Ал map жаңыртуулары жана тышка жөнөтүлгөн байкалуучу натыйжалар сыяктуу кошумча таасирлерди да эске алат.

Эквиваленттүүлүк текшерүүсү төмөнкү суроого кыскарат:

C программасы менен Rust программасы ар башка натыйжа бере турган кандайдыр бир киргизүү барбы?

Эгер Z3 мындай киргизүүнү таба албаса, башкача айтканда каршы мисал жок болсо, программалар эквиваленттүү деп кабыл алынат.

Бул тест жүргүзүүгө караганда күчтүүрөөк ыкма. Анткени тесттерде тандалган мисалдар гана сыналат. Ал эми символдук текшерүүдө мүмкүн болушунча бүт жүрүм-турум мейкиндиги логикалык жактан талданууга аракет кылынат.

Эмне үчүн «Шарттуу эквиваленттүүлүк» колдонулат?

Бул жерде өтө маанилүү жана үйрөтүүчү жагдай бар.

Эгер C программасында коопсуздук боштугу болуп, Rust котормосу аны оңдосо, Rust программасы айрым учурларда C программасынан башкача иштейт. Бул чындыгында кааланган айырма.

Мисалы, C программасы helper ишке ашпай калса да эски маалыматты жөнөтүшү мүмкүн. Rust котормосу болсо ката болгон учурда коопсуз түрдө чыга алат. Катуу эквиваленттүүлүк текшерүүсү мындай учурда «Rust башкача иштеди» деп коопсуз котормону четке кагышы мүмкүн.

Ошондуктан Heimdall «шарттуу эквиваленттүүлүк» идеясын колдонот.

Жөнөкөй мааниси мындай:

Rust программасы C программасынын коопсуз деп эсептелген жолдорунда бирдей жүрүм-турум көрсөтүшү керек.
Ал эми Cдеги коопсуздук катасы ишке кирген жолдордо Rustка коопсузураак жүрүм-турум көрсөтүүгө уруксат берилет.

Бул айырма маанилүү. Анткени максат жаман жүрүм-турумду бирдей көчүрүү эмес, туура жүрүм-турумду сактап, ката жүрүм-турумду коопсуз абалга келтирүү.

Баалоо кантип жүргүзүлгөн?

Изилдөөдө окумуштуулар 119 eBPF программасын топтогон. Aya колдобогон айрым мүмкүнчүлүктөрдөн улам алардын 102си жарактуу котормо жана текшерүү топтомуна киргизилген.

Макала үч которуу ыкмасын салыштырат:

Baseline:
LLM агентине C коду берилет жана Rust/Ayaга которуу талап кылынат. Компиляциялана турган натыйжа чыгарышы күтүлөт.

Heimdall Deterministic:
Беш баскычтуу конвейер тышкы контроллер тарабынан кезеги менен аткарылат. LLM кайра байланыштын негизинде гана жаңы талапкер котормону чыгарат.

Heimdall Agentic:
Агент ошол эле Heimdall принциптерин сактайт, бирок файлдарды окуу, издөө жүргүзүү, bytecode карап чыгуу жана жардамчы куралдарды колдонуу жагынан эркин иштейт.

Бул айырма маанилүү. Анткени заманбап программалык камсыздоо иштеп чыгуу агенттери текст гана чыгарбайт; файл издейт, буйрук аткарат, ката чыгышын окуйт жана кайра аракет кылат. Макала ушул курал колдонуу алып келген айырманы да өлчөйт.

Натыйжалар эмнени көрсөтөт?

Макаладагы эң көңүл бурарлык натыйжалардын бири мындай:

Бардык 102 жарактуу программада Heimdall Agentic 96 программа үчүн формалдуу түрдө текшерилген эквиваленттүү Rust котормосун чыгарган. Бул көрсөткүч пайыз менен 94,1 деп берилет.

Калган алты программа боюнча изилдөөчүлөр муну түздөн-түз чыныгы котормо катасы деп эмес, символдук аткаруунун же чечүүчүнүн масштабдуулук чеги деп түшүндүрүшөт. Үч программа жарым-жартылай текшерилген, дагы үч программа solver чектеринен ашып кеткендиктен текшериле алган эмес.

Benchmark таблицасы компиляциянын өзү жетишсиз экенин да көрсөтөт. Baseline ыкмаларынын баары 51 программаны компиляциялай алат; бирок коопсуздук жана эквиваленттүүлүк текшерүүлөрү кошулганда толук ийгиликтүү котормолордун саны өтө төмөн бойдон калат.

Бул программалык коопсуздук үчүн күчтүү сабак берет:

Коддун компиляцияланышы анын туура жана коопсуз экенин билдирбейт.

Кайсы коопсуздук боштуктары жабылган?

Макаладагы маалымат топтомунда жүргүзүлгөн талдоодо Heimdall байкалган үч ката классын жапканы билдирилет:

• Инициализацияланбаган абал: 10 мисалдын 10у
• Текшерилбеген helper кайтарымдары: 44 мисалдын 44ү
• Белгилүү / белгисиз сан түрлөрүнүн аралашуусу: 6 мисалдын 6сы

Бул натыйжалар Heimdall жөн гана котормо жасаган курал эмес, ошондой эле баштапкы код деңгээлиндеги айрым коопсуздук каталарын азайтуучу көчүрүү конвейери катары иштелип чыкканын көрсөтөт.

Бирок бул натыйжалар бүт eBPF дүйнөсү үчүн жалпы кепилдик эмес. Алар макалада сканерленген жана текшерилген маалымат топтому үчүн гана билдирилген жыйынтыктар.

Runtime сыноолору эмнени түшүндүрөт?

Изилдөөчүлөр формалдуу түрдө текшерилген айрым Rust котормолору иштөө маалында да окшош жүрүм-турум көрсөтөр-көрсөтпөсүн текшерүү үчүн 10 программада эксперимент жүргүзөт.

C жана Rust версиялары бирдей көзөмөлдөнгөн жумуш жүктөрүндө иштетилет. 5-таблицада бул программалардын ар бири үчүн 100 сыноонун 100үндө ийгиликтүү өтүү көрсөтүлгөн. Runtime overhead маанилери программадан программага өзгөрөт. Айрымдарында Rust версиясы жайыраак көрүнсө, кээ бир мисалдарда ылдамыраак же жакын натыйжалар берилген.

Бул бөлүктүн жөнөкөй билдирүүсү мындай:

Формалдуу текшерүү күчтүү курал; бирок иштөө убактысын текшерүү да практикалык жүрүм-турумду көрүү үчүн баалуу.

Изилдөө эмнени айтып жатат?

Изилдөөнүн негизги билдирүүсүн бир нече пунктка топтоого болот.

Биринчиден, eBPF verifier өтө баалуу коопсуздук катмары болгону менен, жалгыз өзү баштапкы код деңгээлиндеги бардык каталарды кармай албайт.

Экинчиден, Rust жана Aya сыяктуу тип коопсуздугу жогору куралдар eBPF программаларындагы айрым ката класстарын компиляция же API деңгээлинде бөгөттөй алат.

Үчүнчүдөн, чоң тил моделдери эски C кодун Rustка көчүрүүдө пайдалуу болушу мүмкүн; бирок мындай котормолор LLM чыгарган жыйынтыкка гана ишенип кабыл алынбашы керек.

Төртүнчүдөн, символдук аткаруу жана Z3 негизиндеги эквиваленттүүлүк текшерүүсү котормонун жүрүм-турумду чындап сактап-сактабаганын күчтүүрөөк түрдө көзөмөлдөй алат.

Бешинчиден, коопсуздукту жакшырткан котормолор үчүн шарттуу эквиваленттүүлүк сыяктуу кылдат текшерүү аныктамалары керек. Анткени коопсуз Rust котормосу Cдеги ката жүрүм-турумду бирдей көчүрбөшү керек.

Бул эмне үчүн маанилүү?

Бул изилдөө жасалма интеллект колдогон программалык трансформациянын келечеги үчүн маанилүү сабак берет.

Эски системалык коддорду заманбап жана коопсузураак тилдерге көчүрүү программалык камсыздоо дүйнөсүндөгү чоң көйгөйлөрдүн бири. Финансы, булут, операциялык система, тармак инфраструктурасы жана коопсуздук куралдарында жылдар бою топтолгон C коду бар. Бул коддорду кол менен кайра жазуу кымбат жана тобокелдүү.

LLMдер бул процессти тездетиши мүмкүн. Бирок системалык деңгээлдеги коопсуздук коддорунда «AI которду, компиляцияланды, бүттү» деген ыкма кооптуу болушу мүмкүн. Анткени кичинекей тип катасы, туура эмес map жаңыртуусу же жетишсиз ката текшерүүсү олуттуу кесепеттерге алып келиши мүмкүн.

Heimdallдын мааниси ушул жерде көрүнөт. Бул изилдөө AI код котормосу күчтүү куралдар менен текшерилгенде гана ишенимдүү боло аларын көрсөткөн изилдөө мисалын сунуш кылат.

Демек, келечекте коопсуз программалык модернизация жасалма интеллекттин текст чыгаруусу менен гана эмес; компилятор, статикалык талдоо, символдук аткаруу, solver жана каршы мисал аркылуу оңдоо циклдерин бирге колдонуу менен өнүгүшү мүмкүн.

Көңүл бурууга тийиш болгон жагдайлар

Бул изилдөө күчтүү натыйжаларды көрсөткөнү менен, айрым чектөөлөргө ээ.

Биринчиден, изилдөө preprint болуп саналат. Жыйынтыктар көз карандысыз академиялык баалоодон өтүп, ар башка системаларда кайталанышы керек.

Экинчиден, Heimdallдын ийгилиги сыналган eBPF программалары жана Aya колдогон мүмкүнчүлүктөр менен чектелет. Aya колдобогон айрым map түрлөрү, USDT аргументтери же эски socket-filter көрсөтмөлөрү камтылган эмес.

Үчүнчүдөн, 96 программанын текшерилиши өтө күчтүү натыйжа болгону менен, калган программаларда solver жана символдук аткаруунун масштабдуулук чектери байкалган. Бул формалдуу текшерүү практикада дагы эле чыгымдуу болушу мүмкүн экенин көрсөтөт.

Төртүнчүдөн, Rust коопсузураак тил болгону менен, Rust eBPF программаларында unsafe таптакыр колдонулбай иштөө дайыма эле мүмкүн эмес. Макала да чыгарылган котормолордо орточо unsafe операциялары бар экенин билдирет. Маанилүүсү — бул unsafe аймактарды тарылтуу жана көзөмөлдөө.

Бешинчиден, макаладагы коопсуздук жыйынтыктары белгилүү ачык булактуу программалар жана тесттик шарттар боюнча берилген. Бул жыйынтыктарды жалпылоодо этият болуу, айыптоочу же кескин өкүмдүү тил колдонбоо керек.

Акырында, формалдуу эквиваленттүүлүк белгилүү моделденген жүрүм-турумдарга таянат. Моделге кирбеген kernel жүрүм-турумдары, аппараттык таасирлер же колдоого алынбаган жардамчы функциялар өзүнчө бааланышы керек.

Жыйынтык

Бул изилдөө жасалма интеллект колдогон код трансформациясын олуттуу системалык программалык камсыздоодо кантип коопсузураак кылууга болорун көрсөткөн маанилүү мисал.

Heimdall эски C eBPF программаларын Rust/Ayaга которуу үчүн чоң тил моделдерин колдонот; бирок которууну LLMге гана тапшырбайт. Ал компиляцияны, kernel verifierди, статикалык коопсуздук саясатын, символдук аткарууну жана Z3 негизиндеги эквиваленттүүлүк текшерүүсүн бир конвейерге бириктирет.

Изилдөөнүн эң маанилүү билдирүүсү мындай:

Коопсуз программалык модернизацияда жасалма интеллект ылдамдык бере алат; бирок ишеним текшерүү куралдары аркылуу жаралат.

eBPF сыяктуу өзөк деңгээлине жакын иштеген системаларда бул ыкма өзгөчө баалуу. Анткени бул жерде баштапкы коддогу кичинекей ката да маалыматтын агып кетишине, туура эмес коопсуздук чечимине же системаны байкоо катасына алып келиши мүмкүн.

Heimdall бул көйгөйлөрдүн акыркы чечими эмес; бирок AI колдогон котормо менен формалдуу текшерүүнү бириктирген күчтүү изилдөө багытын билдирет.

Булак жана ыкма жөнүндө эскертүү

Бул мазмун Vishnu Asutosh Dasu, Monika Santra, Md Rafi Ur Rashid, Ashish Kumar, Saeid Tizpaz-Niari жана Gang Tan тарабынан даярдалган «Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust» аттуу академиялык эмгектин негизинде Verianla редакциялык форматында оригиналдуу түрдө даярдалды.

Изилдөө arXiv платформасында жарыяланган preprint мүнөзүндөгү эмгек. Мазмун маалымат берүү жана билим берүү максатын көздөйт. Ал киберкоопсуздук, Linux өзөгүн иштеп чыгуу, eBPF программалоо, корпоративдик системалардын коопсуздугу же кесиптик программалык текшерүү боюнча кеңештин ордун баспайт.