# AlphaProof Code and Signal: ellenőrzött gépi kódú biztonsági igazolások és megbízható feltételezések

Published: 2026-11-11

A Google DeepMind géppel ellenőrzött biztonsági tulajdonságok igazolásáról számol be egy lefordított libsignal parancssori "heveder" esetében. A Lean ellenőrzi az igazolást, míg az emberek jóváhagyják a specifikációt és annak feltételezéseit. Egy külön összehasonlító ellenőrzi a tételt és az összes függő definíciót a jóváhagyott cél ellenében.

Canonical: https://thedailydiff.dev/hu/video/2026-11-10-signal-machine-proof/

## Amit ez a videó tartalmaz

- Az AI-ügynökök jelölt igazolásokat készítenek; a Lean kernelje ellenőrzi, hogy azok alátámasztják-e az emberi jóváhagyással rendelkező formális állítást.
- Az ellenőrzött cél egy adott lefordított libsignal CLI "heveder", megbízható szemantikával és kriptográfiai szerződésekkel.
- A lefordított bináris bizonyítása eltávolítja a Rust fordítót a megbízható alapból az adott bináris megadott tulajdonságai tekintetében.
- A kutatók két, korábban kijavított hiba elkülönített újra bevezetéséről számolnak be, amelyek sértik a szimbolikus biztonsági tételüket.
- Az összehasonlító ellenőrzi a tételt és minden függő definíciót egy védett, jóváhagyott specifikációval szemben; a módosítások külön felülvizsgálati folyamaton mennek keresztül.

## Kérdések és válaszok

### Mit bizonyított az AlphaProof Code a Signal implementációjáról?

A Google DeepMind ellenőrzött biztonsági tulajdonságok igazolásáról számol be egy lefordított libsignal parancssori "heveder" esetében. A technikai cikk az üzenetek titkosságát és hitelességét fedi le, előrehaladási titkossággal és kompromisszum utáni biztonsággal a megadott modellek szerint. Az eredmény feltételeket tartalmaz a támadóra, a munkamenetre és a kriptográfiai feltételezésekre vonatkozóan. Hatóköre kizárja az általános garanciát minden Signal alkalmazásra vagy telepítésre.

### Ki dönti el, hogy mit kell egy AI által generált biztonsági igazolásnak alátámasztania?

Az emberi felülvizsgálók hagyják jóvá a specifikációt és annak feltételezéseit. A Google DeepMind technikai cikke leírja, hogy az ügynökök emberi útmutatással specifikációkat vázolnak fel, és a felülvizsgálók tesztelik, hogy az állítások megragadják-e a jelentőségteljes biztonsági tulajdonságokat. A Lean ellenőrzi az ebből eredő igazolás logikáját. Az emberek továbbra is felelősek az erős cél kiválasztásáért, a feltételezések felülvizsgálatáért és a jóváhagyott specifikáció javasolt változtatásainak elbírálásáért.

### Miért kell ellenőrizni a fordított gépi kódot a Rust fordítóban való bizalom helyett?

Egy lefordított binárisról szóló igazolás közvetlenül alátámasztja az adott műtermék megadott tulajdonságait. A Google DeepMind cikke elmagyarázza, hogy egy fordítási hiba, amely megsérti ezen tulajdonságok valamelyikét, hamissá tenné a tételt. A Rust fordító ezért elhagyja a megbízható alapot ehhez az állításhoz. Az igazolás továbbra is megbízik az utasításmodellben, a Lean kerneljében és a specifikált kriptográfiai szerződésekben.

### Hogyan akadályozza meg az összehasonlító, hogy egy igazolási ügynök gyengítse a célját?

Az összehasonlító ellenőrzi a tételt és minden definíciót, amelytől függ, egy védett, jóváhagyott specifikációval szemben. A Google DeepMind cikke szerint az igazolási ügynökök nem írhatnak ebbe a tárolt másolatba. Az ellenőrző ellenőrzi az engedélyezett axiómákat is, és új kernelben játssza le az igazolást. A javasolt specifikációs módosítások külön felülvizsgálati folyamaton mennek keresztül, míg az emberek továbbra is felelősek a cél erejéért.

### Mi volt a The Daily Diff ítélete az ellenőrzött igazolási munkafolyamatról?

