Tíz éve bizonyítja matematikailag az AWS-rendszerek helyességét az Amazon

A kutatási prototípusoktól a felhőszolgáltatásokig

Az Amazon 2016-ban indította el az Automated Reasoning Groupot, röviden ARG-t. A csoport célja az volt, hogy az AWS rendszereit ne csak teszteljék, hanem matematikai logikával bizonyítsák a helyességüket. Az Amazon Science beszámolója szerint az elmúlt évtizedben a kutatási projektekből olyan gyártási rendszerek lettek, amelyekre az AWS ügyfeleinek milliói támaszkodnak.

Az első ARG Demo Day egyik bemutatott eszköze a Tiros volt. Ez a virtuális magánhálózatok, vagyis VPC-k konfigurációival kapcsolatban válaszol kérdésekre, és képes azonosítani a hibás beállításokat, illetve biztonsági problémákat. A technológia később az Amazon Inspector hálózati biztonsági elemzésének alapjává vált, ma pedig a Reachability Analyzerben is használják.

A Tirosból emellett létrejött a Zelkova, amely szabályzatokat és azok lehetséges következményeit elemzi. Erre épül többek között az S3 Block Public Access és az IAM Access Analyzer is.

Matematikai garanciák az AWS ügyfeleinek

Az IAM Access Analyzer a Zelkova segítségével azt vizsgálja, hogy a hozzáférési szabályzatok ténylegesen milyen engedélyeket adnak. Az Amazon szerint az eszközt olyan ügyfelek is használják, mint a USAA és a GoTo, hogy felismerjék az erőforrásaikhoz vezető nem szándékos hozzáféréseket.

A Reachability Analyzer a Tirosra épül, és hálózati csomagok továbbítása nélkül elemzi az összes lehetséges hálózati útvonalat. Meg tudja válaszolni, hogy egy cél elérhető-e, illetve ha nem, melyik összetevő akadályozza az elérést.

Az automatizált következtetés a generatív mesterséges intelligenciában is megjelent. Az Amazon Bedrock Guardrails with Automated Reasoning a vállalat szerint formális logikával ellenőrzi, hogy a modell válaszai megfelelnek-e a meghatározott szabályzatoknak. Az Amazon legfeljebb 99 százalékos ellenőrzési pontosságot ad meg ehhez a funkcióhoz.

Ezek a szolgáltatások kielégíthetőségi moduloelméleteken alapuló megoldásokat, úgynevezett SMT-megoldókat és más automatizált következtetési technikákat használnak. A céljuk, hogy ne csak meghatározott tesztesetekben vizsgálják a rendszerek működését, hanem matematikai garanciát adjanak a viselkedésükre.

A felhő legmélyebb rétegeit is ellenőrzik

Az ARG munkája az AWS belső infrastruktúrájára is kiterjedt. Az Amazon szerint formális verifikációval bizonyították többek között az AWS Nitro Isolation Engine, az s2n-bignum kriptográfiai megvalósításai, az AWS adatközpontjaiban futó rendszerindító kód, valamint az S3 tárolórendszerek helyességét.

A csoport egy új engedélyezési motort is bizonyítottan helyesre fejlesztett és lecserélt. Ez a motor másodpercenként egymilliárd API-hívást kezel. Az új megoldást specifikációkkal és bizonyításokkal ellenőrizték, majd a termelési engedélyezések kvadrillióival vetették össze.

Az Amazon tapasztalata szerint a formális verifikáció nemcsak a biztonságot javíthatja, hanem egyszerűbbé és könnyebben karbantarthatóvá is teheti a rendszereket. A pontos specifikációk megírása gyakran egyszerűbb mérnöki megoldásokhoz vezet. A vállalat szerint a csoport tíz évének egyik fontos tanulsága, hogy a matematikai szigor és a gyakorlati fejlesztés egymást erősítheti.