LLM xotirasini dastur tahlili motoriga aylantirish: Lemmalog qanday paydo bo'ldi

LLM agentlar katta kod bazalarida harakatlanish, noma'lum podtizimlarni tushuntirish va hujum sirtlarini o'rganishda ajoyib natijalar ko'rsatmoqda. Lekin tahliil bir necha soat davom ettirilganda, model tez-tez avval aniqlangan faktlarni unutib, rad etilgan yo'llarni taklif qilishi yoki noto'g'ri premissalardan kelib chiqqan xulosalarga qat'iy ishonishi sodir bo'ladi. Bu oddiy gallyutsinatsiya emas — model o'z ichidagi mantiqiy zanjirni boshqara olmasligi.

Xotira tizimlari nima uchun yetarli emas

Mavjud yechimlar odatda eski suhbatlarni yoki kuzatuvlarni vektor bazasiga saqlab, kerak paytida eng mos keluvchilarni qaytaradi. Bu nima aytilganini eslatadi, lekin hozir nima bilinganini saqlamaydi. Farqni tushunish uchun quyidagi misolga e'tibor bering:

attacker controls object_a
object_a points to object_b
object_b is a kernel object

• hujumchi object_a ni boshqaradi;
• object_a → object_b ga ko'rsatadi;
• object_b — kernel obyekti.

Bu uchta faktdan «hujumchi kernel obyektini boshqaradi» xulosasi kelib chiqadi. Oddiy xotira tizimi barcha uchta faktni saqlab, so'rov kelganda ularni modelga beradi — model yana bir marta xulosani o'zi yasaydi.

Lekin ikki soat keyin debuggerda object_a aslida object_b ga ko'rmayotgani aniqlanadi. Endi bazada quyidagilar bo'ladi:

object_a points to object_b
attacker can control object_b
object_a does not actually point to object_b

• object_a → object_b (eski, noto'g'ri fakt);
• hujumchi object_b ni boshqaradi (eski xulosa);
• object_a → object_b emas (yangi, to'g'ri fakt).

Model bu to'plamdan qaysi xulosalar hali kuchda, qaysilari yo'qolganini o'zi aniqlashi kerak. Bu ishonchsiz va qiyin.

Dastur tahlili bilan o'xshashlik

Bu muammo dastur tahlilida (program analysis) juda yaqin tanish. Waalarda ham faktlar (masalan, calls(foo, bar)) va qoidalari (agar A B ni chaqirsa, B C ni chaqirsa → A C ga yetadi) bo'lib, ularning nuqtai tinchlik (fixed point) hisoblanadi. Muhimi — biror kiritma fakt o'zgarganda, faqat ta'sirlangan natijalar yangilanadi, butun tahlil qayta ishga tushirilmas.

calls(foo, bar)
calls(bar, baz)

Shu fikr: «Nima uchun LLM har safar butun holatni qayta qurib, barcha oqibatlarni o'zi topishi kerak? Nima agar biz faqat holatni saqlab turib, o'zgarishlar avtomatik tarqalmasin?»

Shu savol muallifni Datalog motorini LLM uchun yozishga undadi.

controls(attacker, object_a).
points_to(object_a, object_b).
kernel_object(object_b).

Datalog qanday ishlaydi

Datalog — deklarativ mantiqiy dasturlash tili. Siz «qanday hisoblash» ni emas, «qaysi faktlar mavjud» va «qaysi qoidalardan yangi faktlar kelib chiqadi» ni tasvirlaysiz.

controls(attacker, object_a).
points_to(object_a, object_b).
kernel_object(object_b).

controls_kernel_object(Attacker) :-
    controls(Attacker, ObjectA),
    points_to(ObjectA, ObjectB),
    kernel_object(ObjectB).

Motor avtomatik ravishda controls_kernel_object(attacker) ni hosil qiladi. Agar keyin points_to(object_a, object_b) faktini bekor qilsak, motor aniq biladi: controls_kernel_object bu faktga bog'liq edi, shuning uchun u ham bekor qilinadi. Hech qanday «umid qilamiz, model o'zi tushunadi» kerak emas.

controls_kernel_object(Attacker) :-
controls(Attacker, ObjectA),
points_to(ObjectA, ObjectB),
kernel_object(ObjectB).