A The Daily Diff ítélete SHIP IT volt. Niko élesítené az ellenőrzött igazolási munkafolyamatot, mert a jóváhagyott állítás elkülönül attól az ügynöktől, amely a választ adja. Minden eredményhez csatolná a hatóköröket és a feltételezéseket. Az epizód a Google közzétett igazolási műtermékét jelenti anélkül, hogy azt függetlenül újjáépítené, és jóváhagyja a munkafolyamatot ezeken a bizonyítékhatárokon belül.

## Fejezetek

- 0:00 Ki ellenőrzi egy AI biztonsági igazolását?
- 0:57 Hogyan válik egy állítás igazolási céllá?
- 1:39 Miért kell a lefordított binárist igazolni?
- 2:16 Mely biztonsági tulajdonságok élték túl az implementációs rést?
- 2:59 Visszautasíthatja a specifikáció a hibás kódot?
- 3:36 Válaszolhat-e egy helyes igazolás rossz kérdésre?
- 4:13 Mi fogja meg a mozgó célpontokat?
- 4:53 Élesíteném ezt az igazolási munkafolyamatot?

## Lefordított átirat

Az eredeti angol narrációból fordítva. A rendelkezésre álló hangot és feliratokat a YouTube vezérli.

### Ki ellenőrzi egy AI biztonsági igazolását?

0:00 Egy AI biztonsági audit még mindig úgy hangzik, mint egy chatbotban való bizalom. A Google új Signal eredménye matematikai igazolásokkal érkezik egy külön kernel ellenőrzésekkel. Ebben a videóban mit bizonyított a Google? És hogyan akadályozzák meg, hogy egy ügynök mozgassa a célpontokat? Itt van a hasznos válasz. A modellek jelölt igazolásokat írnak, és a Lean ellenőrzi az igazolásokat egy emberi jóváhagyással rendelkező állítás ellenében, amely kiválasztott fordított kódról szól. Az állítás és a feltételezések továbbra is emberek tulajdonában vannak.

0:21 Ellenőrizheti az eredményt anélkül, hogy hinne a modell győzelmi beszédének. Egy külön ellenőrzés észreveszi a kérdés csendes megváltoztatását. Le fogjuk követni a definíciókig. Kedden, november tizedike van, és ez a The Daily Diff. Az AlphaProof Code a Google keretrendszere szoftverspecifikációk írására emberi útmutatással és ellenőrzött igazolások generálására AI-ügynökökkel. Ez a tanulmány a libsignalt célozza, a Rust könyvtárat, amely a Signal üzenetküldési protokollját valósítja meg egy adott parancssori programban.

0:45 A Google ma jelentette be a munkát. A cikkük szerint öt kutató négy hétig dolgozott. Az ügynökök írták az igazolásokat, míg az emberek legtöbb erőfeszítésüket a specifikációkra fordították. A követelményeknek sikerült még drágább találkozókká válniuk. A specifikáció kimondja, hogy mit kell tennie a programnak,

### Hogyan válik egy állítás igazolási céllá?

0:59 mit irányít egy támadó, és mely feltételezésekre van szükség az érveléshez. A felülvizsgálók azt kérdezik, hogy megragadja-e a biztonságot, amelyre az emberek vágynak. Egy gyönyörűen ellenőrzött válasz egy gyenge kérdésre érintetlenül hagyja azt a kérdést. A csapat a Signal kézfogásával és üzenetkulcsos racsnijával kapcsolatos korábbi kutatásokra épít. Formális elemzések már tanulmányozták ezeket a terveket. A Google állítása a biztonsági érvelésüket egy módosítatlan gyártási könyvtár lefordított implementációjához köti, ahol a tervezésnek túl kell élnie a valódi kóddal való érintkezést. A Signal technológiai igazgatója, Ehren Kret,

1:27 a korábbi ellenőrzések kisebb hatókörének kibővítését írja le. Az implementációs részletek közé tartoznak a sorrenden kívüli üzenetek és az archivált munkamenetek a késleltetett üzenetekhez. A valódi szoftver megőrzi azokat a nyugtákat, amelyeket az elegáns diagramja eldobott. A kutatók a módosítatlan Rust könyvtárat a szabványos

### Miért kell a lefordított binárist igazolni?

1:41 fordítóval Arm sixty-four Linux futtathatóvá fordítják. Tételeik ezt a binárist formális utasításmodellel írják le, áthidalva a forráskód és az optimalizált gépi kód közötti szakadékot. Egy fordítási hiba, amely megsért egy megadott tulajdonságot, hamissá tenné a tételt. A fordító ezért elhagyja a megbízható alapot ehhez a binárishoz. Továbbra is megbízik az utasításmodellben és a Lean ellenőrzőjében. A bizalmi határ elmozdult, és van címe. Körülbelül hat és fél millió sor ellenőrzött igazolás alapja körülbelül huszonhat

2:06 ezer megbízható specifikációs és utasításszemantikai sor. Ezek műtermék-számok. Intelligencia-pontszámokként kezelni őket olyan, mintha a fejlesztőket a node\_modules mappájuk mérete alapján rangsorolnánk.

### Mely biztonsági tulajdonságok élték túl az implementációs rést?

2:16 Az érvelések az üzenetek titkosságát és hitelességét fedik le, előrehaladási titkossággal és kompromisszum utáni biztonsággal a megadott modellek szerint. Ez utóbbi kettő a lopott kulcsok okozta károk korlátait és a friss cserék utáni helyreállítást írja le. Minden garancia feltételeket támaszt a támadóra és a munkamenetre. A kriptográfiai primitívek megbízható szerződések mögött állnak. Az igazolás feltételezi, hogy ezek a rutinok a specifikáció szerint viselkednek, és kriptográfiai biztonsági feltételezésekre támaszkodik. Az egyik igazolás idealizálja a kriptográfiát; a másik a támadók siker valószínűségéről érvel.

2:42 Mindkettő korlátozásokat tartalmaz az általa lefedett forgatókönyvekre vonatkozóan. Kérdezze meg, melyik buildről, melyik tulajdonságról és mely feltételezésekről van szó. Ez az eredmény a kutatók parancssori "hevederére" vonatkozik. A csoportos üzenetküldés jövőbeli munka, és a számítási modell kizárja a többeszközös állapotot. Minden Signal telepítés hibamentesnek nevezése túlmegy a tételen. A kutatók két, korábban kijavított Signal hibát vezettek be újra

### Visszautasíthatja a specifikáció a hibás kódot?

3:02 izolált másolatokba és lefordították azokat. Az ellenőrzött igazolások kimutatták, hogy ezek a binárisok sértették a szimbolikus biztonsági tételt. Ez azt tesztelte, hogy a specifikáció elutasíthatja-e a valós, hibás implementációkat. A zöld pipának szüksége van egy piros tesztre. A Google közzéteszi a specifikációkat és az igazolásokat ellenőrzési utasításokkal. A tároló szerint egy tiszta build órákat és jelentős memóriát igényel. A bejelentés elolvasása jelentősen könnyebb a laptopon. A hardvermodell és a megbízható szerződések még mindig felülvizsgálatra szorulnak.

3:26 Nem építettem újjá az óriási műterméket ehhez az epizódhoz. A közzétett eredményt és annak határait jelentjük be. A kívülállóknak van módjuk megvizsgálni, ami számomra fontosabb, mint egy újabb AI győzelmi kör. Most jön a csapda.

### Válaszolhat-e egy helyes igazolás rossz kérdésre?

3:36 A Lean elfogadhat egy helyes igazolást egy olyan állításról, amely szinte semmit sem kér. Lehetetlen feltételezések üresjáratúvá tehetik a tételt. A címtétel alatt elrejtett definíció megváltoztatása gyengítheti a célt. A tanulmány ellenőrzéseket tervezett ez ellen. A kapuőr egy tárolt, jóváhagyott specifikációt tart fenn, amelyet az igazolási ügynökök nem írhatnak. Javításokat javasolhatnak egy külön módosítási folyamaton keresztül. A biztonsági gyengítést potenciális hibaként kezelik. Az igazoló sikerének deklarációjának nincs itt tekintélye.

4:00 Az emberek bírálják el a megbízható feltételezések változásait, közvetlenül vagy politikájukon keresztül, és felülvizsgálják a módosításokat minden kampány után. A szakértői ítélet marad a horogon. Az ügynök kérhet más feladatot. Nem adhat magának átmenő osztályzatot.

### Mi fogja meg a mozgó célpontokat?