Lemmalog arxitekturasi

Lemmalog muammoni ikkiga bo'ladi:

• LLM — noaniq (fuzzy) qism: manba kodini, LLDB chiqishini, loglarni o'qiydi va ularni tuzilgan faktlarga aylantiradi. Masalan: freed(object_a), reused_as(object_a, write_target).
• Lemmalog — aniq (deterministic) qism: faktlar + qoidalardan kelib chiquvchi barcha xulosalarni saqlab turadi va biror fakt o'chirilganda/ o'zgartirilganda ta'sirlangan zanjirni avtomatik yangilaydi.

Bunday ajratma LLM ning kuchli tomonlari (kod tushunish, kontekstni o'qish) dan foydalanib, zaif tomoni (uzun mantiqiy zanjirni eslab turish) ni bazaga yuklaydi.

controls_kernel_object(attacker).

Faktlarni bekor qilish (retraction) muammosi

Fakt qo'shish oson: yangi fakt kiriting, qoidalarni qayta baholang. Lekin o'chirish murakkab. Misol:

a.
b.
c :- a.
c :- b.

c ning ikkita mustaqil sababi bor. Agar a o'chirilsa, c hali b orqali rost. Oddiy Datalog motorlari bu uchun provenance (kelib chiqish izi) yoki reference counting mexanizmlaridan foydalanadi. Lemmalog bu masalani hal qilishi uchun har bir hosil qilingan faktning qaysi asos faktlarga bog'liq ekanligini kuzatib boradi.

points_to(object_a, object_b).

Nima uchun bu muhim

Zarurlik qidiruvi (vulnerability research) — bu faqat kod o'qish emas, bu gipoteza sinovlari ketma-ketligi. Har bir gipoteza yangi faktlar beradi, ba'zilari rad etiladi, ba'zilari mustahkamlab boradi. Oddiy chat konteksti bu dinamikani ushlab turolmaydi. Lemmalog esa bu jarayonni versiyalangan, qayta tiklanadigan, mantiqiy toza holatga aylantiradi.

Bu yondashuv faqat xavfsizlik uchun emas. Har qanday uzluh, ko'p qadamli tahliil talab qiluvchi vazifa — kompyuter tarmog'i diagnostikasi, moliya modelingi, huquqiy hujjatlar tahlili — shu arxitekturadan foyda ko'rishi mumkin.

"LLDB shows that the freed object is later reused
as the destination of the write."
|
v
freed(object_a)
reused_as(object_a, write_target)

Cheklovlar va ochiq savollar

• Faktlarni aniqlash sifati. LLM noto'g'ri fakt chiqarinsa (masalan, pointer arifmetikasini xato tushuntirsa), motor bu xatoni «rost» deb qabul qiladi va notekis xulosalar quradi. Bu yerda tekshiruv mexanizmlari (masalan, ikkinchi LLM tekshiruvi yoki avtomatik testlar) kerak.
• Qoidalarning murakkabligi. Haqiqiy kodda qoidalari yozish — masalan, xotira xavfsizligi, alias analizi, parallelizm — o'ziga xos murakkablikka ega. Lemmalog hozirda umumiy motor, lekin maxsus domen qoidalari to'plami hali rivojlanmoqda.
• Masshtablanish.
  Datalog motorlari katta fakt to'plamlari uchun optimallashtirilgan (Soufflé, Differential Dataflow), lekin real vaqtda interaktiv ishlash va LLM bilan tez almashinuv talab qiladi.

Kelajak: agent — bu faqat «fakt ekstraktor» emas

Muallif fikriga ko'ra, kelajakda LLM agentlari faqat «nima yo'qolganini» topib, faktlarni bazaga tushuruvchi modulga aylanadi. Barcha mantiqiy nazariya, gipoteza sinovi va xulosa yasash — deterministik bazada amalga oshiriladi. Bu agentlarni ko'proq ishonchli, tahlil qilinadigan va qayta ishlatiladigan qiladi.

Lemmalog hali erta bosqichda, lekin u LLM xotirasini «so'zlar to'plami»dan «mantiqiy holat mashinasiga» aylantirish yo'lini ko'rsatdi. Bu — agent arxitekturasida paradigmaviy o'zgarish bo'lishi mumkin.

Asl manba: pwning.systems