4:13 Itt van az ígért ellenőrzés. A Lean összehasonlítója összehasonlítja a tételt és minden definíciót, amelytől függ, azzal a védett, jóváhagyott másolattal. Ellenőrzi az engedélyezett axiómákat is, és új kernelben játssza le az igazolást. Egy segítő definíció csendes gyengítése ezért megváltoztatja az összehasonlított dolgot. Egy elfogadott igazolásnak meg kell alapoznia a jóváhagyott célt. Ez továbbra is az embereket teszi felelőssé az erős cél és az őszinte feltételezések kiválasztásáért. Saját AI munkafolyamatához tartsa az elfogadási kritériumokat a

4:37 dolgozó szerkesztési jogosultságain kívül, és külön vizsgálja felül a javasolt változtatásokat. A Google eredménye ezt a szétválasztást kézzelfoghatóvá teszi. Az igazolásíró végzi a munkát; az ellenőrzési határ dönti el, hogy számít-e. Ha inkább elolvasná ezt, mint hallaná tőlem, a diff minden reggel megérkezik a postaládájába, ingyenesen a daily diff dot dev címen, link lent. Tehát a mai ítélet SHIP IT.

### Élesíteném ezt az igazolási munkafolyamatot?

4:54 Én élesíteném ezt az ellenőrzött igazolási munkafolyamatot, mert a jóváhagyott állítás elkülönül attól az ügynöktől, amely a választ adja. Minden eredményhez csatolnám a hatóköröket és a feltételezéseket. Iratkozz fel, nyomd meg a harangot, és írd meg kommentben, ha te másként pecsételted volna. És ez a mai diff. Én Niko vagyok az Axrisi-tól. Merge felelősségteljesen.

## Források

- [AlphaProof Code: Verifying Signal's Security at the Machine-Code Level — technical scope, trusted base and gatekeeping](https://google-deepmind.github.io/code-verification/) — Swarat Chaudhuri and colleagues / Google DeepMind and Google
- [Introducing AlphaProof Code — November 10 announcement and attributed Signal CTO response](https://deepmind.google/blog/introducing-alphaproof-code/) — Pushmeet Kohli and Swarat Chaudhuri / Google DeepMind
- [Code-verification repository — initial commit, public artifacts and checking instructions](https://github.com/google-deepmind/code-verification) — Google DeepMind / GitHub
- [The PQXDH Key Agreement Protocol — older official specification and prior-analysis context](https://signal.org/docs/specifications/pqxdh/) — Ehren Kret and Rolfe Schmidt / Signal
- [The Double Ratchet Algorithm — Triple Ratchet section](https://signal.org/docs/specifications/doubleratchet/) — Trevor Perrin, Moxie Marlinspike and Rolfe Schmidt / Signal
- [Google DeepMind leadership — Demis Hassabis's relevant lab identity](https://deepmind.google/about/) — Google DeepMind
- [Demis Hassabis in 2025 — authentic portrait, cropped/resized/compressed and unflipped; no background removal or generated expression/detail; lab identity only, no authorship, proof writing, current reaction or endorsement](https://commons.wikimedia.org/wiki/File:Demis_Hassabis_in_2025_by_Christopher_Michel.jpg) — Christopher P. Michel / Cmichel67 / Wikimedia Commons
- [Portrait licence — CC BY-SA 4.0; attribution, adaptation disclosure and ShareAlike](https://creativecommons.org/licenses/by-sa/4.0/) — Creative Commons
- [Expanding Brain template — cropped/captioned artifact-count satire, brief transformed <=2s commentary; no benchmark, hosting licence, legal-clearance or blanket reuse claim](https://imgflip.com/memetemplate/Expanding-Brain) — Imgflip / user-uploaded meme template
- [Tom and Jerry — Boomerang Official actual animated reaction, silent resized/captioned 1.875s excerpt; brief transformed process commentary, no actual researcher or executive reaction, hosting licence, legal-clearance or blanket reuse claim](https://giphy.com/gifs/boomerangtoons-mad-upset-1gdkNV0hroZjOXSHOU) — Boomerang Official / GIPHY / Tom and Jerry
- [Boomerang GIF source link — uploader-provided provenance](https://boomtn.co/GIPHY) — Boomerang
- [AlphaProof Code discussion — attention context, anonymous opinions excluded from factual proof claims](https://news.ycombinator.com/item?id=50439193) — Hacker News
- [Code-verification licence — Apache 2.0 for Google code, third-party licences retained](https://github.com/google-deepmind/code-verification/blob/808b4b7ffef198e6a91f71ed776d641a1c236882/LICENSE) — Google / GitHub